proposition: Lemma mkAndAC_and_and_nand: forall l1 l2 r3, wf_re (CAnd l1) -> wf_re (CAnd l2) -> wf_re r3 -> [/\ r3 != CVoid , r3 != CNot CVoid & (forall l, r3 != CAnd l)] -> mkAnd (mkAnd (CAnd l1) (CAnd l2)) r3 = mkAnd (mkAnd (CAnd l1) r3) (CAnd l2).
proof: Proof. move => l1 l2 r3 hw1 hw2 hw3 hh. rewrite mkAnd_unfold => //. rewrite !toolmkAnd2_r => //. have hs1 : 2 <= size (undup (merge' (sort' (undup (merge' (sort' l1) (sort' l2)))) [:: r3])). rewrite (@perm_size _ (undup (merge' (sort' (undup (merge' (sort' l1) (sort' l2)))) [::r3])) (undup (l1++l2++[::r3]))). rewrite wf_re_CAnd in hw1. case/and4P : hw1 => h1 h2 h3 _. apply (@leq_trans (size l1)). done. rewrite -{1}(@undup_id _ l1). by apply tool_undup_size2. done. apply uniq_perm. by apply undup_uniq. by apply undup_uniq. move => u. by rewrite !mem_undup !mem_merge !mem_cat !mem_sort !mem_undup !mem_merge !mem_cat !mem_sort orbA. have hs2 : (2 <= size (undup (merge' (sort' l1) [::r3]))). rewrite (@perm_size _ (undup (merge' (sort' l1) [::r3])) (undup (l1++[::r3]))). rewrite wf_re_CAnd in hw1. case/and4P : hw1 => h1 h2 h3 _. apply (@leq_trans (size l1)). done. rewrite -{1}(@undup_id _ l1). by apply tool_undup_size2. done. apply uniq_perm. by apply undup_uniq. by apply undup_uniq. move => u. by rewrite !mem_undup !mem_merge !mem_cat !mem_sort. replace (match undup (merge' (sort' (undup (merge' (sort' l1) (sort' l2)))) [:: r3]) with | [::] => CNot CVoid | [:: c] => c | [:: c, s1 & s2] => CAnd [:: c, s1 & s2] end) with (CAnd (undup (merge' (sort' (undup (merge' (sort' l1) (sort' l2)))) [:: r3]))). replace (match undup (merge' (sort' l1) [:: r3]) with | [::] => CNot CVoid | [:: c] => c | [:: c, s1 & s2] => CAnd [:: c, s1 & s2] end) with (CAnd (undup (merge' (sort' l1) [::r3]))). rewrite mkAnd_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. done. 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 uniq_perm. by apply undup_uniq. by apply undup_uniq. move => u. by rewrite !mem_undup !mem_merge !mem_cat !mem_sort !mem_undup !mem_merge !mem_cat !mem_sort orbAC. rewrite wf_re_CAnd. apply/and4P; split. done. by apply undup_uniq. rewrite undup_sorted => //. by apply leS_trans. apply merge_sorted. by apply leS_total. apply sort_sorted. by apply leS_total. done. move :hw1. rewrite wf_re_CAnd. case/and4P => _ _ _. move/allP => hall. apply/allP => x. rewrite mem_undup mem_merge mem_cat !mem_sort. case/orP. by move => hu; apply: hall. rewrite mem_seq1 => heq. by rewrite (eqP heq). done. move : hs2. case: (undup (merge' (sort' l1) [::r3])) => //. move => hd. by case. move : hs1. case: (undup (merge' (sort' (undup (merge' (sort' l1) (sort' l2)))) [::r3])) => // hd. by case. 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)