fact: Fixpoint ssubl (r1: regexp) {struct r1} : regexp -> bool := match r1 with | Void => fun r2 => true | Eps =>(fix ssubl' r2 := match r2 with | Eps => true | Plus e' f' => ssubl' e' || ssubl' f' | _ => false end ) | Dot =>(fix ssubl' r2 := match r2 with | Dot => true | Plus e' f' => ssubl' e' || ssubl' f' | _ => false end ) | Atom p =>(fix ssubl' r2 := match r2 with | Atom q => p == q | Plus e' f' => ssubl' e' || ssubl' f' | _ => false end ) | Plus e f => fun r2 => ssubl e r2 && ssubl f r2 | Conc e f => (fix ssubl' r2 := match r2 with | Conc e' f' => ssubl e e' && ssubl f f' | Plus e' f' => ssubl' e' || ssubl' f' | _ => false end ) | Star e => (fix ssubl' r2 := match r2 with | Star f => ssubl e f | Plus e' f' => ssubl' e' || ssubl' f' | _ => false end ) | And e f => (fix ssubl' r2 := match r2 with | And e' f' => ssubl e e' && ssubl f f' | Plus e' f' => ssubl' e' || ssubl' f' | _ => false end ) | Not r1 => (fix ssubl' r2 := match r2 with | Not r2 => ssubr r1 r2 | Plus e' f' => ssubl' e' || ssubl' f' | _ => false end) end with ssubr (r1 : regexp) : regexp -> bool := match r1 with | Void => (fix ssub' r2 := match r2 with | Void => true | Plus e' f' => ssub' e' && ssub' f' | _ => false end ) | Eps =>(fix ssub' r2 := match r2 with | Void => true | Eps => true | Plus e' f' => ssub' e' && ssub' f' | _ => false end ) | Dot =>(fix ssub' r2 := match r2 with | Void => true | Dot => true | Plus e' f' => ssub' e' && ssub' f' | _ => false end ) | Atom p =>(fix ssub' r2 := match r2 with | Void => true | Atom q => p == q | Plus e' f' => ssub' e' && ssub' f' | _ => false end ) | Plus e f => (fix ssub' r2 := match r2 with | Plus e' f' => ssub' e' && ssub' f' | _ => ssubr e r2 || ssubr f r2 end ) | Conc e f => (fix ssub' r2 := match r2 with | Void => true | Conc e' f' => ssubr e e' && ssubr f f' | Plus e' f' => ssub' e' && ssub' f' | _ => false end ) | Star e => (fix ssub' r2 := match r2 with | Void => true | Star f => ssubr e f | Plus e' f' => ssub' e' && ssub' f' | _ => false end ) | And e f => (fix ssub' r2 := match r2 with | Void => true | And e' f' => ssubr e e' && ssubr f f' | Plus e' f' => ssub' e' && ssub' f' | _ => false end ) | Not r1 => (fix ssub' r2 := match r2 with | Void => true | Not r2 => ssubl r1 r2 | Plus e' f' => ssub' e' && ssub' f' | _ => false end ) end.
imports: Coq(RelationClasses Setoid Morphisms Permutation) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegLang(languages) RegexpBrzozowski(regexp finite_der equiv)