fact: Fixpoint regexp_struct_eq (e1 e2: regular_expression) : bool := match e1,e2 with | Void, Void => true | Eps, Eps => true | Dot, Dot => true | Atom n, Atom p => n == p | Star e1, Star e2 => regexp_struct_eq e1 e2 | Plus e1 e2, Plus f1 f2 => regexp_struct_eq e1 f1 && regexp_struct_eq e2 f2 | And e1 e2, And f1 f2 => regexp_struct_eq e1 f1 && regexp_struct_eq e2 f2 | Conc e1 e2, Conc f1 f2 => regexp_struct_eq e1 f1 && regexp_struct_eq e2 f2 | Not e1, Not e2 => regexp_struct_eq e1 e2 | _, _ => false end.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegLang(languages) RegexpBrzozowski(glue)