introduce any predicate in Language and proof that or (star any) is universal

Author: awalterschulze

Katydid/Regex/Language.lean

@@ -23,6 +23,9 @@ def char {α: Type} (x : α): Lang α :=
 def pred {α: Type} (p : α -> Prop): Lang α :=
   fun xs => ∃ x, xs = [x] /\ p x
 
+def any {α: Type}: Lang α :=
+  fun xs => ∃ x, xs = [x]
+
 -- onlyif is used as an and to make derive char not require an if statement
 -- (derive (char c) a) w <-> (onlyif (a = c) emptystr)
 def onlyif {α: Type} (cond : Prop) (R : Lang α) : Lang α :=
@@ -924,3 +927,23 @@ theorem simp_star_emptyset_is_emptystr {α: Type}:
     intro h
     rw [h]
     exact star.zero
+
+theorem simp_star_any_is_universal {α: Type}:
+  star (@any α) = @universal α := by
+  funext xs
+  simp only [universal, eq_iff_iff]
+  apply Iff.intro
+  case mp =>
+    intro h
+    exact True.intro
+  case mpr =>
+    intro h
+    induction xs with
+    | nil =>
+      exact star.zero
+    | cons x xs ih =>
+      apply star.more x [] xs
+      · simp only [singleton_append]
+      · unfold any
+        exists x
+      · exact ih

Katydid/Regex/SmartRegex.lean

@@ -346,6 +346,36 @@ theorem orToList_is_orFromList (x: Regex α):
     rw [orFromList_cons_NonEmptyList_is_or]
     rw [ih2]
 
+theorem simp_pred_any_is_any:
+  denote (Regex.pred (@Predicate.mkAny α o)) = Language.any := by
+  unfold denote
+  unfold Predicate.mkAny
+  unfold Predicate.func
+  simp only
+  unfold mkAnyPredFunc
+  unfold Language.pred
+  unfold Language.any
+  funext xs
+  simp only [and_true]
+
+theorem simp_star_pred_any_is_universal [o: Ord α]:
+  denote (Regex.star (Regex.pred (@Predicate.mkAny α o))) = Language.universal := by
+  unfold denote
+  rw [simp_pred_any_is_any]
+  exact Language.simp_star_any_is_universal
+
+theorem simp_or_universal_r_is_universal [Ord α] (x: Regex α):
+  denote (Regex.or x (Regex.star (Regex.pred Predicate.mkAny))) = Language.universal := by
+  nth_rewrite 1 [denote]
+  rw [simp_star_pred_any_is_universal]
+  rw [Language.simp_or_universal_r_is_universal]
+
+theorem simp_or_universal_l_is_universal [Ord α] (x: Regex α):
+  denote (Regex.or (Regex.star (Regex.pred Predicate.mkAny)) x) = Language.universal := by
+  nth_rewrite 1 [denote]
+  rw [simp_star_pred_any_is_universal]
+  rw [Language.simp_or_universal_l_is_universal]
+
 -- 1. If x or y is emptyset then return the other (Language.simp_or_emptyset_r_is_l and Language.simp_or_emptyset_l_is_r)
 -- 2. If x or y is star (any) then return star (any) (Language.simp_or_universal_r_is_universal and Language.simp_or_universal_l_is_universal)
 -- 3. Get the lists of ors using orToList (Language.simp_or_assoc)