proposition: Lemma derE : forall x e, der x e =i residual x (mem e).
proof: Proof. move=> x; elim=> //= [ | y | e IHe | e1 IHe1 e2 IHe2 | e1 IHe1 e2 IHe2 | e1 IHe1 e2 IHe2 | e1 IHe1] u. - rewrite -!topredE /=. apply/idP/idP => h. rewrite /eps !inE /= in h . by rewrite (eqP h) /=. rewrite /residual !inE /= in h. by case :u h. - by rewrite 2!fun_if. - by apply/concP/concP=> [] [v e_v]; exists v; rewrite // IHe in e_v *. - by rewrite !inE IHe1 IHe2. - by rewrite !inE IHe1 IHe2. - case he: (has_eps e1). + apply/orP/concP=> [[] | [[|y v]]] /=; rewrite -/mem_reg. * move/concP=> [w1 [w2 uw]]. move: uw; rewrite IHe1 in_residual; move => [uw [w1e w2e]]. by exists (x :: w1), w2; rewrite uw. * move => hu. exists [::]. rewrite -has_epsE. exists (x::u) => //. by rewrite -in_residual -IHe2. * case=> w [def_w [_ e2w]]; right. by rewrite IHe2 !inE def_w. * case=> w [[xy uvw] [e1w e2w]]; left; apply/concP. by exists v, w; rewrite IHe1 xy in_residual. + apply/concP/concP => [[v] | ] /=; rewrite -/mem_reg. case=> w [uw [e1w e2w]]. exists (x :: v), w. by rewrite uw -in_residual -IHe1. + case; case => [|y v]; case => /= w [hv [he1 he2]]. by move: he; rewrite has_epsE he1. move/eqP: hv. rewrite eqseq_cons. case/andP. move/eqP => hx. move/eqP => hu. exists v. by rewrite IHe1 in_residual hx; exists w. - by rewrite -topredE /= /compl /= topredE IHe1. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegLang(languages) RegexpBrzozowski(glue)