proposition: Lemma mem_mkConc : forall r1 r2, (mkConc r1 r2) =i (CConc [:: r1 ; r2]).
proof: Proof. move => r1. case: (toolmkConc r1). - move => heq; rewrite (eqP heq) => r2 u; clear r1 heq. rewrite -!topredE /= /mem_creg /=. apply/idP/concP; first by case: r2 => //=. by case => w1; case => w2 [w [hw1 hw2]]. - move => heq; rewrite (eqP heq) /= => r2 u; clear r1 heq. rewrite -!topredE /= /mem_creg /=. apply/idP/concP. move => h; exists [::] => //. exists u => //=. split => //; split => //. apply/concP. by exists u => //; exists [::] => //; rewrite cats0. case => vnil /=. case => v [hu [hep hv]]. case: vnil hep hu => //= _. move: hv; case/concP => w [w0 [hw [hu hw0]]]. case: w0 hw0 hw => //= _. by rewrite cats0 => -> ->. - case => l heq; rewrite (eqP heq) => r2 u; clear r1 heq. case: (toolmkConc r2). * move => heq; rewrite (eqP heq); clear r2 heq. rewrite -!topredE /= /mem_creg /=. apply/idP/concP => //. case => v; case => w [hu [hw1 hw2]]. move: hw2 hu. by case/concP => x; case => x0 [hw [hx hx0]]. * move => heq; rewrite (eqP heq) /=; clear r2 heq. rewrite -!topredE /= /mem_creg /=. apply/idP/concP. move => h; exists u => //. exists [::]. split; first by rewrite cats0. split => //. apply/concP. exists [::] => //. by exists [::] => //. case => v; case => vnil [hu [hv hc]]. move: hc hu. move/concP. case => w; case => [w0 [hww0 [hw hw0]]]. case: w hw hww0 => // _. by case: w0 hw0 => //= _ ->->; rewrite cats0. * case => l' heq; rewrite (eqP heq) /=; clear r2 heq. change [:: CConc l; CConc l'] with ([:: CConc l] ++ [:: CConc l']). apply/CConcP/CConcP. case => v1 hv1 [v2 hv2 ->]. exists v1. rewrite -topredE /= /mem_creg /=. apply/concP. exists v1 => //. by exists [::] => //; rewrite cats0. exists v2 => //. rewrite -topredE /= /mem_creg /=. apply/concP. exists v2 => //. by exists [::] => //; rewrite cats0. case => v1 hv1 [v2 hv2 ->]. exists v1. move: hv1. rewrite -!topredE /= /mem_creg /=. case/concP => v. case => w [hvw [hv hw]]. case: w hw hvw => // _. by rewrite cats0 => ->. move: hv2. rewrite -!topredE /= /mem_creg /=. case/concP => v; case => w [hvw [hv hw]]. case: w hw hvw => // _. rewrite cats0 => ->. by exists v. * move => h; rewrite mkConc_unfold => //=. change [:: CConc l; r2] with ([:: CConc l]++[::r2]). apply/CConcP/CConcP. case => v hv [w hw ->]. exists v. rewrite -topredE /= /mem_creg /=. apply/concP. exists v => //. exists [::] => //; by rewrite cats0. by exists w. case => v hv [w hw -> ]. rewrite -topredE /= /mem_creg /= in hv. case/concP: hv => v'; case => w' [hv'w' [hv' hw']]. case: w' hv'w' hw' => //. rewrite cats0 =>-> _. by exists v' => //=; exists w. - move => h0 r2 u. case: (toolmkConc r2). * move => heq; rewrite (eqP heq) mkConc_CVoid_rt; clear r2 heq. rewrite -!topredE /= /mem_creg /=. apply/idP/concP => //. case => v. case => w [hvw [hv hw]]. case/concP: hw. by move => w0; case => w1 [hw0w1 [hw0 hw1]]. * move => heq; rewrite (eqP heq) mkConc_CEps_rt ; clear r2 heq. rewrite -!topredE /= /mem_creg /=. apply/idP/concP. move => h; exists u => //. exists [::] => /=. split; first by rewrite cats0. split => //. apply/concP. exists [::] => //. by exists [::] => //. case => v; case => vnil [huv [hv hvnil]]. move/concP: hvnil; case => w0; case => w1 [hw0w1 [hw0 hw1]]. case: w0 hw0 hw0w1 => // _. case: w1 hw1 => // _. move: huv. rewrite cats0=>->->. by rewrite cats0. * case => l' heq; rewrite (eqP heq) mkConc_unfold2 //=; clear r2 heq. rewrite -!topredE /= /mem_creg /=. apply/concP/concP. case => v; case => w [hvw [hv hw]]. exists v => //. exists w => //. split => //; split => //. apply/concP. exists w => //. by exists [::] => //; rewrite cats0. case => v; case => w [hvw [hv hw]]. case/concP: hw => w'; case => w0 [hw'w0 [hw' hw0]]. case: w0 hw'w0 hw0 => // heq _. move: heq hvw hw'. rewrite cats0 =><- hw'. by exists v => //; exists w. * move => h1. by rewrite mkConc_unfold3 => //. 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)