WIP: refactoring towards verified String.split

src/Init/Data/Iterators/Basic.lean

@@ -965,6 +965,11 @@ class LawfulDeterministicIterator (α : Type w) (m : Type w → Type w') [Iterat
   -/
   isPlausibleStep_eq_eq : ∀ it : IterM (α := α) m β, ∃ step, it.IsPlausibleStep = (· = step)
 
+theorem Iter.step_eq {IsPlausibleStep step} {it : Iter (α := α) β} :
+    letI : Iterator α Id β := ⟨IsPlausibleStep, step⟩
+    it.step = IterM.Step.toPure (it := it.toIterM) (step it.toIterM).run.inflate :=
+  (rfl)
+
 namespace Iterators
 
 /--

src/Init/Data/String.lean

@@ -26,3 +26,4 @@ public import Init.Data.String.ToSlice
 public import Init.Data.String.Search
 public import Init.Data.String.Legacy
 public import Init.Data.String.Grind
+public import Init.Data.String.Subslice

src/Init/Data/String/Basic.lean

@@ -1453,6 +1453,12 @@ def Slice.Pos.toReplaceStart {s : Slice} (p₀ : s.Pos) (pos : s.Pos) (h : p₀
 theorem Slice.Pos.offset_sliceFrom {s : Slice} {p₀ : s.Pos} {pos : s.Pos} {h} :
     (sliceFrom p₀ pos h).offset = pos.offset.unoffsetBy p₀.offset := (rfl)
 
+@[simp]
+theorem Slice.Pos.sliceFrom_inj {s : Slice} {p₀ : s.Pos} {pos pos' : s.Pos} {h h'} :
+    p₀.sliceFrom pos h = p₀.sliceFrom pos' h' ↔ pos = pos' := by
+  simp [Pos.ext_iff, Pos.Raw.ext_iff, Pos.le_iff, Pos.Raw.le_iff] at ⊢ h h'
+  omega
+
 @[simp]
 theorem Slice.Pos.ofSliceFrom_startPos {s : Slice} {pos : s.Pos} :
     ofSliceFrom (s.sliceFrom pos).startPos = pos :=
@@ -1722,6 +1728,16 @@ theorem Slice.Pos.offset_cast {s t : Slice} {pos : s.Pos} {h : s = t} :
 theorem Slice.Pos.cast_rfl {s : Slice} {pos : s.Pos} : pos.cast rfl = pos :=
   Slice.Pos.ext (by simp)
 
+@[simp]
+theorem Slice.Pos.cast_le_cast_iff {s t : Slice} {pos pos' : s.Pos} {h : s = t} :
+    pos.cast h ≤ pos'.cast h ↔ pos ≤ pos' := by
+  cases h; simp
+
+@[simp]
+theorem Slice.Pos.cast_lt_cast_iff {s t : Slice} {pos pos' : s.Pos} {h : s = t} :
+    pos.cast h < pos'.cast h ↔ pos < pos' := by
+  cases h; simp
+
 /-- Constructs a valid position on `t` from a valid position on `s` and a proof that `s = t`. -/
 @[inline]
 def Pos.cast {s t : String} (pos : s.Pos) (h : s = t) : t.Pos where
@@ -1956,6 +1972,7 @@ theorem Pos.ne_startPos_of_lt {s : String} {p q : s.Pos} :
     Pos.Raw.byteIdx_zero]
   omega
 
+@[simp]
 theorem Pos.next_ne_startPos {s : String} {p : s.Pos} {h} :
     p.next h ≠ s.startPos :=
   ne_startPos_of_lt p.lt_next
@@ -1992,6 +2009,7 @@ theorem Pos.ne_of_lt {s : String} {p q : s.Pos} : p < q → p ≠ q := by
 theorem Pos.lt_of_lt_of_le {s : String} {p q r : s.Pos} : p < q → q ≤ r → p < r := by
   simpa [Pos.lt_iff, Pos.le_iff] using Pos.Raw.lt_of_lt_of_le
 
+@[simp]
 theorem Pos.le_endPos {s : String} (p : s.Pos) : p ≤ s.endPos := by
   simpa [Pos.le_iff] using p.isValid.le_rawEndPos
 

src/Init/Data/String/Defs.lean

@@ -399,7 +399,7 @@ achieved by tracking the bounds by hand, the slice API is much more convenient.
 string. For this reason, it should be preferred over `Substring.Raw`.
 -/
 structure Slice where
-  /-- The underlying strings. -/
+  /-- The underlying string. -/
   str : String
   /-- The byte position of the start of the string slice. -/
   startInclusive : str.Pos
@@ -441,6 +441,18 @@ def Slice.utf8ByteSize (s : Slice) : Nat :=
 theorem Slice.utf8ByteSize_eq {s : Slice} :
     s.utf8ByteSize = s.endExclusive.offset.byteIdx - s.startInclusive.offset.byteIdx := (rfl)
 
+/--
+Checks whether a slice is empty.
+
+Empty slices have {name}`utf8ByteSize` {lean}`0`.
+
+Examples:
+ * {lean}`"".toSlice.isEmpty = true`
+ * {lean}`" ".toSlice.isEmpty = false`
+-/
+@[inline]
+def Slice.isEmpty (s : Slice) : Bool := s.utf8ByteSize == 0
+
 instance : HAdd Pos.Raw Slice Pos.Raw where
   hAdd p s := { byteIdx := p.byteIdx + s.utf8ByteSize }
 

src/Init/Data/String/Lemmas.lean

@@ -14,6 +14,8 @@ public import Init.Data.Char.Lemmas
 public import Init.Data.List.Lex
 import Init.Data.Order.Lemmas
 public import Init.Data.String.Basic
+public import Init.Data.String.Lemmas.SliceIsEmpty
+public import Init.Data.String.Lemmas.Order
 
 public section
 

src/Init/Data/String/Lemmas/Order.lean

@@ -0,0 +1,81 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Markus Himmel
+-/
+module
+
+prelude
+public import Init.Data.String.Basic
+import Init.Data.String.Grind
+import Init.Data.String.Lemmas.Basic
+
+public section
+
+namespace Std
+
+theorem lt_irrefl {α : Type u} [LT α] [Std.Irrefl (α := α) (· < ·)] {a : α} : ¬ a < a :=
+  Std.Irrefl.irrefl a
+
+theorem ne_of_lt {α : Type u} [LT α] [Std.Irrefl (α := α) (· < ·)] {a b : α} : a < b → a ≠ b :=
+  fun h h' => absurd (h' ▸ h) (h' ▸ lt_irrefl)
+
+end Std
+
+namespace String
+
+@[simp]
+theorem Slice.Pos.next_le_iff_lt {s : Slice} {p q : s.Pos} {h} : p.next h ≤ q ↔ p < q :=
+  ⟨fun h => Std.lt_of_lt_of_le lt_next h, next_le_of_lt⟩
+
+@[simp]
+theorem Slice.Pos.lt_next_iff_le {s : Slice} {p q : s.Pos} {h} : p < q.next h ↔ p ≤ q := by
+  rw [← Decidable.not_iff_not, Std.not_lt, next_le_iff_lt, Std.not_le]
+
+@[simp]
+theorem Pos.next_le_iff_lt {s : String} {p q : s.Pos} {h} : p.next h ≤ q ↔ p < q := by
+  rw [next, Pos.ofToSlice_le_iff, ← Pos.toSlice_lt_toSlice_iff]
+  exact Slice.Pos.next_le_iff_lt
+
+@[simp]
+theorem Slice.Pos.le_startPos {s : Slice} (p : s.Pos) : p ≤ s.startPos ↔ p = s.startPos :=
+  ⟨fun h => Std.le_antisymm h (startPos_le _), by simp +contextual⟩
+
+@[simp]
+theorem Slice.Pos.startPos_lt_iff {s : Slice} (p : s.Pos) : s.startPos < p ↔ p ≠ s.startPos := by
+  simp [← le_startPos, Std.not_le]
+
+@[simp]
+theorem Slice.Pos.endPos_le {s : Slice} (p : s.Pos) : s.endPos ≤ p ↔ p = s.endPos :=
+  ⟨fun h => Std.le_antisymm (le_endPos _) h, by simp +contextual⟩
+
+@[simp]
+theorem Pos.le_startPos {s : String} (p : s.Pos) : p ≤ s.startPos ↔ p = s.startPos :=
+  ⟨fun h => Std.le_antisymm h (startPos_le _), by simp +contextual⟩
+
+@[simp]
+theorem Pos.endPos_le {s : String} (p : s.Pos) : s.endPos ≤ p ↔ p = s.endPos :=
+  ⟨fun h => Std.le_antisymm (le_endPos _) h, by simp +contextual⟩
+
+@[simp]
+theorem Slice.Pos.not_lt_startPos {s : Slice} {p : s.Pos} : ¬ p < s.startPos :=
+  fun h => Std.lt_irrefl (Std.lt_of_lt_of_le h (Slice.Pos.startPos_le _))
+
+theorem Slice.Pos.ne_startPos_of_lt {s : Slice} {p q : s.Pos} : p < q → q ≠ s.startPos := by
+  rintro h rfl
+  simp at h
+
+@[simp]
+theorem Slice.Pos.next_ne_startPos {s : Slice} {p : s.Pos} {h} :
+    p.next h ≠ s.startPos :=
+  ne_startPos_of_lt lt_next
+
+theorem Slice.Pos.ofSliceFrom_lt_ofSliceFrom_iff {s : Slice} {p : s.Pos}
+    {q r : (s.sliceFrom p).Pos} : Slice.Pos.ofSliceFrom q < Slice.Pos.ofSliceFrom r ↔ q < r := by
+  simp [Slice.Pos.lt_iff, Pos.Raw.lt_iff]
+
+theorem Slice.Pos.ofSliceFrom_le_ofSliceFrom_iff {s : Slice} {p : s.Pos}
+    {q r : (s.sliceFrom p).Pos} : Slice.Pos.ofSliceFrom q ≤ Slice.Pos.ofSliceFrom r ↔ q ≤ r := by
+  simp [Slice.Pos.le_iff, Pos.Raw.le_iff]
+
+end String

src/Init/Data/String/Lemmas/SliceIsEmpty.lean

@@ -0,0 +1,66 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Markus Himmel
+-/
+module
+
+prelude
+public import Init.Data.String.Basic
+import all Init.Data.String.Defs
+import Init.Data.String.Lemmas.Order
+import Init.Data.String.Lemmas.Basic
+import Init.Data.String.Grind
+import Init.Grind
+
+public section
+
+namespace String
+
+theorem Slice.isEmpty_eq {s : Slice} : s.isEmpty = (s.utf8ByteSize == 0) :=
+  (rfl)
+
+theorem Slice.isEmpty_iff {s : Slice} :
+    s.isEmpty ↔ s.utf8ByteSize = 0 := by
+  simp [Slice.isEmpty_eq]
+
+theorem Slice.startPos_eq_endPos_iff {s : Slice} :
+    s.startPos = s.endPos ↔ s.isEmpty := by
+  rw [eq_comm]
+  simp [Slice.Pos.ext_iff, Pos.Raw.ext_iff, Slice.isEmpty_iff]
+
+theorem Slice.startPos_ne_endPos_iff {s : Slice} :
+    s.startPos ≠ s.endPos ↔ s.isEmpty = false := by
+  simp [Slice.startPos_eq_endPos_iff]
+
+theorem Slice.startPos_ne_endPos {s : Slice} : s.isEmpty = false → s.startPos ≠ s.endPos :=
+  Slice.startPos_ne_endPos_iff.2
+
+theorem Slice.isEmpty_iff_eq_endPos {s : Slice} :
+    s.isEmpty ↔ ∀ (p q : s.Pos), p = q := by
+  rw [← Slice.startPos_eq_endPos_iff]
+  refine ⟨fun h p q => ?_, fun h => h _ _⟩
+  apply Std.le_antisymm
+  · apply Std.le_trans (Pos.le_endPos _) (h ▸ Pos.startPos_le _)
+  · apply Std.le_trans (Pos.le_endPos _) (h ▸ Pos.startPos_le _)
+
+theorem Slice.isEmpty_eq_false_of_lt {s : Slice} {p q : s.Pos} :
+    p < q → s.isEmpty = false := by
+  rw [← Decidable.not_imp_not]
+  simp
+  rw [Slice.isEmpty_iff_eq_endPos]
+  intro h
+  cases h p q
+  apply Std.lt_irrefl
+
+@[simp]
+theorem Slice.isEmpty_sliceFrom {s : Slice} {p : s.Pos} :
+    (s.sliceFrom p).isEmpty ↔ p = s.endPos := by
+  simp [← startPos_eq_endPos_iff, ← Pos.ofSliceFrom_inj]
+
+@[simp]
+theorem Slice.isEmpty_sliceFrom_eq_false_iff {s : Slice} {p : s.Pos} :
+    (s.sliceFrom p).isEmpty = false ↔ p ≠ s.endPos :=
+  Decidable.not_iff_not.1 (by simp)
+
+end String

src/Init/Data/String/Lemmas/Split.lean

@@ -0,0 +1,140 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Markus Himmel
+-/
+module
+
+prelude
+public import Init.Data.String.Pattern.Basic
+public import Init.Data.String.Subslice
+import Init.Data.String.Lemmas.Basic
+import Init.Data.String.Termination
+import Init.Data.String.Grind
+
+public section
+
+namespace String.Slice.Pattern
+
+namespace SearchStep
+
+inductive Equiv {s : Slice} : List (SearchStep s) → List (SearchStep s) → Prop where
+  | nil : Equiv [] []
+  | cons {l l'} (st) : Equiv l l' → Equiv (st :: l) (st :: l')
+  | trans {l l' l''} : Equiv l l' → Equiv l' l'' → Equiv l l''
+  | cons_rejected_left (p₁ p₂ p₃ l) : p₁ < p₂ → p₂ < p₃ → Equiv (.rejected p₁ p₂ :: .rejected p₂ p₃ :: l) (.rejected p₁ p₃ :: l)
+  | cons_rejected_right (p₁ p₂ p₃ l) : p₁ < p₂ → p₂ < p₃ → Equiv (.rejected p₁ p₃ :: l) (.rejected p₁ p₂ :: .rejected p₂ p₃ :: l)
+
+theorem Equiv.refl {s : Slice} (l : List (SearchStep s)) : Equiv l l := by
+  induction l <;> simp_all [Equiv.nil, Equiv.cons]
+
+theorem Equiv.symm {s : Slice} {l l' : List (SearchStep s)} (h : Equiv l l') : Equiv l' l := by
+  induction h with
+  | nil => exact Equiv.nil
+  | cons st h ih => exact ih.cons _
+  | trans _ _ ih₁ ih₂ => exact ih₂.trans ih₁
+  | cons_rejected_left _ _ _ _ h₁ h₂ => exact cons_rejected_right _ _ _ _ h₁ h₂
+  | cons_rejected_right _ _ _ _ h₁ h₂ => exact cons_rejected_left _ _ _ _ h₁ h₂
+
+end SearchStep
+
+inductive IsMatchListAt {s : Slice} : (pos : s.Pos) → (l : List (SearchStep s)) → Prop where
+  | atEnd : IsMatchListAt s.endPos []
+  | notAtEnd (st : SearchStep s) (hst : st.startPos < st.endPos)
+      (l : List (SearchStep s)) (hl : IsMatchListAt st.endPos l) : IsMatchListAt st.startPos (st::l)
+
+theorem IsMatchListAt.cons {s : Slice} {pos pos' : s.Pos} {st : SearchStep s} {l : List (SearchStep s)}
+    (h : IsMatchListAt pos' l) (hst : st.startPos < st.endPos) (h₁ : st.startPos = pos)
+    (h₂ : st.endPos = pos') : IsMatchListAt pos (st::l) := by
+  cases h₁
+  cases h₂
+  apply IsMatchListAt.notAtEnd _ hst _ h
+
+theorem IsMatchListAt.tail {s : Slice} {pos : s.Pos} {st : SearchStep s} {l : List (SearchStep s)}
+    (h : IsMatchListAt pos (st::l)) : IsMatchListAt st.endPos l := by
+  cases h; assumption
+
+theorem IsMatchListAt.tail_matched {s : Slice} {pos p₁ p₂ : s.Pos} {l : List (SearchStep s)}
+    (h : IsMatchListAt pos (.matched p₁ p₂::l)) : IsMatchListAt p₂ l := by
+  cases h; simp_all
+
+theorem IsMatchListAt.tail_rejected {s : Slice} {pos p₁ p₂ : s.Pos} {l : List (SearchStep s)}
+    (h : IsMatchListAt pos (.rejected p₁ p₂::l)) : IsMatchListAt p₂ l := by
+  cases h; simp_all
+
+theorem IsMatchListAt.eq {s : Slice} {pos : s.Pos} {st : SearchStep s} {l : List (SearchStep s)}
+    (h : IsMatchListAt pos (st::l)) : pos = st.startPos := by
+  cases h; rfl
+
+theorem IsMatchListAt.lt {s : Slice} {pos : s.Pos} {st : SearchStep s} {l : List (SearchStep s)}
+    (h : IsMatchListAt pos (st::l)) : pos < st.endPos := by
+  cases h; assumption
+
+theorem IsMatchListAt.le {s : Slice} {pos : s.Pos} {st : SearchStep s} {l : List (SearchStep s)}
+    (h : IsMatchListAt pos (st::l)) : pos ≤ st.endPos :=
+  Slice.Pos.le_of_lt h.lt
+
+def splitFromSearch {s : Slice} (l : List (SearchStep s)) (currPos : s.Pos)
+    (h : IsMatchListAt currPos l) :
+    { l : List s.Subslice // l.head?.any (·.startInclusive = currPos) } :=
+  match l with
+  | [] => ⟨[s.subslice currPos s.endPos (Slice.Pos.le_endPos _)], by simp⟩
+  | st::sts =>
+    match st with
+    | .matched p₁ p₂ =>
+      ⟨s.subslice currPos currPos (Pos.le_refl _) :: splitFromSearch sts p₂ (by simpa using h.tail), by simp⟩
+    | .rejected p₁ p₂ =>
+      match splitFromSearch sts p₂ (by simpa using h.tail) with
+      | ⟨st'::sts', h'⟩ => ⟨st'.extendLeft currPos (by simp at h'; simpa [h'] using h.le) :: sts', by simp⟩
+
+theorem SearchStep.equiv_nil_iff {s : Slice} {l : List (SearchStep s)} : Equiv l [] ↔ l = [] := by
+  refine ⟨fun h => ?_, fun h => h ▸ Equiv.nil⟩
+  generalize hm : [] = m
+  rw [hm] at h
+  induction h with
+  | nil => rfl
+  | cons => simp at hm
+  | trans h₁ h₂ ih₁ ih₂ => simp_all
+  | cons_rejected_left => simp_all
+  | cons_rejected_right => simp_all
+
+theorem SearchStep.Equiv.isMatchListAt {s : Slice} {l l' : List (SearchStep s)}
+    {currPos : s.Pos} (h : Equiv l l') (h' : IsMatchListAt currPos l) : IsMatchListAt currPos l' := by
+  induction h generalizing currPos with
+  | nil => assumption
+  | cons =>
+    cases h'
+    apply IsMatchListAt.notAtEnd <;> simp_all
+  | trans => simp_all
+  | cons_rejected_left p₁ p₂ p₃ l h₁ h₂ =>
+    apply h'.tail.tail.cons
+    · simpa using Std.lt_trans h₁ h₂
+    · simpa using h'.eq.symm
+    · simp
+  | cons_rejected_right p₁ p₂ p₃ l h₁ h₂ =>
+    apply (h'.tail.cons (pos := p₂) ..).cons
+    · simpa
+    · simpa using h'.eq.symm
+    · simp
+    · simpa
+    · simp
+    · simp
+
+theorem SearchStep.Equiv.splitFromSearch_eq {s : Slice} {l l' : List (SearchStep s)} {currPos : s.Pos}
+    (h : Equiv l l') (h₀) : splitFromSearch l currPos h₀ = splitFromSearch l' currPos (h.isMatchListAt h₀) := by
+  induction h generalizing currPos with
+  | nil => simp [splitFromSearch]
+  | cons st h ih => cases st <;> simp_all [splitFromSearch]
+  | trans h h' ih ih' => rw [ih, ih']
+  | cons_rejected_left p₁ p₂ p₃ l h₁ h₂ =>
+    simp [splitFromSearch]
+    rcases splitFromSearch l p₃ _ with ⟨(_|_),_⟩
+    · contradiction
+    · simp
+  | cons_rejected_right p₁ p₂ p₃ l h₁ h₂ =>
+    simp [splitFromSearch]
+    rcases splitFromSearch l p₃ _ with ⟨(_|_),_⟩
+    · contradiction
+    · simp
+
+end String.Slice.Pattern