proposition: Lemma clean_inner_dot n m (e: guard n m) (He: clean1 e): forall p (f: guard m p), clean1 f -> gl (tatom n (fst e) ⋅ G (g_inner_dot e f) ⋅ tatom p (fst e)) ≡ latom n (fst e) ⋅ R (v (o (g_inner_dot e f))) ⋅ latom p (fst e).
proof: Proof. assert (Z: forall n m p q (e: glang n m) (f: glang p q) e' f', gl (e⋅G 0⋅f) ≡ e'⋅R 0⋅f'). intros. rewrite G.lang_0, dotx0, dot0x, gl_bot. setoid_rewrite R.lang_0. ra. destruct e as [n a|n m a e b]; destruct f as [p c|p q c f d]; intros Hf; simpl fst; simpl lst; simpl g_inner_dot. - apply Z. - case eqb_spec. intros <-. 2: intros; apply Z. case eqb_spec. intros <-. 2: intros; apply Z. unfold andb. unfold clean1, geval in Hf. rewrite 2G.lang_dot, 2G.lang_atom in Hf. rewrite Hf. rewrite <-2R_lang_atom, <-2R.lang_dot. reflexivity. - case eqb_spec. intros <-. 2: intros; apply Z. case eqb_spec. intros <-. 2: intros; apply Z. unfold andb. unfold clean1, geval in He. rewrite 2G.lang_dot, 2G.lang_atom in He. rewrite He. rewrite <-2R_lang_atom, <-2R.lang_dot. reflexivity. - case eqb_spec. intros <-. 2: intros; apply Z. case eqb_spec. intros <-. 2: intros; apply Z. unfold andb. unfold clean1, geval in He. rewrite 2G.lang_dot, 2G.lang_atom in He. unfold clean1, geval in Hf. rewrite 2G.lang_dot, 2G.lang_atom in Hf. simpl o in *; simpl v in *. rewrite 2R.lang_dot in He. repeat change (o_pred ?a (atom ?b)) with (o (g_atom a b)) in He. setoid_rewrite R_lang_atom in He. rewrite 2R.lang_dot in Hf. repeat change (o_pred ?a (atom ?b)) with (o (g_atom a b)) in Hf. setoid_rewrite R_lang_atom in Hf. rewrite 2R.lang_dot. repeat change (o_pred ?a (atom ?b)) with (o (g_atom a b)). setoid_rewrite R_lang_atom. setoid_rewrite G.lang_dot. rewrite dotA. setoid_rewrite G.lang_dot. rewrite G.lang_atom. rewrite dotA. rewrite <-(dotA _ (G f)). rewrite <-2dotA in Hf. rewrite gl_dot by eassumption. ra. Qed.
imports: Coq.PArith.BinPosDef denum lset sums normalisation kat ka_completeness untyping regex gregex lsyntax syntax lang glang boolean atoms