proposition: Lemma incl_star_tool: forall tl hd E F u, similar F (wder_sigma (wder u E) (Star E) [::] (hd :: tl)) -> exists e : regexp, exists l : seq regexp, set_of_der E e /\ gpred_list (set_of_der E) l /\ similar F (rPlus2 (Conc e (Star E)) (Star E) l).
proof: Proof. elim => [ | hd2 tl hi] hd E F u /=. - case he: (has_eps (wder u E)) => /=. + move => hsim. exists (wder (u++[::hd]) E); exists [:: (der hd E)]; split => /=. * exists (u ++ [:: hd]); reflexivity. split => /=. * split => //=. by exists [:: hd]; reflexivity. by rewrite wder_cat => /=. move => hsim. exists (wder (u++[::hd]) E); exists [::]; split => //=. + exists (u++ [::hd]); reflexivity. split => //. by rewrite wder_cat => /=. case: (hi hd2 E (wder_sigma (wder [::hd] E) (Star E) [::] (hd2::tl)) [::hd]) => //= [ | e1 [l1 [hder1 [hpred1]]]]. - reflexivity. case: (hi hd2 E (wder_sigma (wder (u++[::hd]) E) (Star E) [::] (hd2::tl)) (u++[::hd])) => //= [ | e2 [l2 [hder2 [hpred2]]]]. - reflexivity. rewrite !wder_cat. case : (has_eps (wder u E)); case: (has_eps (der hd (wder u E))); case: (has_eps (der hd E)). - rewrite -!wder_sigma_switch !wder_Plus !wder_Conc /=. move => hsim2 hsim1. exists e1; exists (e2::l2++l1); split => //. split => /=. + split => //. by apply gpred_list_cat. transitivity (Plus (Plus (wder_sigma (der hd2 (der hd (wder u E))) (Star E) [::] tl) (wder_sigma (der hd2 E) (Star E) [::] tl)) (Plus (wder_sigma (der hd2 (der hd E)) (Star E) [::] tl) (wder_sigma (der hd2 E) (Star E) [::] tl))) => //. transitivity (Plus (rPlus2 (Conc e2 (Star E)) (Star E) l2) (rPlus2 (Conc e1 (Star E)) (Star E) l1)). + by apply similar_congr_Plus. by apply rPlus2_cat. - rewrite -!wder_sigma_switch !wder_Conc /=. move => hsim2 hsim1 hF. exists e1; exists (e2::l2++l1); split => //. split => /=. + split => //. by apply gpred_list_cat. transitivity (Plus (Plus (wder_sigma (der hd2 (der hd (wder u E))) (Star E) [::] tl) (wder_sigma (der hd2 E) (Star E) [::] tl)) (wder_sigma (der hd2 (der hd E)) (Star E) [::] tl)) => //. transitivity (Plus (rPlus2 (Conc e2 (Star E)) (Star E) l2) (rPlus2 (Conc e1 (Star E)) (Star E) l1)). + by apply similar_congr_Plus. by apply rPlus2_cat. - rewrite -!wder_sigma_switch !wder_Plus !wder_Conc /=. move => hsim2 hsim1 hF. exists e1; exists (e2::l2++l1); split => //. split => /=. + split => //. by apply gpred_list_cat. transitivity (Plus (wder_sigma (der hd2 (der hd (wder u E))) (Star E) [::] tl) (Plus (wder_sigma (der hd2 (der hd E)) (Star E) [::] tl) (wder_sigma (der hd2 E) (Star E) [::] tl))) => //. transitivity (Plus (rPlus2 (Conc e2 (Star E)) (Star E) l2) (rPlus2 (Conc e1 (Star E)) (Star E) l1)). + by apply similar_congr_Plus. by apply rPlus2_cat. - rewrite -!wder_sigma_switch !wder_Conc /=. move => hsim2 hsim1 hF. exists e1; exists (e2::l2++l1); split => //. split => /=. + split => //. by apply gpred_list_cat. transitivity (Plus (wder_sigma (der hd2 (der hd (wder u E))) (Star E) [::] tl) (wder_sigma (der hd2 (der hd E)) (Star E) [::] tl)) => //. transitivity (Plus (rPlus2 (Conc e2 (Star E)) (Star E) l2) (rPlus2 (Conc e1 (Star E)) (Star E) l1)). + by apply similar_congr_Plus. by apply rPlus2_cat. - rewrite -!wder_sigma_switch !wder_Conc /=. move => hsim2 _ hf. exists e2; exists l2; split => //. split => //. by transitivity (Plus (wder_sigma (der hd2 (der hd (wder u E))) (Star E) [::] tl) (wder_sigma (der hd2 E) (Star E) [::] tl)) => //. - rewrite -!wder_sigma_switch !wder_Conc /=. move => hsim2 _ hF. exists e2; exists l2; split => //. split => //. by transitivity (Plus (wder_sigma (der hd2 (der hd (wder u E))) (Star E) [::] tl) (wder_sigma (der hd2 E) (Star E) [::] tl)). - rewrite -!wder_sigma_switch !wder_Conc /=. move => hsim2 _ hF. exists e2; exists l2; split => //. split => //. by transitivity (wder_sigma (der hd2 (der hd (wder u E))) (Star E) [::] tl). rewrite -!wder_sigma_switch /=. move => hsim2 hF. exists e2; exists l2; split => //. split => //. by transitivity (wder_sigma (der hd2 (der hd (wder u E))) (Star E) [::] tl). Qed.
imports: Coq(RelationClasses Setoid Morphisms Permutation) Coq(SetoidList Mergesort Orders) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegLang(languages) RegexpBrzozowski(glue gfinset regexp)