proposition: Lemma gl_dot n m p (e: glang n m) a (f: glang m p) (e' f': lang): gl (e ⋅ tatom m a) ≡ e' ⋅ latom m a -> gl (tatom m a ⋅ f) ≡ latom m a ⋅ f' -> gl (e ⋅ tatom m a ⋅ f) ≡ e' ⋅ latom m a ⋅ f'.
proof: Proof. setoid_rewrite weq_spec. intros He Hf. split; intro w. - apply proj1 in He. apply proj1 in Hf. intros [g [-> [xa [x Hx [? <- Hxa]] [y Hy Hg]]]]. apply tapp_x_nil_eq in Hxa as [Ha ->]. destruct (tapp_bounds Hg) as (H1&H2&H3). destruct (He (gword_to_word n x)) as [x' Hx' [? <- Hxa']]. repeat eexists; eauto. rewrite Ha. apply tapp_x_nil. destruct (Hf (gword_to_word m y)) as [? <- [y' Hy' Hay']]. repeat eexists; eauto. rewrite Ha. rewrite H1. apply tapp_nil_x. repeat eexists; eauto. rewrite <-app_assoc, <-Hay', (gword_to_word_cut m y), (gword_tapp Hg), app_assoc. congruence. - apply proj2 in He. apply proj2 in Hf. intros [ea [x Hx [? <- ->]] [y Hy ->]]. edestruct (He (x++atom_to_word m a)) as [xa [Hxa [x' Hx' [? <- Hxa']]]]. eexists; eauto. edestruct (Hf (atom_to_word m a++y)) as [ay [Hay [? <- [y' Hy' Hay']]]]. eexists; eauto. apply tapp_x_nil_eq in Hxa' as [-> ->]. apply tapp_nil_x_eq in Hay' as [Ha ->]. destruct (tapp_cat x' y' Ha) as [z Hz]. repeat eexists; eauto. 2: apply tapp_x_nil. rewrite (gword_tapp Hz), <-Hxa, <-app_assoc, Hay, gword_to_word_cut, <-app_assoc. congruence. Qed.
imports: Coq.PArith.BinPosDef denum lset sums normalisation kat ka_completeness untyping regex gregex lsyntax syntax lang glang boolean atoms