regex closure commutes

Author: awalterschulze

Validator/Regex/Closure.lean

@@ -37,23 +37,12 @@ theorem derive_is_closure_derive (Φ: σ -> α -> Bool) (r: Regex σ) (a: α):
     simp only [Regex.derive, Regex.Closure.derive]
     rw [ih1]
 
-theorem closure_derive_is_derive (Φ: σ -> Bool) (r: Regex σ) (a: α):
-  Regex.Closure.derive Φ r = Regex.derive (fun s _ => Φ s) r a := by
-  induction r with
-  | emptyset =>
-    simp only [Regex.derive, Regex.Closure.derive]
-  | emptystr =>
-    simp only [Regex.derive, Regex.Closure.derive]
-  | symbol s =>
-    simp only [Regex.derive, Regex.Closure.derive]
-  | or r1 r2 ih1 ih2 =>
-    simp only [Regex.derive, Regex.Closure.derive]
-    rw [ih1]
-    rw [ih2]
-  | concat r1 r2 ih1 ih2 =>
-    simp only [Regex.derive, Regex.Closure.derive]
-    rw [ih1]
-    rw [ih2]
-  | star r1 ih1 =>
-    simp only [Regex.derive, Regex.Closure.derive]
-    rw [ih1]
+theorem derive_commutesb {σ: Type} {α: Type} (Φ: σ -> α -> Bool) (r: Regex σ) (a: α):
+  denote (fun s a => Φ s a) (Regex.Closure.derive (fun s => Φ s a) r) = Language.derive (denote (fun s a => Φ s a) r) a := by
+  rw [<- derive_is_closure_derive]
+  rw [<- Regex.derive_commutesb]
+
+theorem derive_commutesb' {σ: Type} {α: Type} (Φ: σ -> α -> Bool) (r: Regex σ) (a: α):
+  denote (fun s a => Φ s a) (Regex.Closure.derive (fun s => Φ s a) r) = Language.derive (denote (fun s a => Φ s a) r) a := by
+  rw [<- derive_is_closure_derive]
+  rw [<- Regex.derive_commutesb]

Validator/Regex/Regex.lean

@@ -12,15 +12,15 @@ inductive Regex (σ: Type) where
   | star (p: Regex σ)
   deriving DecidableEq, Ord, Repr, Hashable
 
-instance [Ord α]: Ord (Regex α) := inferInstance
+instance [Ord σ]: Ord (Regex σ) := inferInstance
 
-instance [Repr α]: Repr (Regex α) := inferInstance
+instance [Repr σ]: Repr (Regex σ) := inferInstance
 
-instance [DecidableEq α]: DecidableEq (Regex α) := inferInstance
+instance [DecidableEq σ]: DecidableEq (Regex σ) := inferInstance
 
-instance [DecidableEq α]: BEq (Regex α) := inferInstance
+instance [DecidableEq σ]: BEq (Regex σ) := inferInstance
 
-instance [Hashable α]: Hashable (Regex α) := inferInstance
+instance [Hashable σ]: Hashable (Regex σ) := inferInstance
 
 namespace Regex
 
@@ -200,3 +200,10 @@ theorem derive_commutes {σ: Type} {α: Type} (Φ: σ -> α -> Prop) [DecidableR
     congrm ((Language.concat_n ?_ (Language.star_n (denote Φ r))))
     guard_target = denote Φ (derive (fun s a => Φ s a) r x) = Language.derive (denote Φ r) x
     exact ih
+
+theorem derive_commutesb {σ: Type} {α: Type} (Φ: σ -> α -> Bool) (r: Regex σ) (x: α):
+  denote (fun s a => Φ s a) (derive (fun s a => Φ s a) r x) = Language.derive (denote (fun s a => Φ s a) r) x := by
+  rw [<- derive_commutes]
+  congr
+  funext s a
+  simp only [Bool.decide_eq_true]