prove decidability

Katydid/Regex/Language.lean

@@ -106,6 +106,12 @@ theorem null_derives {α: Type} (R: Lang α) (xs: List α):
   unfold null
   simp
 
+theorem validate {α: Type} (R: Lang α) (xs: List α):
+  null (derives R xs) = R xs := by
+  unfold derives
+  unfold null
+  simp
+
 theorem derives_foldl (R: Lang α) (xs: List α):
   (derives R) xs = (List.foldl derive R) xs := by
   revert R

Katydid/Regex/SimpleRegex.lean

@@ -227,5 +227,46 @@ theorem derive_commutes {α: Type} (r: Regex α) (x: α):
     guard_target = denote (derive r x) = Language.derive (denote r) x
     exact ih
 
+def derives (r: Regex α) (xs: List α): Regex α :=
+  (List.foldl derive r) xs
+
+theorem derives_commutes {α: Type} (r: Regex α) (xs: List α):
+  denote (derives r xs) = Language.derives (denote r) xs := by
+  unfold derives
+  rw [Language.derives_foldl]
+  revert r
+  induction xs with
+  | nil =>
+    simp only [foldl_nil]
+    intro h
+    exact True.intro
+  | cons x xs ih =>
+    simp only [foldl_cons]
+    intro r
+    have h := derive_commutes r x
+    have ih' := ih (derive r x)
+    rw [h] at ih'
+    exact ih'
+
+def validate (r: Regex α) (xs: List α): Bool :=
+  null (derives r xs)
+
+theorem validate_commutes {α: Type} (r: Regex α) (xs: List α):
+  (validate r xs = true) = (denote r) xs := by
+  rw [<- Language.validate (denote r) xs]
+  unfold validate
+  rw [<- derives_commutes]
+  rw [<- null_commutes]
+
+-- decidableDenote shows that the derivative algorithm is decidable
 def decidableDenote (r: Regex α): DecidablePred (denote r) := by
-  sorry
+  unfold DecidablePred
+  intro xs
+  rw [<- validate_commutes]
+  cases (validate r xs)
+  · simp only [Bool.false_eq_true]
+    apply Decidable.isFalse
+    simp only [not_false_eq_true]
+  · simp only
+    apply Decidable.isTrue
+    exact True.intro

README.md

@@ -18,7 +18,7 @@ Prove theorems about Symbolic regular expressions as a foundation to build upon.
 
 - [x] Prove correctness of derivative algorithm via a commuting diagram.
 - [ ] Prove correctness of derivative algorithm via a Regex type indexed with Language.
-- [ ] Prove decidability of derivative algorithm.
+- [x] Prove decidability of derivative algorithm.
 - [ ] Prove correctness of simplification rules.
 - [ ] Prove correctness of smart constructors.