proposition: Lemma gl_itr n (e: glang n n) a (e': lang): gl (tatom n a ⋅ e ⋅ tatom n a) ≡ e' ⋅ latom n a -> gl ((tatom n a ⋅ e)^+ ⋅ tatom n a) ≡ e'^+ ⋅ latom n a.
proof: Proof. rename n into m. intro H. rewrite <-itr_dot. apply antisym. - apply weq_spec in H as [H _]. intros w [g [-> [? <- [u [n Hn] Hg]]]]. apply tapp_nil_x_eq in Hg as [Hu ->]. revert u Hu Hn. induction n; intros u Hu Hn. destruct Hn as [v Hv [? <- Hn]]. apply tapp_x_nil_eq in Hn as [Hn ->]. destruct (H (gword_to_word m v)) as [u He [? <- H']]. repeat eexists; eauto. rewrite Hu. apply tapp_nil_x. rewrite Hn. apply tapp_x_nil. exists u. now exists O. eauto. destruct Hn as [w [v Hv [? <- Hn]] [w' Hw' H']]. apply tapp_x_nil_eq in Hn as [Hn ->]. assert (H'' := tapp_bounds H'). assert (Haw: a=thead w') by (rewrite Hn; intuition congruence). destruct (H (gword_to_word m v)) as [xe He [? <- Hxe]]. repeat eexists; eauto. rewrite Hu, <-(tapp_head H'). apply tapp_nil_x. rewrite Hn; apply tapp_x_nil. assert (Hext: e' ⋅ (e'^+ ⋅ latom m a) ≦ e'^+ ⋅ latom m a). now rewrite dotA, itr_cons. apply Hext. clear Hext. eexists. eassumption. eexists. apply IHn. apply Haw. assumption. rewrite (gword_tapp H'), Hxe, gword_to_word_cut, Haw, <-app_assoc. congruence. - apply itr_ind_l. now rewrite <-H, <-itr_ext, dotA. rewrite <-itr_cons at 2. destruct (gl_nildot a ((e ⋅ tatom m a)^+)) as [f' Hf]. rewrite 2dotA. rewrite gl_dot by eassumption. now rewrite Hf, dotA. Qed.
imports: Coq.PArith.BinPosDef denum lset sums normalisation kat ka_completeness untyping regex gregex lsyntax syntax lang glang boolean atoms