move replace function into its own file

Author: awalterschulze

Validator/Regex.lean

@@ -7,5 +7,6 @@ import Validator.Regex.Num
 import Validator.Regex.Pair
 import Validator.Regex.Regex
 import Validator.Regex.RegexID
+import Validator.Regex.Replace
 import Validator.Regex.Smart
 import Validator.Regex.Symbol

Validator/Regex/Replace.lean

@@ -0,0 +1,142 @@
+import Validator.Regex.Num
+import Validator.Regex.Regex
+import Validator.Regex.RegexID
+
+namespace Symbol
+
+def replace (r: RegexID n) (xs: Vec σ l) (h: n <= l): Regex σ :=
+  match r with
+  | Regex.emptyset => Regex.emptyset
+  | Regex.emptystr => Regex.emptystr
+  | Regex.symbol s => Regex.symbol (Vec.get xs (Fin.mk s.val (by
+      cases s
+      simp only
+      omega
+    )))
+  | Regex.or r1 r2 =>
+    Regex.or (replace r1 xs h) (replace r2 xs h)
+  | Regex.concat r1 r2 =>
+    Regex.concat (replace r1 xs h) (replace r2 xs h)
+  | Regex.star r1 =>
+    Regex.star (replace r1 xs h)
+
+def replaceFrom (r: RegexID n) (xs: Vec σ n): Regex σ :=
+  replace r xs (le_refl n)
+
+def replacesFrom (rs: Vec (RegexID n) l) (xs: Vec σ n): Vec (Regex σ) l :=
+  Vec.map rs (fun r => replaceFrom r xs)
+
+
+theorem replace_cast_both (r: RegexID n) (xs: Vec σ n) (h: n = l):
+  replace r xs (by omega) = replace (RegexID.cast r h) (Vec.cast xs h) (by omega) := by
+  subst h
+  simp only [Vec.cast_rfl]
+  rfl
+
+theorem replaceFrom_cast_both (r: RegexID n) (xs: Vec σ n) (h: n = l):
+  replaceFrom r xs = replaceFrom (RegexID.cast r h) (Vec.cast xs h) := by
+  unfold replaceFrom
+  rw [replace_cast_both]
+
+theorem replace_cast_symbols (r: RegexID n) (xs: Vec σ n) (h: n = l):
+  replace r xs (by omega) = replace r (Vec.cast xs h) (by omega) := by
+  subst h
+  simp only [Vec.cast_rfl]
+
+theorem replace_nil_is_map_id (r: Regex (Fin 0)):
+  replace r Vec.nil (by simp) = Regex.map r id := by
+  induction r with
+  | emptyset =>
+    simp only [replace, Regex.map]
+  | emptystr =>
+    simp only [replace, Regex.map]
+  | symbol s =>
+    nomatch s
+  | or r1 r2 ih1 ih2 =>
+    simp only [replace, Regex.map, Regex.or.injEq]
+    rw [ih1]
+    rw [ih2]
+    apply And.intro rfl rfl
+  | concat r1 r2 ih1 ih2 =>
+    simp only [replace, Regex.map, Regex.concat.injEq]
+    rw [ih1]
+    rw [ih2]
+    apply And.intro rfl rfl
+  | star r1 ih1 =>
+    simp only [replace, Regex.map]
+    rw [ih1]
+
+theorem replace_take (r: RegexID n) (xs: Vec σ (n + l)):
+  replace r (Vec.take n xs) (by omega) = replace r xs (by omega):= by
+  induction r with
+  | emptyset =>
+    simp only [replace]
+  | emptystr =>
+    simp only [replace]
+  | symbol s =>
+    generalize_proofs h1 h2 at *
+    simp only [replace]
+    obtain ⟨s, hs⟩ := s
+    simp only [Regex.symbol.injEq]
+    generalize_proofs h3 h4
+    rw [Vec.take_get]
+    omega
+  | or r1 r2 ih1 ih2 =>
+    simp only [replace, Regex.or.injEq]
+    generalize_proofs h1 h2 at *
+    rw [<- ih1]
+    rw [<- ih2]
+    apply And.intro rfl rfl
+  | concat r1 r2 ih1 ih2 =>
+    simp only [replace, Regex.concat.injEq]
+    generalize_proofs h1 h2 at *
+    rw [<- ih1]
+    rw [<- ih2]
+    apply And.intro rfl rfl
+  | star r1 ih1 =>
+    simp only [replace]
+    generalize_proofs h1 at *
+    rw [<- ih1]
+
+theorem replace_regexid_add (r: RegexID n) (xs: Vec σ (n + l)):
+  replace r xs (by omega) = replace (RegexID.add l r) xs (by omega):= by
+  generalize_proofs h1 h2
+  induction r with
+  | emptyset =>
+    simp only [replace, RegexID.add, Regex.map]
+  | emptystr =>
+    simp only [replace, RegexID.add, Regex.map]
+  | symbol s =>
+    generalize_proofs h1 h2 at *
+    simp only [replace, RegexID.add, Regex.map, Fin.coe_castLE]
+  | or r1 r2 ih1 ih2 =>
+    simp only [replace, RegexID.add, Regex.map, Regex.or.injEq]
+    generalize_proofs h1 h2 at *
+    rw [ih1]
+    rw [ih2]
+    apply And.intro rfl rfl
+  | concat r1 r2 ih1 ih2 =>
+    simp only [replace, RegexID.add, Regex.map, Regex.concat.injEq]
+    generalize_proofs h1 h2 at *
+    rw [ih1]
+    rw [ih2]
+    apply And.intro rfl rfl
+  | star r1 ih1 =>
+    simp only [replace, RegexID.add, Regex.map, Regex.star.injEq]
+    generalize_proofs h1 h2 at *
+    rw [ih1]
+    rfl
+
+theorem replacesFrom_cast_both (rs: Vec (RegexID n) l) (ss: Vec σ n) (h: n = m):
+  replacesFrom rs ss =
+  replacesFrom (RegexID.casts rs h) (Vec.cast ss h) := by
+  subst h
+  simp only [Vec.cast_rfl]
+  simp only [RegexID.casts_rfl]
+
+theorem replacesFrom_cons (rs: Vec (RegexID n) l) (xs: Vec σ n):
+  replacesFrom (Vec.cons r rs) xs
+  = Vec.cons (replaceFrom r xs) (replacesFrom rs xs)
+  := by
+  simp only [replacesFrom]
+  simp only [Vec.map]

Validator/Regex/Symbol.lean

@@ -6,6 +6,7 @@ import Validator.Regex.Num
 import Validator.Regex.Pair
 import Validator.Regex.Regex
 import Validator.Regex.RegexID
+import Validator.Regex.Replace
 
 -- I want to define a map function over a regular expression:
 
@@ -36,25 +37,6 @@ import Validator.Regex.RegexID
 
 namespace Symbol
 
-def replace (r: RegexID n) (xs: Vec σ l) (h: n <= l): Regex σ :=
-  match r with
-  | Regex.emptyset => Regex.emptyset
-  | Regex.emptystr => Regex.emptystr
-  | Regex.symbol s => Regex.symbol (Vec.get xs (Fin.mk s.val (by
-      cases s
-      simp only
-      omega
-    )))
-  | Regex.or r1 r2 =>
-    Regex.or (replace r1 xs h) (replace r2 xs h)
-  | Regex.concat r1 r2 =>
-    Regex.concat (replace r1 xs h) (replace r2 xs h)
-  | Regex.star r1 =>
-    Regex.star (replace r1 xs h)
-
-def replaceFrom (r: RegexID n) (xs: Vec σ n): Regex σ :=
-  replace r xs (le_refl n)
-
 def derive {σ: Type} {α: Type} (Φ: σ -> α -> Bool) (r: Regex σ) (a: α): Regex σ :=
   Regex.Pair.derive
     (replaceFrom
@@ -72,9 +54,6 @@ def derive' {σ: Type} {α: Type} (Φ: σ -> α -> Bool) (r: Regex σ) (a: α):
   let replaced: Regex (σ × Bool) := replaceFrom r' replaces
   Regex.Pair.derive replaced
 
-def replacesFrom (rs: Vec (RegexID n) l) (xs: Vec σ n): Vec (Regex σ) l :=
-  Vec.map rs (fun r => replaceFrom r xs)
-
 def derives {σ: Type} {α: Type} (Φ: σ -> α -> Bool) (rs: Vec (Regex σ) l) (a: α): Vec (Regex σ) l :=
   let (rs', symbols): (Vec (RegexID (Symbol.nums rs)) l × Vec σ (Symbol.nums rs)) := Symbol.extractsFrom rs
   let pred_results: Vec Bool (Symbol.nums rs) := Vec.map symbols (fun s => Φ s a)
@@ -137,106 +116,6 @@ def derive_closure' {σ: Type}
       )
     )
 
-theorem replace_cast_both (r: RegexID n) (xs: Vec σ n) (h: n = l):
-  replace r xs (by omega) = replace (RegexID.cast r h) (Vec.cast xs h) (by omega) := by
-  subst h
-  simp only [Vec.cast_rfl]
-  rfl
-
-theorem replaceFrom_cast_both (r: RegexID n) (xs: Vec σ n) (h: n = l):
-  replaceFrom r xs = replaceFrom (RegexID.cast r h) (Vec.cast xs h) := by
-  unfold replaceFrom
-  rw [replace_cast_both]
-
-theorem replace_cast_symbols (r: RegexID n) (xs: Vec σ n) (h: n = l):
-  replace r xs (by omega) = replace r (Vec.cast xs h) (by omega) := by
-  subst h
-  simp only [Vec.cast_rfl]
-
-theorem replace_nil_is_map_id (r: Regex (Fin 0)):
-  replace r Vec.nil (by simp) = Regex.map r id := by
-  induction r with
-  | emptyset =>
-    simp only [replace, Regex.map]
-  | emptystr =>
-    simp only [replace, Regex.map]
-  | symbol s =>
-    nomatch s
-  | or r1 r2 ih1 ih2 =>
-    simp only [replace, Regex.map, Regex.or.injEq]
-    rw [ih1]
-    rw [ih2]
-    apply And.intro rfl rfl
-  | concat r1 r2 ih1 ih2 =>
-    simp only [replace, Regex.map, Regex.concat.injEq]
-    rw [ih1]
-    rw [ih2]
-    apply And.intro rfl rfl
-  | star r1 ih1 =>
-    simp only [replace, Regex.map]
-    rw [ih1]
-
-theorem replace_take (r: RegexID n) (xs: Vec σ (n + l)):
-  replace r (Vec.take n xs) (by omega) = replace r xs (by omega):= by
-  induction r with
-  | emptyset =>
-    simp only [replace]
-  | emptystr =>
-    simp only [replace]
-  | symbol s =>
-    generalize_proofs h1 h2 at *
-    simp only [replace]
-    obtain ⟨s, hs⟩ := s
-    simp only [Regex.symbol.injEq]
-    generalize_proofs h3 h4
-    rw [Vec.take_get]
-    omega
-  | or r1 r2 ih1 ih2 =>
-    simp only [replace, Regex.or.injEq]
-    generalize_proofs h1 h2 at *
-    rw [<- ih1]
-    rw [<- ih2]
-    apply And.intro rfl rfl
-  | concat r1 r2 ih1 ih2 =>
-    simp only [replace, Regex.concat.injEq]
-    generalize_proofs h1 h2 at *
-    rw [<- ih1]
-    rw [<- ih2]
-    apply And.intro rfl rfl
-  | star r1 ih1 =>
-    simp only [replace]
-    generalize_proofs h1 at *
-    rw [<- ih1]
-
-theorem replace_regexid_add (r: RegexID n) (xs: Vec σ (n + l)):
-  replace r xs (by omega) = replace (RegexID.add l r) xs (by omega):= by
-  generalize_proofs h1 h2
-  induction r with
-  | emptyset =>
-    simp only [replace, RegexID.add, Regex.map]
-  | emptystr =>
-    simp only [replace, RegexID.add, Regex.map]
-  | symbol s =>
-    generalize_proofs h1 h2 at *
-    simp only [replace, RegexID.add, Regex.map, Fin.coe_castLE]
-  | or r1 r2 ih1 ih2 =>
-    simp only [replace, RegexID.add, Regex.map, Regex.or.injEq]
-    generalize_proofs h1 h2 at *
-    rw [ih1]
-    rw [ih2]
-    apply And.intro rfl rfl
-  | concat r1 r2 ih1 ih2 =>
-    simp only [replace, RegexID.add, Regex.map, Regex.concat.injEq]
-    generalize_proofs h1 h2 at *
-    rw [ih1]
-    rw [ih2]
-    apply And.intro rfl rfl
-  | star r1 ih1 =>
-    simp only [replace, RegexID.add, Regex.map, Regex.star.injEq]
-    generalize_proofs h1 h2 at *
-    rw [ih1]
-    rfl
-
 theorem extract_replaceFrom_is_id (r: Regex σ) (acc: Vec σ l):
   r = replaceFrom (extract r acc).1 (extract r acc).2 := by
   simp only [replaceFrom]
@@ -455,20 +334,6 @@ theorem Symbol_derive_is_Regex_derive
   rw [<- extractFrom_replaceFrom_is_fmap]
   rw [Regex.Pair.derive_is_pair_derive]
 
-theorem replacesFrom_cast_both (rs: Vec (RegexID n) l) (ss: Vec σ n) (h: n = m):
-  replacesFrom rs ss =
-  replacesFrom (RegexID.casts rs h) (Vec.cast ss h) := by
-  subst h
-  simp only [Vec.cast_rfl]
-  simp only [RegexID.casts_rfl]
-
-theorem replacesFrom_cons (rs: Vec (RegexID n) l) (xs: Vec σ n):
-  replacesFrom (Vec.cons r rs) xs
-  = Vec.cons (replaceFrom r xs) (replacesFrom rs xs)
-  := by
-  simp only [replacesFrom]
-  simp only [Vec.map]
-
 theorem replaceFrom_append {r: Regex α} {xs: Vec α (n + Symbol.num r)} {acc: Vec α n} {ys: Vec α m}:
   replaceFrom (RegexID.add m (extract r acc).1) (Vec.append xs ys)
   = replaceFrom (extract r acc).1 xs := by