proposition: Lemma mkConcA : forall r1 r2 r3, mkConc (mkConc r1 r2) r3 = mkConc r1 (mkConc r2 r3).
proof: Proof. move => r1 r2 r3. case: (toolmkConc r1). - by move => heq; rewrite (eqP heq) !mkConc_CVoid_lt. - by move => heq; rewrite (eqP heq) !mkConc_CEps_lt. - case => l heq; rewrite (eqP heq). case: (toolmkConc r2). * by move => heq2; rewrite (eqP heq2) !mkConc_CVoid_lt. * by move => heq2; rewrite (eqP heq2) !mkConc_CEps_lt. * case => l2 heq2; rewrite (eqP heq2). rewrite {2}/mkConc. case: (toolmkConc r3). + by move => heq3; rewrite (eqP heq3) !mkConc_CVoid_rt. + by move => heq3; rewrite (eqP heq3) !mkConc_CEps_rt. + by case => l3 heq3; rewrite (eqP heq3) /mkConc catA. + case => h1 h2 h3. rewrite !(@mkConc_unfold _ r3) => //. by rewrite /mkConc catA. * case => h1 h2 h3. rewrite mkConc_unfold => //. case: (toolmkConc r3). + by move => heq3; rewrite (eqP heq3) !mkConc_CVoid_rt. + by move => heq3; rewrite (eqP heq3) !mkConc_CEps_rt mkConc_unfold. + case => l3 heq3; rewrite (eqP heq3) (@mkConc_unfold2 _ r2) /mkConc => //. by rewrite -catA. + case => h'1 h'2 h'3. rewrite (@mkConc_unfold3 r2 r3)=> //. rewrite (@mkConc_unfold _ r3) /mkConc => //. by rewrite -catA. - case => h1 h2 h3. case: (toolmkConc r2). * by move => heq2; rewrite (eqP heq2) !mkConc_CVoid_lt !mkConc_CVoid_rt mkConc_CVoid_lt. * by move => heq2; rewrite (eqP heq2) mkConc_CEps_rt !mkConc_CEps_lt. * case => l2 heq2; rewrite (eqP heq2). rewrite mkConc_unfold2 => //. case: (toolmkConc r3). + by move => heq3; rewrite (eqP heq3) !mkConc_CVoid_rt. + by move => heq3; rewrite (eqP heq3) !mkConc_CEps_rt mkConc_unfold2 => //. + by case => l3 heq3; rewrite (eqP heq3) !(@mkConc_unfold2 _ r1) => //. + case => h'1 h'2 h'3. rewrite !(@mkConc_unfold _ r3) => //. by rewrite mkConc_unfold2. * case => h'1 h'2 h'3. rewrite (@mkConc_unfold3 r1 r2) => //. case: (toolmkConc r3). + by move => heq3; rewrite (eqP heq3) !mkConc_CVoid_rt. + by move => heq3; rewrite (eqP heq3) !mkConc_CEps_rt mkConc_unfold3. + case => l3 heq3; rewrite (eqP heq3) (@mkConc_unfold2 _ r2) // (@mkConc_unfold2 _ r1) => //. + case => h''1 h''2 h''3. rewrite (@mkConc_unfold3 r2 r3)=> //. rewrite (@mkConc_unfold2 _ r1) => //. by rewrite (@mkConc_unfold _ r3) => //. 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)