proposition: Lemma wf_CPlus_plus_plus: forall l1 l2, wf_re (CPlus l1) -> wf_re (CPlus l2) -> wf_re (mkPlus (CPlus l1) (CPlus l2)).
proof: Proof. rewrite /mkPlus => l1 l2 /=. case/and4P => hs1 hu1 hst1. move/allP => ha1. case/and4P => hs2 hu2 hst2. move/allP => ha2. case_eq (undup (merge' (sort' l1) (sort' l2))) => //. move => hd. case => [ | hd2 tl] //=. move => heq. have : hd \in l1 ++ l2. rewrite mem_cat. rewrite -(@mem_sort _ cregexp_le l1). rewrite -(@mem_sort _ cregexp_le l2). 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: ha1. by apply : ha2. move => heq. have : [&& (hd \in l1 ++ l2) , (hd2 \in l1 ++ l2) & (all (fun a => a \in l1 ++ l2) tl )]. apply/and3P; split. rewrite mem_cat -(@mem_sort _ cregexp_le l1) -(@mem_sort _ cregexp_le l2). 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 l2). 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 l2). rewrite -mem_cat -(@mem_merge _ cregexp_le) -mem_undup heq. apply/orP; right. by apply/orP; right. case/and3P => hh1 hh2. move/allP => hh3. apply/and3P ; split. have : uniq [:: hd , hd2 & tl]. rewrite -heq. by rewrite undup_uniq. move => hu. apply/and3P; split. by case/and3P : hu. by case/and3P: hu. by case/and3P: hu. 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. apply: sort_sorted. by apply leS_total. move => hs. apply/andP; split. by case/andP: hs. by case/andP: hs. apply/and3P; split. rewrite mem_cat in hh1. case/orP : hh1 => hh1. by apply: ha1. by apply: ha2. rewrite mem_cat in hh2. case/orP : hh2 => hh2. by apply: ha1. by apply: ha2. apply/allP => x hx. have := (hh3 x hx). rewrite mem_cat. case/orP => hu. by apply: ha1. by apply: ha2. 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)