proposition: Lemma compare_eq_axiom : forall r1 r2, compare r1 r2 = Eq -> r1 = r2.
proof: Proof. apply (@creg_ind (fun r1 => forall r2, compare r1 r2 = Eq -> r1 = r2) (fun l => forall l', compareList l l' = Eq -> l = l')). - by case => //=. - by elim => //=. - by case => //=. - move => s; elim => //=. move => s0. move/eqP. move/cmpS_eq_axiom. by move => ->. - move => c hc. elim => //. move => c2 hc2 heq. move : heq => /= heq. by rewrite (hc c2). - move => l hl. elim => //. move => l' hl'. by rewrite (hl l'). - move => l hl. elim => //. move => l' hl'. by rewrite (hl l'). - move => l hl. elim => //. move => l' hl'. by rewrite (hl l'). - move => c hc. elim => //. move => c2 hc2 heq. move : heq => /= heq. by rewrite (hc c2). - elim => //=. - move => c hc l hl. elim => //. move => c' l' hl' heq. rewrite (hl l'). rewrite (hc c'). done. move : heq => /=. case (compare c c') => //. move : heq => /=. case (compare c c') => //. 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)