Use sentinel value instead of Option.none (#145)

* Use sentinel value instead of Option.none

* Fix test setup

Author: pandaman64

correctness/RegexCorrectness/Backtracker/Refinement.lean

@@ -6,7 +6,7 @@ set_option autoImplicit false
 open Regex (NFA)
 open Regex.Data (BitMatrix BVPos)
 open Regex.Strategy (materializeUpdates)
-open String (ValidPos)
+open String (ValidPos ValidPosPlusOne)
 namespace Regex.Backtracker
 
 variable {s : String} {nfa : NFA} {wf : nfa.WellFormed} {startPos : ValidPos s} {bufferSize : Nat}

correctness/RegexCorrectness/Regex/Basic.lean

@@ -94,8 +94,8 @@ theorem captureNextBuf_soundness (h : re.captureNextBuf bufferSize pos = .some m
     pos ≤ pos' ∧
     s.expr.Captures pos' pos'' groups ∧
     EquivMaterializedUpdate (materializeRegexGroups groups) matched ∧
-    matched[0] = .some pos' ∧
-    matched[1] = .some pos'' := by
+    matched[0] = .validPos pos' ∧
+    matched[1] = .validPos pos'' := by
   have ⟨pos', pos'', groups, le, c, eqv⟩ := captureNextBuf_soundness' h s
   refine ⟨pos', pos'', groups, le, c, eqv, ?_⟩
 

correctness/RegexCorrectness/Regex/Captures.lean

@@ -68,7 +68,7 @@ theorem captures_of_next?_some (h : self.next? = .some (captured, self')) (isr :
         . intro index p₁ p₂ le
           have hbufsize : captured.buffer.size = self.regex.maxTag + 1 := by grind
           if lt : 2 * index + 1 < self.regex.maxTag + 1 then
-            simp [eqv.eq index lt p₁ p₂, ←h.1, CapturedGroups.get, Option.bind_eq_some_iff, le]
+            simp [eqv.eq index lt p₁ p₂, CapturedGroups.get, ←h.1, Option.bind_eq_some_iff]
             grind
           else
             have : self.regex.maxTag ≤ 2 * index := by grind

correctness/RegexCorrectness/Strategy/Materialize/Basic.lean

@@ -3,7 +3,7 @@ import RegexCorrectness.Data.Expr.Semantics.CaptureGroups
 set_option autoImplicit false
 
 open Regex.Data (CaptureGroups)
-open String (ValidPos)
+open String (ValidPos ValidPosPlusOne)
 
 namespace Regex.Strategy
 
@@ -24,27 +24,59 @@ def materializeRegexGroups : CaptureGroups s → Nat → Option (ValidPos s × V
     -- The later one will be preferred
     materializeRegexGroups g₂ tag <|> materializeRegexGroups g₁ tag
 
-def materializeUpdatesAux (n : Nat) (accum : Vector (Option (ValidPos s)) n) : List (Nat × ValidPos s) → Vector (Option (ValidPos s)) n
+def materializeUpdatesAux (n : Nat) (accum : Vector (ValidPosPlusOne s) n) : List (Nat × ValidPos s) → Vector (ValidPosPlusOne s) n
   | [] => accum
   | (offset, pos) :: rest =>
-    materializeUpdatesAux n (accum.setIfInBounds offset (some pos)) rest
+    materializeUpdatesAux n (accum.setIfInBounds offset (.validPos pos)) rest
 
 /--
 `materializeUpdates n updates` constructs a buffer of size `n` which interprets the updates list
 as the writes to the buffer. When the same offset appears multiple times in the list, the last
 one wins.
 -/
-def materializeUpdates (n : Nat) (updates : List (Nat × ValidPos s)) : Vector (Option (ValidPos s)) n :=
-  materializeUpdatesAux n (Vector.replicate n .none) updates
+def materializeUpdates (n : Nat) (updates : List (Nat × ValidPos s)) : Vector (ValidPosPlusOne s) n :=
+  materializeUpdatesAux n (Vector.replicate n (.sentinel s)) updates
 
-def EquivMaterializedUpdate {n} (groups : Nat → Option (ValidPos s × ValidPos s)) (updates : Vector (Option (ValidPos s)) n) : Prop :=
+def equivPos {s} (p : Option (ValidPos s)) (p' : ValidPosPlusOne s) : Prop :=
+  match p with
+  | .some p => p' = .validPos p
+  | .none => p' = .sentinel s
+
+@[simp, grind =]
+theorem equivPos.some_iff {p : ValidPos s} {p' : ValidPosPlusOne s} : equivPos (.some p) p' ↔ p' = .validPos p := by
+  grind [equivPos]
+
+@[simp, grind =]
+theorem equivPos.none_iff {p' : ValidPosPlusOne s} : equivPos .none p' ↔ p' = .sentinel s := by
+  grind [equivPos]
+
+@[simp, grind =]
+theorem equivPos.validPos_iff {p p' : ValidPos s} : equivPos p (.validPos p') ↔ p = p' := by
+  grind [equivPos]
+
+@[simp, grind =]
+theorem equivPos.sentinel_iff {p} : equivPos p (.sentinel s) ↔ p = .none := by
+  match p with
+  | .some p => simpa using ValidPosPlusOne.validPos_ne_sentinel.symm
+  | .none => simp
+
+def EquivMaterializedUpdate {n} (groups : Nat → Option (ValidPos s × ValidPos s)) (updates : Vector (ValidPosPlusOne s) n) : Prop :=
   ∀ tag,
-    ((h₁ : 2 * tag < n) → ((groups tag).map (·.1) = updates[2 * tag])) ∧
-    ((h₂ : 2 * tag + 1 < n) → ((groups tag).map (·.2) = updates[2 * tag + 1]))
+    ((h₁ : 2 * tag < n) → (equivPos ((groups tag).map (·.1)) updates[2 * tag])) ∧
+    ((h₂ : 2 * tag + 1 < n) → (equivPos ((groups tag).map (·.2)) updates[2 * tag + 1]))
+
+theorem EquivMaterializedUpdate.eq {n} {groups : Nat → Option (ValidPos s × ValidPos s)} {updates : Vector (ValidPosPlusOne s) n}
+  (eqv : EquivMaterializedUpdate groups updates) (tag : Nat) (lt : 2 * tag + 1 < n) (p₁ p₂ : ValidPos s) :
+  groups tag = .some (p₁, p₂) ↔ updates[2 * tag] = .validPos p₁ ∧ updates[2 * tag + 1] = .validPos p₂ := by
+  have eq₁ := (eqv tag).1 (by grind)
+  have eq₂ := (eqv tag).2 lt
+  match h : groups tag with
+  | .some (p₁', p₂') => grind
+  | .none => grind
 
-theorem EquivMaterializedUpdate.eq {n} {groups : Nat → Option (ValidPos s × ValidPos s)} {updates : Vector (Option (ValidPos s)) n}
+theorem EquivMaterializedUpdate.eq_none {n} {groups : Nat → Option (ValidPos s × ValidPos s)} {updates : Vector (ValidPosPlusOne s) n}
   (eqv : EquivMaterializedUpdate groups updates) (tag : Nat) (lt : 2 * tag + 1 < n) (p₁ p₂ : ValidPos s) :
-  groups tag = .some (p₁, p₂) ↔ updates[2 * tag] = .some p₁ ∧ updates[2 * tag + 1] = .some p₂ := by
+  groups tag = .none ↔ updates[2 * tag] = .sentinel s ∧ updates[2 * tag + 1] = .sentinel s := by
   have eq₁ := (eqv tag).1 (by grind)
   have eq₂ := (eqv tag).2 lt
   match h : groups tag with

correctness/RegexCorrectness/Strategy/Materialize/Lemmas.lean

@@ -4,7 +4,7 @@ import RegexCorrectness.Data.Expr.Semantics
 
 set_option autoImplicit false
 
-open String (ValidPos)
+open String (ValidPos ValidPosPlusOne)
 open Regex.Data (CaptureGroups)
 
 namespace Regex.Strategy
@@ -61,12 +61,12 @@ theorem mem_tags_of_materializeRegexGroups_some {e : Expr} {pos pos' : ValidPos
 @[simp]
 theorem materializeUpdatesAux_snoc {n accum updates offset} {pos : ValidPos s} :
   materializeUpdatesAux n accum (updates ++ [(offset, pos)]) =
-  (materializeUpdatesAux n accum updates).setIfInBounds offset (some pos) := by
+  (materializeUpdatesAux n accum updates).setIfInBounds offset (.validPos pos) := by
   induction updates generalizing accum with
   | nil => simp [materializeUpdatesAux]
   | cons _ _ ih => simp [materializeUpdatesAux, ih]
 
-theorem materializeUpdatesAux_swap {n : Nat} {accum : Vector (Option (ValidPos s)) n} {updates : List (Nat × ValidPos s)} {offset₁ pos₁ offset₂ pos₂}
+theorem materializeUpdatesAux_swap {n : Nat} {accum : Vector (ValidPosPlusOne s) n} {updates : List (Nat × ValidPos s)} {offset₁ pos₁ offset₂ pos₂}
   (ne : offset₁ ≠ offset₂) :
   materializeUpdatesAux n accum ((offset₁, pos₁) :: (offset₂, pos₂) :: updates) =
   materializeUpdatesAux n accum ((offset₂, pos₂) :: (offset₁, pos₁) :: updates) := by
@@ -86,7 +86,7 @@ theorem materializeUpdatesAux_swap {n : Nat} {accum : Vector (Option (ValidPos s
 theorem materializeUpdatesAux_cons_of_not_in {n accum updates offset} {pos : ValidPos s}
   (h : ∀ offset' pos', (offset', pos') ∈ updates → offset ≠ offset') :
   materializeUpdatesAux n accum ((offset, pos) :: updates) =
-  (materializeUpdatesAux n accum updates).setIfInBounds offset (some pos) := by
+  (materializeUpdatesAux n accum updates).setIfInBounds offset (.validPos pos) := by
   induction updates generalizing accum with
   | nil => simp [materializeUpdatesAux]
   | cons head updates ih =>
@@ -102,44 +102,29 @@ theorem materializeUpdatesAux_cons_of_not_in {n accum updates offset} {pos : Val
     rfl
 
 @[simp]
-theorem materializeUpdatesAux_nil {n : Nat} {accum : Vector (Option (ValidPos s)) n} :
+theorem materializeUpdatesAux_nil {n : Nat} {accum : Vector (ValidPosPlusOne s) n} :
   materializeUpdatesAux n accum [] = accum := rfl
 
-theorem materializeUpdatesAux_append {n : Nat} {accum : Vector (Option (ValidPos s)) n} {updates₁ updates₂ : List (Nat × ValidPos s)} :
+theorem materializeUpdatesAux_append {n : Nat} {accum : Vector (ValidPosPlusOne s) n} {updates₁ updates₂ : List (Nat × ValidPos s)} :
   materializeUpdatesAux n accum (updates₁ ++ updates₂) = materializeUpdatesAux n (materializeUpdatesAux n accum updates₁) updates₂ := by
   induction updates₁ generalizing accum with
   | nil => simp
   | cons head tail ih => simp [materializeUpdatesAux, ih]
 
-theorem materializeUpdatesAux_getElem {n : Nat} {accum : Vector (Option (ValidPos s)) n} {updates : List (Nat × ValidPos s)} {offset : Nat} (h : offset < n) :
+theorem materializeUpdatesAux_getElem {n : Nat} {accum : Vector (ValidPosPlusOne s) n} {updates : List (Nat × ValidPos s)} {offset : Nat} (h : offset < n) :
   (materializeUpdatesAux n accum updates)[offset] =
-  ((materializeUpdatesAux n (Vector.replicate n .none) updates)[offset] <|> accum[offset]) := by
+  ((materializeUpdatesAux n (Vector.replicate n (.sentinel s)) updates)[offset] <|> accum[offset]) := by
   induction updates generalizing accum with
   | nil => simp
-  | cons head updates ih =>
-    simp [materializeUpdatesAux]
-    conv =>
-      lhs
-      rw [ih]
-    conv =>
-      rhs
-      rw [ih]
-    cases (materializeUpdatesAux n (Vector.replicate n .none) updates)[offset] with
-    | some _ => simp
-    | none =>
-      simp
-      if h' : head.1 = offset then
-        simp [h']
-      else
-        simp [h']
+  | cons head updates ih => grind [materializeUpdatesAux]
 
 @[simp]
-theorem materializeUpdates_empty {n} : @materializeUpdates s n [] = Vector.replicate n .none := rfl
+theorem materializeUpdates_empty {n} : @materializeUpdates s n [] = Vector.replicate n (.sentinel s) := rfl
 
 @[simp]
 theorem materializeUpdates_snoc {n : Nat} {updates : List (Nat × ValidPos s)} {offset : Nat} {pos : ValidPos s} :
   materializeUpdates n (updates ++ [(offset, pos)]) =
-  (materializeUpdates n updates).setIfInBounds offset (some pos) := by
+  (materializeUpdates n updates).setIfInBounds offset (.validPos pos) := by
   simp [materializeUpdates]
 
 theorem materializeUpdates_append_getElem {n : Nat} {updates₁ updates₂ : List (Nat × ValidPos s)} {offset : Nat} (h : offset < n) :

correctness/RegexCorrectness/Strategy/Materialize/Naturality.lean

@@ -6,7 +6,7 @@ set_option autoImplicit false
 
 open Regex.Data (Expr CaptureGroups)
 open Regex.Strategy
-open String (ValidPos)
+open String (ValidPos ValidPosPlusOne)
 
 namespace Regex.NFA
 
@@ -97,8 +97,7 @@ where
       match h : materializeRegexGroups g₂ tag with
       | .some (first, last) =>
         have := (eqv₂ tag).1 h₁
-        simp [h] at this
-        simp [←this]
+        grind
       | .none =>
         have := (eqv₂ tag).1 h₁
         simp [h] at this
@@ -108,8 +107,7 @@ where
       match h : materializeRegexGroups g₂ tag with
       | .some (first, last) =>
         have := (eqv₂ tag).2 h₂
-        simp [h] at this
-        simp [←this]
+        grind
       | .none =>
         have := (eqv₂ tag).2 h₂
         simp [h] at this

regex/Regex/Data/String.lean

@@ -209,7 +209,7 @@ def validPos (p : ValidPos s) : ValidPosPlusOne s :=
 def sentinel (s : String) : ValidPosPlusOne s :=
   ⟨s.rawEndPos.offsetBy ⟨1⟩, .inr rfl⟩
 
-@[elab_as_elim]
+@[elab_as_elim, cases_eliminator]
 def rec'.{u} {motive : ValidPosPlusOne s → Sort u}
   (validPos : (p : ValidPos s) → motive (validPos p))
   (sentinel : motive (sentinel s))
@@ -231,6 +231,7 @@ instance : Inhabited (ValidPosPlusOne s) := ⟨.validPos s.startValidPos⟩
 def isValid (p : ValidPosPlusOne s) : Bool :=
   p.offset ≠ s.rawEndPos.offsetBy ⟨1⟩
 
+@[grind _=_]
 theorem isValid_iff_isValid (p : ValidPosPlusOne s) : p.isValid ↔ p.offset.IsValid s := by
   cases p.isValidOrPlusOne with
   | inl h =>
@@ -295,6 +296,105 @@ instance : WellFoundedRelation (ValidPosPlusOne s) where
   rel p q := q < p
   wf := wellFounded_gt
 
+def le (p₁ p₂ : ValidPosPlusOne s) : Prop :=
+  p₁.offset ≤ p₂.offset
+
+instance : LE (ValidPosPlusOne s) := ⟨le⟩
+
+@[grind =]
+theorem le_iff {p₁ p₂ : ValidPosPlusOne s} : p₁ ≤ p₂ ↔ p₁.offset ≤ p₂.offset :=
+  Iff.rfl
+
+@[simp, grind =]
+theorem validPos_le_validPos_iff {p₁ p₂ : ValidPos s} : ValidPosPlusOne.validPos p₁ ≤ ValidPosPlusOne.validPos p₂ ↔ p₁ ≤ p₂ :=
+  Iff.rfl
+
+instance {s : String} (p₁ p₂ : ValidPosPlusOne s) : Decidable (p₁ ≤ p₂) :=
+  decidable_of_iff' _ le_iff
+
+theorem isValid_of_isValid_of_le {p₁ p₂ : ValidPosPlusOne s} (h : p₂.isValid) (le : p₁ ≤ p₂) : p₁.isValid := by
+  cases p₁.isValidOrPlusOne with
+  | inl h₁ => simpa [p₁.isValid_iff_isValid] using h₁
+  | inr h₁ =>
+    rw [p₂.isValid_iff_isValid] at h
+    have le' : p₂.offset ≤ s.rawEndPos := h.le_rawEndPos
+    have le'' : s.rawEndPos.offsetBy ⟨1⟩ ≤ s.rawEndPos := h₁ ▸ Pos.Raw.le_trans le le'
+    simp [Pos.Raw.le_iff] at le''
+    grind
+
+@[grind .]
+theorem validPos_inj {p₁ p₂ : ValidPos s} (h : ValidPosPlusOne.validPos p₁ = ValidPosPlusOne.validPos p₂) : p₁ = p₂ := by
+  simp only [validPos, ValidPosPlusOne.mk.injEq] at h
+  exact ValidPos.ext h
+
+def or (p₁ p₂ : ValidPosPlusOne s) : ValidPosPlusOne s :=
+  if p₁.isValid then
+    p₁
+  else
+    p₂
+
+def orElse (p₁ : ValidPosPlusOne s) (p₂ : Unit → ValidPosPlusOne s) : ValidPosPlusOne s :=
+  if p₁.isValid then
+    p₁
+  else
+    p₂ ()
+
+instance : OrElse (ValidPosPlusOne s) := ⟨orElse⟩
+
+@[simp, grind =]
+theorem orElse_eq_or {p₁ : ValidPosPlusOne s} {p₂} : p₁.orElse p₂ = p₁.or (p₂ ()) := by
+  grind [orElse, or]
+
+@[simp, grind =]
+theorem hOrElse_eq_orElse {p₁ : ValidPosPlusOne s} {p₂} : HOrElse.hOrElse p₁ p₂ = p₁.orElse p₂ := rfl
+
+@[simp, grind =]
+theorem or_valid {p₁ p₂ : ValidPosPlusOne s} (h : p₁.isValid) : p₁.or p₂ = p₁ := by
+  simp [or, h]
+
+@[simp, grind =]
+theorem or_not_valid {p₁ p₂ : ValidPosPlusOne s} (h : ¬p₁.isValid) : p₁.or p₂ = p₂ := by
+  simp [or, h]
+
+@[simp, grind =]
+theorem isValid_validPos {p : ValidPos s} : (ValidPosPlusOne.validPos p).isValid = true :=
+  (isValid_iff_isValid (.validPos p)).mpr p.isValid
+
+@[simp, grind =]
+theorem not_isValid_sentinel {s : String} : (ValidPosPlusOne.sentinel s).isValid = false := by
+  simp [sentinel, isValid]
+@[simp, grind =]
+theorem sentinel_or {p₁ p₂ : ValidPosPlusOne s} (h : p₁ = .sentinel s) : p₁.or p₂ = p₂ := by
+  grind
+
+@[simp, grind =>]
+theorem validPos_or {p₁ p₂ : ValidPosPlusOne s} (h : p₁ = .validPos p) : p₁.or p₂ = p₁ := by
+  grind
+
+@[simp, grind =]
+theorem or_sentinel {p₁ p₂ : ValidPosPlusOne s} (h : p₂ = .sentinel s) : p₁.or p₂ = p₁ := by
+  cases p₁ with
+  | validPos p => simp
+  | sentinel => simp [h]
+
+@[grind .]
+theorem validPos_ne_sentinel {p : ValidPos s} : ValidPosPlusOne.validPos p ≠ ValidPosPlusOne.sentinel s := by
+  intro eq
+  have : isValid (.validPos p) = isValid (.sentinel s) := by grind
+  simp at this
+
+@[simp, grind =]
+theorem or_self {p : ValidPosPlusOne s} : p.or p = p := by
+  cases p with
+  | validPos p => simp
+  | sentinel => simp
+
+@[simp, grind =]
+theorem asValidPos_validPos {p : ValidPos s} : (ValidPosPlusOne.validPos p).asValidPos (by grind) = p := rfl
+
+@[simp, grind =]
+theorem validPos_asValidPos {p : ValidPosPlusOne s} {h : p.isValid} : (ValidPosPlusOne.validPos (p.asValidPos h)) = p := rfl
+
 end ValidPosPlusOne
 
 def startValidPosPlusOne (s : String) : ValidPosPlusOne s :=

regex/Regex/Regex/Basic.lean

@@ -6,7 +6,7 @@ import Regex.Regex.OptimizationInfo
 
 set_option autoImplicit false
 
-open String (ValidPos Slice)
+open String (ValidPos ValidPosPlusOne Slice)
 open Regex.Data (Expr)
 
 /--
@@ -51,10 +51,12 @@ Searches for the next match in the input string.
 -/
 def searchNext {s : String} (self : Regex) (p : ValidPos s) : Option Slice := do
   let slots ← captureNextBuf self 2 p
-  let startPos ← slots[0]
-  let stopPos ← slots[1]
-  if h : startPos ≤ stopPos then
-    pure ⟨s, startPos, stopPos, h⟩
+  let startPos := slots[0]
+  let stopPos := slots[1]
+  if h : stopPos.isValid && startPos ≤ stopPos then
+    have isStopPosValid : stopPos.isValid := by grind
+    have h' : startPos.isValid := ValidPosPlusOne.isValid_of_isValid_of_le isStopPosValid (by grind)
+    pure ⟨s, startPos.asValidPos h', stopPos.asValidPos isStopPosValid, ValidPosPlusOne.le_iff.mp (by grind)⟩
   else
     .none
 
@@ -65,8 +67,7 @@ theorem searchNext_str_eq_some {s : String} {self : Regex} {p : ValidPos s} {s'
   (h : searchNext self p = some s') :
   s'.str = s := by
   simp [searchNext, Option.bind_eq_some_iff] at h
-  obtain ⟨_, _, _, _, _, _, _, eq⟩ := h
-  simp [←eq]
+  grind
 
 /--
 Constructs a `Regex` from a regular expression.