proposition: Lemma canonize_mem : forall c u, (u \in c) = ( u \in canonize c).
proof: Proof. elim => [ | | | s | c1 hc1 | c1 hc1 c2 hc2 | c1 hc1 c2 hc2 | c1 hc1 c2 hc2 | c1 hc1] u //=. - rewrite -mkStar_mem. rewrite -!topredE /= /mem_creg /=. by apply/starP/starP; case => v; move/allP => h1 h2; exists v => //; apply/allP => x hx; case/andP : (h1 x hx) => hh1 hh2; rewrite !inE hh1 /=; [ rewrite -hc1 | rewrite hc1]. - rewrite mem_mkPlus. rewrite -!topredE /= /mem_creg /=. apply/orP/orP. * move => [h1 | h2]; [left | right ]. by rewrite -hc1. by rewrite inE orbF -hc2. * move => [h1 | h2 ]; [left | right]; first by rewrite hc1. move/orP : h2 => [h1 | h2] //. by rewrite hc2. - rewrite mem_mkAnd. rewrite -!topredE /= /mem_creg /=. apply/andP/andP; rewrite !inE => [[h1 h2]]. * by rewrite -hc1 -hc2 h1 h2 andbT. * move/andP: h2 => [h2 h3]. by rewrite hc1 h1 hc2 h2. - rewrite mem_mkConc. rewrite -!topredE /= /mem_creg /=. apply/concP/concP. * case => v1; case => v2 [heq [hv2 hv1]]. exists v1 , v2. split => //. split; first by rewrite -hc1. apply/concP. exists v2, [::]. split; first by rewrite cats0. by rewrite -hc2. * case => v1; case => v2 [heq [hv1 hv2]]. case/concP: hv2 => v2'; case => v3 [hv2'v3 [hv2' hv3]]. case: v3 hv2'v3 hv3 => //. rewrite cats0 => hv2'v3 _. exists v1 , v2'. rewrite -hv2'v3; split => //. split; first by rewrite hc1. by rewrite hc2 hv2'v3. - rewrite mem_mkNot. rewrite -!topredE /= /mem_creg /=. congr negb. by rewrite topredE hc1. Qed.
imports: Coq(RelationClasses Setoid Morphisms) HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegLang(languages) RegexpBrzozowski(glue regexp finite_der equiv)