fact: Fixpoint compare r1 r2 {struct r1} : comparison := let fix compareList l1 l2 {struct l1} : comparison := match l1,l2 with | [::], [::] => Eq | [::], _ => Lt | _, [::] => Gt | a1 :: t1, a2 :: t2 => match compare a1 a2 with | Eq => compareList t1 t2 | o => o end end in match r1,r2 with | CEps, CEps => Eq | CEps, _ => Lt | _, CEps => Gt | CDot, CDot => Eq | CDot, _ => Lt | _, CDot => Gt | CVoid, CVoid => Eq | CVoid, _ => Lt | _, CVoid => Gt | CAtom a, CAtom b => cmpS a b | CAtom a, _ => Lt | _, CAtom b => Gt | CConc l1, CConc l2 => compareList l1 l2 | CConc _, _ => Lt | _, CConc _ => Gt | CStar r1, CStar r2 => compare r1 r2 | CStar _, _=> Lt | _, CStar _ => Gt | CPlus l1, CPlus l2 => compareList l1 l2 | CPlus _, _ => Lt | _, CPlus _ => Gt | CAnd l1, CAnd l2 => compareList l1 l2 | CAnd _, _ => Lt | _, CAnd _ => Gt | CNot a, CNot b => compare a b end.
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)