proposition: Lemma toolmkAnd3 : forall r1 r2, [/\ r1 != CVoid, r1 != CNot CVoid & (forall l, r1 != CAnd l)] -> [/\ r2 != CVoid , r2 != CNot CVoid & (forall l, r2 != CAnd l) ] -> mkAnd r1 r2 = match compare r1 r2 with | Lt => CAnd [:: r1; r2] | Eq => r1 | Gt => CAnd [:: r2; r1] end .
proof: Proof. case => [ | | | s | c | l | l | l | c ] r2 [] _ //=. - case : r2 => [ | | | t | d | k | k | k | d ] _ _ [] //= _. move => _ h. move/negP: (h k); by case. by case: d. - case : r2 => [ | | | t | d | k | k | k | d ] _ _ [] //= _. move => _ h. move/negP: (h k); by case. by case: d. - case : r2 => [ | | | t | d | k | k | k | d ] _ _ [] //= _. move => _ h. move/negP: (h k); by case. by case: d. - case : r2 => [ | | | t | d | k | k | k | d ] _ _ [] //= _. move => _ h. move/negP: (h k); by case. by case: d. - case : r2 => [ | | | t | d | k | k | k | d ] _ _ [] //= _. move => _ h. move/negP: (h k); by case. by case: d. - move => _ h. move/negP: (h l); by case. - case : r2 => [ | | | t | d | k | k | k | d ] _ _ [] //= _. move => _ h. move/negP: (h k); by case. by case: d. - case : r2 => [ | | | t | d | k | k | k | d ] hc1 _ [] //=; try (by case:c hc1). move => _ _ h; move/negP : (h k); by case. by case: d; case : c hc1. 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)