proposition: Lemma compare_trans : forall r1 r2 r3 s, compare r1 r2 = s -> compare r2 r3 = s -> compare r1 r3 = s.
proof: Proof. apply (@creg_ind (fun r1 => forall r2 r3 s, compare r1 r2 = s -> compare r2 r3 = s -> compare r1 r3 = s) (fun l1 => forall l2 l3 s, compareList l1 l2 = s -> compareList l2 l3 = s -> compareList l1 l3 = s)) => [ | | | s | c hc | l hl | l hl | l hl | c hc | | hd hc tl htl ] /=. - case => [ | | | s' | c' | l' | l' | l' | c' ] //=; try (case => //=; by move => s'' <-). - case => [ | | | s' | c' | l' | l' | l' | c' ] //=; try (case => //=; by move => s'' <-). - case => [ | | | s' | c' | l' | l' | l' | c' ] //=; try (case => //=; by move => s'' <-). - case => [ | | | s' | c' | l' | l' | l' | c' ] //=; try (case => //; by move => s1 s2 <-). case => //=. by apply cmpS_trans. - case => [ | | | s' | c' | l' | l' | l' | c' ] //=; try (case => //; by move => s1 s2 <-). case => //. by apply: hc. - case => [ | | | s' | c' | l' | l' | l' | c' ] //=; try (case => //; by move => s1 s2 <-). case => //. by apply: hl. - case => [ | | | s' | c' | l' | l' | l' | c' ] //=; try (case => //; by move => s1 s2 <-). case => //. by apply: hl. - case => [ | | | s' | c' | l' | l' | l' | c' ] //=; try (case => //; by move => s1 s2 <-). case => //. by apply: hl. - case => [ | | | s' | c' | l' | l' | l' | c' ] //=; try (case => //; by move => s1 s2 <-). case => //. by apply: hc. - case => [ | hd tl] //=. case => [ | hd' tl'] //=. by move => s <-. - case => [ | hd' tl' ] //=. case => [ | hd'' tl''] //= ; by move => s <-. case => [ | hd'' tl''] //=. move => s. move: (hc hd' hd'' s); clear hc. move: (htl tl' tl'' s); clear htl. case_eq (compare hd hd') => h1 //=. * rewrite (compare_eq_axiom h1). by case_eq (compare hd' hd'') => h2 //=. * case_eq (compare hd' hd'') => h2 //=. rewrite -(compare_eq_axiom h2) h1. by move => _ _ <- _. move => _ h hs _. move: h. rewrite -hs. by move => ->. by move => _ _ <-. * case_eq (compare hd' hd'') => h2 //=. rewrite -(compare_eq_axiom h2) h1. by move => _ _ <- _. by move => _ _ <-. move => _ h hs _. move: h. rewrite -hs. by move => ->. 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)