feat: lemmas about splitting the empty string/slice

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

@@ -20,6 +20,7 @@ import Init.Data.String.OrderInstances
 import Init.Data.Iterators.Lemmas.Basic
 import Init.Data.Iterators.Lemmas.Consumers.Collect
 import Init.Data.Iterators.Lemmas.Combinators.FilterMap
+import Init.Data.String.Lemmas.IsEmpty
 
 set_option doc.verso true
 
@@ -164,12 +165,29 @@ end Pattern
 
 open Pattern
 
+public theorem toList_splitToSubslice_of_isEmpty {ρ : Type} (pat : ρ)
+    [Model.ForwardPatternModel pat] {σ : Slice → Type}
+    [ToForwardSearcher pat σ] [∀ s, Std.Iterator (σ s) Id (SearchStep s)]
+    [∀ s, Std.Iterators.Finite (σ s) Id] [Model.LawfulToForwardSearcherModel pat] {s : Slice}
+    (h : s.isEmpty = true) :
+    (s.splitToSubslice pat).toList = [s.subsliceFrom s.endPos] := by
+  simp [toList_splitToSubslice_eq_modelSplit, Slice.startPos_eq_endPos_iff.2 h]
+
 public theorem toList_split_eq_splitToSubslice {ρ : Type} (pat : ρ) {σ : Slice → Type}
     [ToForwardSearcher pat σ] [∀ s, Std.Iterator (σ s) Id (SearchStep s)]
     [∀ s, Std.Iterators.Finite (σ s) Id] {s : Slice} :
     (s.split pat).toList = (s.splitToSubslice pat).toList.map Subslice.toSlice := by
   simp [split, Std.Iter.toList_map]
 
+public theorem toList_split_of_isEmpty {ρ : Type} (pat : ρ)
+    [Model.ForwardPatternModel pat] {σ : Slice → Type}
+    [ToForwardSearcher pat σ] [∀ s, Std.Iterator (σ s) Id (SearchStep s)]
+    [∀ s, Std.Iterators.Finite (σ s) Id] [Model.LawfulToForwardSearcherModel pat] {s : Slice}
+    (h : s.isEmpty = true) :
+    (s.split pat).toList.map Slice.copy = [""] := by
+  rw [toList_split_eq_splitToSubslice, toList_splitToSubslice_of_isEmpty _ h]
+  simp
+
 end Slice
 
 open Slice.Pattern
@@ -178,4 +196,12 @@ public theorem split_eq_split_toSlice {ρ : Type} {pat : ρ} {σ : Slice → Typ
     [ToForwardSearcher pat σ] [∀ s, Std.Iterator (σ s) Id (SearchStep s)] {s : String} :
   s.split pat = s.toSlice.split pat := (rfl)
 
+@[simp]
+public theorem toList_split_empty {ρ : Type} (pat : ρ)
+    [Model.ForwardPatternModel pat] {σ : Slice → Type}
+    [ToForwardSearcher pat σ] [∀ s, Std.Iterator (σ s) Id (SearchStep s)]
+    [∀ s, Std.Iterators.Finite (σ s) Id] [Model.LawfulToForwardSearcherModel pat] :
+    ("".split pat).toList.map Slice.copy = [""] := by
+  rw [split_eq_split_toSlice, Slice.toList_split_of_isEmpty _ (by simp)]
+
 end String

src/Init/Data/String/Subslice.lean

@@ -7,6 +7,8 @@ module
 
 prelude
 public import Init.Data.String.Basic
+import Init.Data.String.Lemmas.IsEmpty
+import Init.Data.String.Lemmas.Basic
 
 set_option doc.verso true
 
@@ -59,6 +61,11 @@ theorem startInclusive_toSlice {s : Slice} {sl : s.Subslice} :
 theorem endExclusive_toSlice {s : Slice} {sl : s.Subslice} :
     sl.toSlice.endExclusive = sl.endExclusive.str := rfl
 
+@[simp]
+theorem isEmpty_toSlice_iff {s : Slice} {sl : s.Subslice} :
+    sl.toSlice.isEmpty ↔ sl.startInclusive = sl.endExclusive := by
+  simp [toSlice]
+
 instance {s : Slice} : CoeOut s.Subslice Slice where
   coe := Subslice.toSlice
 
@@ -144,6 +151,11 @@ theorem endExclusive_subsliceFrom {s : Slice} {newStart : s.Pos} :
 theorem subslice_endPos {s : Slice} {newStart : s.Pos} :
     s.subslice newStart s.endPos (Slice.Pos.le_endPos _) = s.subsliceFrom newStart := (rfl)
 
+@[simp]
+theorem toSlice_subsliceFrom {s : Slice} {newStart : s.Pos} :
+    (s.subsliceFrom newStart).toSlice = s.sliceFrom newStart := by
+  ext1 <;> simp
+
 /-- The entire slice, as a subslice of itself. -/
 @[inline]
 def toSubslice (s : Slice) : s.Subslice :=