proposition: Lemma teval_inner_dot n m p (x: guard n m) (y: guard m p): dirac n p + g_atom _ (fst x) ⋅ g_inner_dot x y ⋅ g_atom _ (fst x) ≡ dirac n p + ofbool (eqb (fst x) (lst y)) ⋅ geval x ⋅ geval y.
proof: Proof. unfold g_inner_dot. revert p y. destruct x as [n a|n m a e b]; destruct y as [p c|p q c f d]; simpl fst; simpl lst; simpl geval. rewrite dirac_refl. case eqb. 2: ra. ra_normalise. setoid_rewrite <-inj_cap. rewrite <-inj_top, <-inj_cup. apply inj_weq. lattice. case eqb_spec; intro E. subst. case eqb_spec; intro E'. subst. simpl. ra_normalise. now rewrite idem_atom_dot. ra. simpl. ra_normalise. rewrite <-(dotA _ (g_atom p a)). rewrite empty_atom_dot by assumption. ra. case eqb_spec; intro E. subst. case eqb_spec; intro E'. subst. simpl. ra_normalise. now rewrite <-3dotA, idem_atom_dot. ra. simpl. case eqb_spec; intro E'. subst. ra_normalise. rewrite <-dotA. rewrite empty_atom_dot by congruence. ra. ra. case eqb_spec; intro E. subst. case eqb_spec; intro E'. subst. simpl. ra_normalise. now rewrite <-(dotA _ (g_atom p c) (g_atom p c)), idem_atom_dot. ra. simpl. case eqb_spec; intro E'. subst. ra_normalise. rewrite <-(dotA _ (g_atom p b) (g_atom p c)), empty_atom_dot by assumption. ra. ra. Qed.
imports: Coq.PArith.BinPosDef denum lset sums normalisation kat ka_completeness untyping regex gregex lsyntax syntax lang glang boolean atoms