proposition: Lemma wf_CAnd_and_nand: forall l1 r2, wf_re (CAnd l1) -> wf_re r2 -> [/\ r2 != CVoid , r2 != CNot CVoid & (forall l, r2 != CAnd l) ] -> wf_re (mkAnd (CAnd l1) r2).
proof: Proof. move => l1 r2. rewrite wf_re_CAnd. case/and4P => h1 h2 h3. move/allP => h4 h hh. rewrite toolmkAnd2_r => //. case_eq (undup (merge' (sort' l1) [:: r2])) => //. move => hd. case => [ | hd2 tl] //=. move => heq. have : hd \in l1 ++ [:: r2]. rewrite mem_cat. rewrite -(@mem_sort _ cregexp_le l1). rewrite -(@mem_sort _ cregexp_le [:: r2]). rewrite -mem_cat. rewrite -(@mem_merge _ cregexp_le). rewrite -mem_undup. rewrite heq. by apply/orP; left. rewrite mem_cat. case/orP => hu. by apply: h4. rewrite mem_seq1 in hu. by rewrite (eqP hu). move => heq. have : (hd \in l1 ++ [:: r2]) && (hd2 \in l1 ++ [::r2]) && (all (fun a => a \in l1 ++ [::r2]) tl). apply/andP; split. apply/andP; split. rewrite mem_cat -(@mem_sort _ cregexp_le l1) -(@mem_sort _ cregexp_le [::r2]). rewrite -mem_cat -(@mem_merge _ cregexp_le) -mem_undup heq. apply/orP; by left. rewrite mem_cat -(@mem_sort _ cregexp_le l1) -(@mem_sort _ cregexp_le [::r2]). rewrite -mem_cat -(@mem_merge _ cregexp_le) -mem_undup heq. apply/orP; right. apply/orP ; by left. apply/allP. move => x hx. rewrite mem_cat -(@mem_sort _ cregexp_le l1) -(@mem_sort _ cregexp_le [::r2]). rewrite -mem_cat -(@mem_merge _ cregexp_le) -mem_undup heq. apply/orP; right. by apply/orP; right. case/andP. case/andP => hh4 hh5. move/allP => hh6. apply/andP; split. have : uniq [:: hd , hd2 & tl]. rewrite -heq. by rewrite undup_uniq. done. apply/andP; split. have : sorted cregexp_le [:: hd, hd2 & tl]. rewrite -heq. rewrite undup_sorted => //. by apply: leS_trans. apply merge_sorted. by apply leS_total. apply: sort_sorted. by apply leS_total. done. case/andP => hss1 hss2. by apply/andP; split. apply/andP; split. rewrite mem_cat in hh4. case/orP : hh4 => hh4. by apply: h4. rewrite mem_seq1 in hh4. by rewrite (eqP hh4). apply/andP; split. rewrite mem_cat in hh5. case/orP : hh5 => hh5. by apply: h4. rewrite mem_seq1 in hh5. by rewrite (eqP hh5). apply/allP => x hx. have := (hh6 x hx). rewrite mem_cat. case/orP => hu. by apply: h4. by rewrite mem_seq1 in hu; rewrite (eqP hu). 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)