proposition: Lemma mkPlusAC_nplus_nplus_plus : forall r1 r2 l3, wf_re r1 -> wf_re r2 -> wf_re (CPlus l3) -> (r1 != CVoid /\ (forall l, r1 != CPlus l)) -> (r2 != CVoid /\ (forall l, r2 != CPlus l)) -> mkPlus (mkPlus r1 r2) (CPlus l3) = mkPlus (mkPlus r1 (CPlus l3)) r2.
proof: Proof. move => r1 r2 l3 hw1 hw2 hw3 hh1 hh2. rewrite (@toolmkPlus3 r1 r2) => //. rewrite (@mkPlus_unfold3 _ r1) => //. rewrite (@mkPlus_unfold2 _ r2) => //. case_eq (compare r1 r2) => heq. - rewrite mkPlus_unfold3 => //. 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. done. apply sort_sorted. by apply leS_total. 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. rewrite mem_undup mem_merge mem_cat !mem_sort !mem_seq1. rewrite (compare_eq_axiom heq). by rewrite orbAC orbb. - rewrite mkPlus_unfold => //. 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. apply sort_sorted. by apply leS_total. 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. rewrite mem_seq2 mem_undup mem_merge mem_cat !mem_sort !mem_seq1. by rewrite orbAC. rewrite wf_re_CPlus /=. apply/and4P; split => //. rewrite andbT. apply/negP; rewrite mem_seq1 => heq2. move :heq. rewrite (eqP heq2). by rewrite compare_refl. by rewrite andbT /cregexp_le /leS /cmpS /= heq. by rewrite hw2. - rewrite mkPlus_unfold => //. 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. apply sort_sorted. by apply leS_total. 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. rewrite mem_seq2 mem_undup mem_merge mem_cat !mem_sort !mem_seq1. by rewrite orbAC orbC orbA orbAC. rewrite wf_re_CPlus /=. apply/and4P; split. rewrite andbT. apply/negP; rewrite mem_seq1 => heq2. move :heq. rewrite (eqP heq2). by rewrite compare_refl. rewrite andbT. move : heq ; rewrite /cregexp_le /leS /cmpS /= compare_neg. by case_eq (compare r2 r1). by rewrite hw2. by rewrite andbT. move: hw3. rewrite !wf_re_CPlus. case/and4P => h3 h4 h5. move/allP => h6. apply/and4P; split. apply (@leq_trans (size l3)) => //. rewrite (@perm_size _ (undup (merge' [::r1] (sort' l3))) (undup ([::r1]++l3))). rewrite -{1}(@undup_id _ l3) => //. by apply tool_undup_size. apply uniq_perm. by apply undup_uniq. by apply undup_uniq. move => u. by rewrite !mem_undup mem_merge !mem_cat mem_sort !mem_seq1. by apply undup_uniq. apply undup_sorted. by apply leS_trans. apply merge_sorted =>// . by apply leS_total. apply sort_sorted. by apply leS_total. apply/allP => x. rewrite mem_undup mem_merge mem_cat mem_sort mem_seq1. case/orP => hu. by rewrite (eqP hu). by apply : h6. 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)