proposition: Lemma geval_dot n m p (x: guard n m) (y: guard m p): teval (g_dot1 x y) ≡ geval x ⋅ geval y.
proof: Proof. destruct x as [? a|? ? a e b]; destruct y as [? c|? ? c f d]; unfold g_dot1; (case eqb_spec; [intros <-|intro E]); unfold geval; rewrite ?sup_singleton; unfold sup. - now rewrite idem_atom_dot. - symmetry. apply (empty_atom_dot _ E). - now rewrite 2dotA, idem_atom_dot. - rewrite 2dotA, (empty_atom_dot _ E). ra. - now rewrite <-3dotA, idem_atom_dot. - rewrite <-2dotA, (empty_atom_dot _ E). ra. - transitivity (g_atom _ a⋅(e⋅(g_atom _ b⋅g_atom _ b)⋅f)⋅g_atom _ d). 2:ra. now rewrite idem_atom_dot. - transitivity (g_atom _ a⋅(e⋅(g_atom _ b⋅g_atom _ c)⋅f)⋅g_atom _ d). 2:ra. rewrite (empty_atom_dot _ E). ra. Qed.
imports: Coq.PArith.BinPosDef denum lset sums normalisation kat ka_completeness untyping regex gregex lsyntax syntax lang glang boolean atoms