proposition: Lemma CConcP : forall l1 l2 u, reflect (exists2 v1 , v1 \in CConc l1 & exists2 v2, v2 \in CConc l2 & u = v1++v2) (u \in (CConc (l1++l2))).
proof: Proof. elim => [ | hd tl ih] l2 u /=; rewrite -!topredE /= /mem_creg /=. - apply: (iffP idP). exists [::] => //. exists u => //. case => [v1 hv1 [v2 hv2 heq]]. case: l2 v2 hv2 heq => [ | hd2 tl2 ] v2 /=. * move: hv1. rewrite -!topredE /= /mem_creg /= /eps /=. move => h1 h2 -> ; by rewrite (eqP h1) (eqP h2). * move:hv1; rewrite -topredE /= /mem_creg /=. rewrite /eps /=; move=> h. move/concP => [w1 [w2 [hw [hw1 hw2]]]] ->. rewrite (eqP h). apply/concP. by exists w1, w2. - apply: (iffP (@concP char _ _ _)). * case => [v1 [v2 [hv [hv1 hv2]]]]. case: (ih l2 v2 hv2) => v2' hv2' [v3 hv3]. exists (v1 ++ v2'). rewrite -topredE /= /mem_creg /=. apply/concP; first by exists v1 , v2'. by exists v3 => //; rewrite hv q catA. * case => [v1]. rewrite -topredE /= /mem_creg /=. move/concP => [w1 [w2 [hw [hw1 hw2]]]]. case => [v2 hv2 ->]. exists w1 => //. exists (w2++v2) => //. split; first by rewrite hw catA. split => //; apply/ih. by exists w2 => //; exists v2. 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)