proposition: Lemma mkPlusAC_nplus_nplus_nplus : forall r1 r2 r3, wf_re r1 -> wf_re r2 -> wf_re r3 -> (r1 != CVoid /\ (forall l, r1 != CPlus l)) -> (r2 != CVoid /\ (forall l, r2 != CPlus l)) -> (r3 != CVoid /\ (forall l, r3 != CPlus l)) -> mkPlus (mkPlus r1 r2) r3 = mkPlus (mkPlus r1 r3) r2.
proof: Proof. move => r1 r2 r3 hw1 hw2 hw3 hh1 hh2 hh3. rewrite (@toolmkPlus3 r1 r2) ?(@toolmkPlus3 r1 r3) => //. case_eq (compare r1 r2) => heq1 //. - case_eq (compare r1 r3) => heq2. + by rewrite -(compare_eq_axiom heq1) -(compare_eq_axiom heq2). + rewrite toolmkPlus3 ?mkPlus_unfold2 ?heq2 => //. f_equal. apply (@sorted_eq _ cregexp_le). by apply leS_trans. by apply leS_antisym. simpl. by rewrite andbT /cregexp_le /leS /cmpS /= heq2. apply undup_sorted. by apply leS_trans. apply merge_sorted. by apply leS_total. apply sort_sorted. by apply leS_total. done. apply uniq_perm. simpl. rewrite andbT. apply/negP. rewrite mem_seq1 => h. move : heq2. by rewrite (eqP h) compare_refl. by apply undup_uniq. move => u. rewrite mem_undup mem_merge mem_cat mem_sort !mem_seq2 mem_seq1. rewrite (compare_eq_axiom heq1). by rewrite orbAC orbb orbC. rewrite wf_re_CPlus. apply/and4P; split => //=. rewrite andbT. apply/negP; rewrite mem_seq1 => heq. move: heq2. by rewrite (eqP heq) compare_refl. rewrite andbT. by rewrite /cregexp_le /leS /cmpS /= heq2. by rewrite hw1 hw3. + rewrite toolmkPlus3 ?mkPlus_unfold2 ?heq2 => //. f_equal. apply : (@sorted_eq _ cregexp_le). by apply leS_trans. by apply leS_antisym. simpl. by rewrite andbT /cregexp_le /leS /cmpS /= compare_neg heq2. apply undup_sorted. by apply leS_trans. apply merge_sorted. by apply leS_total. apply sort_sorted. by apply leS_total. done. apply uniq_perm. simpl. rewrite andbT. apply/negP. rewrite mem_seq1 => h. move : heq2. by rewrite (eqP h) compare_refl. by apply undup_uniq. move => u. rewrite !mem_undup !mem_merge !mem_cat !mem_sort !mem_seq2 !mem_seq1. rewrite (compare_eq_axiom heq1). by rewrite -orbA orbb. rewrite wf_re_CPlus. apply/and4P; split => //=. rewrite andbT. apply/negP; rewrite mem_seq1 => heq. move: heq2. by rewrite (eqP heq) compare_refl. rewrite andbT. by rewrite /cregexp_le /leS /cmpS /= compare_neg heq2. by rewrite hw1 hw3. - case_eq (compare r1 r3) => heq2 //. + rewrite mkPlus_unfold2 ?toolmkPlus3 => //. rewrite heq1. f_equal. apply (@sorted_eq _ cregexp_le). by apply leS_trans. by apply leS_antisym. apply undup_sorted. by apply leS_trans. apply merge_sorted. by apply leS_total. apply sort_sorted. by apply leS_total. done. simpl. rewrite andbT. by rewrite /cregexp_le /leS /cmpS /= heq1. apply uniq_perm. by apply undup_uniq. simpl. rewrite andbT. apply/negP. rewrite mem_seq1 => h. move : heq1. by rewrite (eqP h) compare_refl. move => u. rewrite mem_undup mem_merge mem_cat mem_sort !mem_seq2 mem_seq1. rewrite (compare_eq_axiom heq2). by rewrite orbAC orbb orbC. rewrite wf_re_CPlus. apply/and4P; split => //=. rewrite andbT. apply/negP; rewrite mem_seq1 => heq. move: heq1. by rewrite (eqP heq) compare_refl. rewrite andbT. by rewrite /cregexp_le /leS /cmpS /= heq1. by rewrite hw1 hw2. + rewrite !mkPlus_unfold2 => //. f_equal. apply : (@sorted_eq _ cregexp_le). by apply leS_trans. by apply leS_antisym. apply undup_sorted. by apply leS_trans. apply merge_sorted. by apply leS_total. apply sort_sorted. by apply leS_total. done. apply undup_sorted. by apply leS_trans. apply merge_sorted. by apply leS_total. apply sort_sorted. by apply leS_total. done. apply uniq_perm. by apply undup_uniq. by apply undup_uniq. move => u. rewrite !mem_undup !mem_merge !mem_cat !mem_sort !mem_seq2 !mem_seq1. by rewrite orbAC. rewrite wf_re_CPlus. apply/and4P; split => //=. rewrite andbT. apply/negP; rewrite mem_seq1 => heq. move: heq2. by rewrite (eqP heq) compare_refl. rewrite andbT. by rewrite /cregexp_le /leS /cmpS /= heq2. by rewrite hw1 hw3. rewrite wf_re_CPlus. apply/and4P; split => //=. rewrite andbT. apply/negP; rewrite mem_seq1 => heq. move: heq1. by rewrite (eqP heq) compare_refl. rewrite andbT. by rewrite /cregexp_le /leS /cmpS /= heq1. by rewrite hw1 hw2. + rewrite !mkPlus_unfold2 => //. f_equal. apply : (@sorted_eq _ cregexp_le). by apply leS_trans. by apply leS_antisym. apply undup_sorted. by apply leS_trans. apply merge_sorted. by apply leS_total. apply sort_sorted. by apply leS_total. done. apply undup_sorted. by apply leS_trans. apply merge_sorted. by apply leS_total. apply sort_sorted. by apply leS_total. done. apply uniq_perm. by apply undup_uniq. by apply undup_uniq. move => u. rewrite !mem_undup !mem_merge !mem_cat !mem_sort !mem_seq2 !mem_seq1. by rewrite orbC orbA. rewrite wf_re_CPlus. apply/and4P; split => //=. rewrite andbT. apply/negP; rewrite mem_seq1 => heq. move: heq2. by rewrite (eqP heq) compare_refl. rewrite andbT. by rewrite /cregexp_le /leS /cmpS /= compare_neg heq2. by rewrite hw1 hw3. rewrite wf_re_CPlus. apply/and4P; split => //=. rewrite andbT. apply/negP; rewrite mem_seq1 => heq. move: heq1. by rewrite (eqP heq) compare_refl. rewrite andbT. by rewrite /cregexp_le /leS /cmpS /= heq1. by rewrite hw1 hw2. - case_eq (compare r1 r3) => heq2 //. + rewrite mkPlus_unfold2 ?toolmkPlus3 => //. rewrite heq1. f_equal. apply (@sorted_eq _ cregexp_le). by apply leS_trans. by apply leS_antisym. apply undup_sorted. by apply leS_trans. apply merge_sorted. by apply leS_total. apply sort_sorted. by apply leS_total. done. simpl. rewrite andbT. by rewrite /cregexp_le /leS /cmpS /= compare_neg heq1. apply uniq_perm. by apply undup_uniq. simpl. rewrite andbT. apply/negP. rewrite mem_seq1 => h. move : heq1. by rewrite (eqP h) compare_refl. move => u. rewrite mem_undup mem_merge mem_cat mem_sort !mem_seq2 mem_seq1. rewrite (compare_eq_axiom heq2). by rewrite -orbA orbC orbb orbC. rewrite wf_re_CPlus. apply/and4P; split => //=. rewrite andbT. apply/negP; rewrite mem_seq1 => heq. move: heq1. by rewrite (eqP heq) compare_refl. rewrite andbT. by rewrite /cregexp_le /leS /cmpS /= compare_neg heq1. by rewrite hw2 hw1. + rewrite !mkPlus_unfold2 => //. f_equal. apply : (@sorted_eq _ cregexp_le). by apply leS_trans. by apply leS_antisym. apply undup_sorted. by apply leS_trans. apply merge_sorted. by apply leS_total. apply sort_sorted. by apply leS_total. done. apply undup_sorted. by apply leS_trans. apply merge_sorted. by apply leS_total. apply sort_sorted. by apply leS_total. done. apply uniq_perm. by apply undup_uniq. by apply undup_uniq. move => u. rewrite !mem_undup !mem_merge !mem_cat !mem_sort !mem_seq2 !mem_seq1. by rewrite -orbA orbC. rewrite wf_re_CPlus. apply/and4P; split => //=. rewrite andbT. apply/negP; rewrite mem_seq1 => heq. move: heq2. by rewrite (eqP heq) compare_refl. rewrite andbT. by rewrite /cregexp_le /leS /cmpS /= heq2. by rewrite hw1 hw3. rewrite wf_re_CPlus. apply/and4P; split => //=. rewrite andbT. apply/negP; rewrite mem_seq1 => heq. move: heq1. by rewrite (eqP heq) compare_refl. rewrite andbT. by rewrite /cregexp_le /leS /cmpS /= compare_neg heq1. by rewrite hw2 hw1. + rewrite !mkPlus_unfold2 => //. f_equal. apply : (@sorted_eq _ cregexp_le). by apply leS_trans. by apply leS_antisym. apply undup_sorted. by apply leS_trans. apply merge_sorted. by apply leS_total. apply sort_sorted. by apply leS_total. done. apply undup_sorted. by apply leS_trans. apply merge_sorted. by apply leS_total. apply sort_sorted. by apply leS_total. done. apply uniq_perm. by apply undup_uniq. by apply undup_uniq. move => u. rewrite !mem_undup !mem_merge !mem_cat !mem_sort !mem_seq2 !mem_seq1. by rewrite orbC orbAC orbA. rewrite wf_re_CPlus. apply/and4P; split => //=. rewrite andbT. apply/negP; rewrite mem_seq1 => heq. move: heq2. by rewrite (eqP heq) compare_refl. rewrite andbT. by rewrite /cregexp_le /leS /cmpS /= compare_neg heq2. by rewrite hw3 hw1. rewrite wf_re_CPlus. apply/and4P; split => //=. rewrite andbT. apply/negP; rewrite mem_seq1 => heq. move: heq1. by rewrite (eqP heq) compare_refl. rewrite andbT. by rewrite /cregexp_le /leS /cmpS /= compare_neg heq1. by rewrite hw2 hw1. 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)