feat: assorted string lemmas (#12709)

This PR adds various `String` lemmas that will be useful for deriving
high-level theorems about `String.split`.

src/Init/Data/String/Defs.lean

@@ -403,7 +403,6 @@ achieved by tracking the bounds by hand, the slice API is much more convenient.
 `String.Slice` bundles proofs to ensure that the start and end positions always delineate a valid
 string. For this reason, it should be preferred over `Substring.Raw`.
 -/
-@[ext]
 structure Slice where
   /-- The underlying strings. -/
   str : String

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

@@ -99,6 +99,15 @@ theorem Slice.utf8ByteSize_eq_size_toByteArray_copy {s : Slice} :
     s.utf8ByteSize = s.copy.toByteArray.size := by
   simp [utf8ByteSize_eq]
 
+@[ext (iff := false)]
+theorem Slice.ext {s t : Slice} (h : s.str = t.str)
+    (hsi : s.startInclusive.cast h = t.startInclusive)
+    (hee : s.endExclusive.cast h = t.endExclusive) : s = t := by
+  rcases s with ⟨s, s₁, e₁, h₁⟩
+  rcases t with ⟨t, s₂, e₂, h₂⟩
+  cases h
+  simp_all
+
 section Iterate
 
 /-
@@ -106,32 +115,71 @@ These lemmas are slightly evil because they are non-definitional equalities betw
 are useful and they are at least equalities between slices with definitionally equal underlying
 strings, so it should be fine.
 -/
-set_option backward.isDefEq.respectTransparency false in
 @[simp]
 theorem Slice.sliceTo_sliceFrom {s : Slice} {pos pos'} :
     (s.sliceFrom pos).sliceTo pos' =
       s.slice pos (Slice.Pos.ofSliceFrom pos') Slice.Pos.le_ofSliceFrom := by
-  ext <;> simp [String.Pos.ext_iff, Pos.Raw.offsetBy_assoc]
+  ext <;> simp [Pos.Raw.offsetBy_assoc]
 
-set_option backward.isDefEq.respectTransparency false in
 @[simp]
 theorem Slice.sliceFrom_sliceTo {s : Slice} {pos pos'} :
     (s.sliceTo pos).sliceFrom pos' =
       s.slice (Slice.Pos.ofSliceTo pos') pos Slice.Pos.ofSliceTo_le := by
-  ext <;> simp [String.Pos.ext_iff]
+  ext <;> simp
 
-set_option backward.isDefEq.respectTransparency false in
 @[simp]
 theorem Slice.sliceFrom_sliceFrom {s : Slice} {pos pos'} :
     (s.sliceFrom pos).sliceFrom pos' =
       s.sliceFrom (Slice.Pos.ofSliceFrom pos') := by
-  ext <;> simp [String.Pos.ext_iff, Pos.Raw.offsetBy_assoc]
+  ext <;> simp [Pos.Raw.offsetBy_assoc]
 
-set_option backward.isDefEq.respectTransparency false in
 @[simp]
 theorem Slice.sliceTo_sliceTo {s : Slice} {pos pos'} :
     (s.sliceTo pos).sliceTo pos' = s.sliceTo (Slice.Pos.ofSliceTo pos') := by
-  ext <;> simp [String.Pos.ext_iff]
+  ext <;> simp
+
+@[simp]
+theorem Slice.sliceFrom_slice {s : Slice} {p₁ p₂ h p} :
+    (s.slice p₁ p₂ h).sliceFrom p = s.slice (Pos.ofSlice p) p₂ Pos.ofSlice_le := by
+  ext <;> simp [Nat.add_assoc]
+
+@[simp]
+theorem Slice.sliceTo_slice {s : Slice} {p₁ p₂ h p} :
+    (s.slice p₁ p₂ h).sliceTo p = s.slice p₁ (Pos.ofSlice p) Pos.le_ofSlice := by
+  ext <;> simp [Nat.add_assoc]
+
+@[simp]
+theorem sliceTo_sliceFrom {s : String} {pos pos'} :
+    (s.sliceFrom pos).sliceTo pos' =
+      s.slice pos (Pos.ofSliceFrom pos') Pos.le_ofSliceFrom := by
+  ext <;> simp
+
+@[simp]
+theorem sliceFrom_sliceTo {s : String} {pos pos'} :
+    (s.sliceTo pos).sliceFrom pos' =
+      s.slice (Pos.ofSliceTo pos') pos Pos.ofSliceTo_le := by
+  ext <;> simp
+
+@[simp]
+theorem sliceFrom_sliceFrom {s : String} {pos pos'} :
+    (s.sliceFrom pos).sliceFrom pos' =
+      s.sliceFrom (Pos.ofSliceFrom pos') := by
+  ext <;> simp
+
+@[simp]
+theorem sliceTo_sliceTo {s : String} {pos pos'} :
+    (s.sliceTo pos).sliceTo pos' = s.sliceTo (Pos.ofSliceTo pos') := by
+  ext <;> simp
+
+@[simp]
+theorem sliceFrom_slice {s : String} {p₁ p₂ h p} :
+    (s.slice p₁ p₂ h).sliceFrom p = s.slice (Pos.ofSlice p) p₂ Pos.ofSlice_le := by
+  ext <;> simp
+
+@[simp]
+theorem sliceTo_slice {s : String} {p₁ p₂ h p} :
+    (s.slice p₁ p₂ h).sliceTo p = s.slice p₁ (Pos.ofSlice p) Pos.le_ofSlice := by
+  ext <;> simp
 
 end Iterate
 
@@ -176,4 +224,7 @@ theorem Pos.get_ofToSlice {s : String} {p : (s.toSlice).Pos} {h} :
     (ofToSlice p).get h = p.get (by simpa [← ofToSlice_inj]) := by
   simp [get_eq_get_toSlice]
 
+@[simp]
+theorem push_empty {c : Char} : "".push c = singleton c := rfl
+
 end String

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

@@ -87,6 +87,10 @@ theorem isEmpty_iff_utf8ByteSize_eq_zero {s : String} : s.isEmpty ↔ s.utf8Byte
 theorem isEmpty_iff {s : String} : s.isEmpty ↔ s = "" := by
   simp [isEmpty_iff_utf8ByteSize_eq_zero]
 
+@[simp]
+theorem isEmpty_eq_false_iff {s : String} : s.isEmpty = false ↔ s ≠ "" := by
+  simp [← isEmpty_iff]
+
 theorem startPos_ne_endPos_iff {s : String} : s.startPos ≠ s.endPos ↔ s ≠ "" := by
   simp
 
@@ -175,4 +179,34 @@ theorem Slice.toByteArray_copy_ne_empty_iff {s : Slice} :
     s.copy.toByteArray ≠ ByteArray.empty ↔ s.isEmpty = false := by
   simp
 
+section CopyEqEmpty
+
+-- Yes, `simp` can prove these, but we still need to mark them as simp lemmas.
+
+@[simp]
+theorem copy_slice_self {s : String} {p : s.Pos} : (s.slice p p (Pos.le_refl _)).copy = "" := by
+  simp
+
+@[simp]
+theorem copy_sliceTo_startPos {s : String} : (s.sliceTo s.startPos).copy = "" := by
+  simp
+
+@[simp]
+theorem copy_sliceFrom_startPos {s : String} : (s.sliceFrom s.endPos).copy = "" := by
+  simp
+
+@[simp]
+theorem Slice.copy_slice_self {s : Slice} {p : s.Pos} : (s.slice p p (Pos.le_refl _)).copy = "" := by
+  simp
+
+@[simp]
+theorem Slice.copy_sliceTo_startPos {s : Slice} : (s.sliceTo s.startPos).copy = "" := by
+  simp
+
+@[simp]
+theorem Slice.copy_sliceFrom_startPos {s : Slice} : (s.sliceFrom s.endPos).copy = "" := by
+  simp
+
+end CopyEqEmpty
+
 end String

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

@@ -105,6 +105,22 @@ theorem Slice.Pos.le_next {s : Slice} {p : s.Pos} {h} : p ≤ p.next h :=
 theorem Pos.le_next {s : String} {p : s.Pos} {h} : p ≤ p.next h :=
   Std.le_of_lt (by simp)
 
+@[simp]
+theorem Slice.Pos.ne_next {s : Slice} {p : s.Pos} {h} : p ≠ p.next h :=
+  Std.ne_of_lt (by simp)
+
+@[simp]
+theorem Pos.ne_next {s : String} {p : s.Pos} {h} : p ≠ p.next h :=
+  Std.ne_of_lt (by simp)
+
+@[simp]
+theorem Slice.Pos.next_ne {s : Slice} {p : s.Pos} {h} : p.next h ≠ p :=
+  Ne.symm (by simp)
+
+@[simp]
+theorem Pos.next_ne {s : String} {p : s.Pos} {h} : p.next h ≠ p :=
+  Ne.symm (by simp)
+
 @[simp]
 theorem Slice.Pos.next_ne_startPos {s : Slice} {p : s.Pos} {h} :
     p.next h ≠ s.startPos :=

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

@@ -416,14 +416,6 @@ theorem splits_singleton_iff {s : String} {p : s.Pos} {c : Char} {t : String} :
   rw [← Pos.splits_toSlice_iff, Slice.splits_singleton_iff]
   simp [← Pos.ofToSlice_inj]
 
-@[simp]
-theorem Slice.copy_sliceTo_startPos {s : Slice} : (s.sliceTo s.startPos).copy = "" :=
-  s.startPos.splits.eq_left s.splits_startPos
-
-@[simp]
-theorem copy_sliceTo_startPos {s : String} : (s.sliceTo s.startPos).copy = "" :=
-  s.startPos.splits.eq_left s.splits_startPos
-
 theorem Slice.splits_next_startPos {s : Slice} {h : s.startPos ≠ s.endPos} :
     (s.startPos.next h).Splits
       (singleton (s.startPos.get h)) (s.sliceFrom (s.startPos.next h)).copy := by
@@ -597,4 +589,40 @@ theorem Slice.Pos.Splits.copy_sliceFrom_eq {s : Slice} {p : s.Pos} (h : p.Splits
     (s.sliceFrom p).copy = t₂ :=
   p.splits.eq_right h
 
+theorem copy_slice_eq_append_of_lt {s : String} {p q : s.Pos} (h : p < q) :
+    (s.slice p q (by exact Std.le_of_lt h)).copy =
+      String.singleton (p.get (by exact Pos.ne_endPos_of_lt h)) ++
+        (s.slice (p.next (by exact Pos.ne_endPos_of_lt h)) q (by simpa)).copy := by
+  have hsp := (s.slice p q (Std.le_of_lt h)).splits_startPos
+  obtain ⟨t₂, ht⟩ := hsp.exists_eq_singleton_append (by simpa [← Pos.ofSlice_inj] using Std.ne_of_lt h)
+  have := (ht ▸ hsp).next.eq_right (Slice.Pos.splits _)
+  simpa [Pos.ofSlice_next, this, Pos.get_eq_get_ofSlice] using ht
+
+@[simp]
+theorem copy_slice_next {s : String} {p : s.Pos} {h} :
+    (s.slice p (p.next h) (by simp)).copy = String.singleton (p.get h) := by
+  rw [copy_slice_eq_append_of_lt (by simp), copy_slice_self, String.append_empty]
+
+theorem splits_slice {s : String} {p₀ p₁ : s.Pos} (h) (p : (s.slice p₀ p₁ h).Pos) :
+    p.Splits (s.slice p₀ (Pos.ofSlice p) Pos.le_ofSlice).copy (s.slice (Pos.ofSlice p) p₁ Pos.ofSlice_le).copy := by
+  simpa using p.splits
+
+theorem Slice.copy_slice_eq_append_of_lt {s : Slice} {p q : s.Pos} (h : p < q) :
+    (s.slice p q (by exact Std.le_of_lt h)).copy =
+      String.singleton (p.get (by exact Pos.ne_endPos_of_lt h)) ++
+        (s.slice (p.next (Pos.ne_endPos_of_lt h)) q (by simpa)).copy := by
+  have hsp := (s.slice p q (Std.le_of_lt h)).splits_startPos
+  obtain ⟨t₂, ht⟩ := hsp.exists_eq_singleton_append (by simpa [← Pos.ofSlice_inj] using Std.ne_of_lt h)
+  have := (ht ▸ hsp).next.eq_right (Slice.Pos.splits _)
+  simpa [Pos.ofSlice_next, this, Pos.get_eq_get_ofSlice] using ht
+
+@[simp]
+theorem Slice.copy_slice_next {s : Slice} {p : s.Pos} {h} :
+    (s.slice p (p.next h) (by simp)).copy = String.singleton (p.get h) := by
+  rw [copy_slice_eq_append_of_lt (by simp), copy_slice_self, String.append_empty]
+
+theorem Slice.splits_slice {s : Slice} {p₀ p₁ : s.Pos} (h) (p : (s.slice p₀ p₁ h).Pos) :
+    p.Splits (s.slice p₀ (Pos.ofSlice p) Pos.le_ofSlice).copy (s.slice (Pos.ofSlice p) p₁ Pos.ofSlice_le).copy := by
+  simpa using p.splits
+
 end String

src/Init/Data/String/Subslice.lean

@@ -76,6 +76,15 @@ def toString {s : Slice} (sl : s.Subslice) : String :=
 instance {s : Slice} : ToString s.Subslice where
   toString
 
+@[simp]
+theorem copy_eq {s : Slice} {sl : s.Subslice} : sl.copy = sl.toSlice.copy := (rfl)
+
+@[simp]
+theorem toString_eq {s : Slice} {sl : s.Subslice} : sl.toString = sl.toSlice.copy := (rfl)
+
+@[simp]
+theorem toStringToString_eq {s : Slice} {sl : s.Subslice} : ToString.toString sl = sl.toSlice.copy := (rfl)
+
 end Subslice
 
 /--
@@ -130,6 +139,10 @@ theorem startInclusive_subsliceFrom {s : Slice} {newStart : s.Pos} :
 theorem endExclusive_subsliceFrom {s : Slice} {newStart : s.Pos} :
     (s.subsliceFrom newStart).endExclusive = s.endPos := (rfl)
 
+@[simp]
+theorem subslice_endPos {s : Slice} {newStart : s.Pos} :
+    s.subslice newStart s.endPos (Slice.Pos.le_endPos _) = s.subsliceFrom newStart := (rfl)
+
 /-- The entire slice, as a subslice of itself. -/
 @[inline]
 def toSubslice (s : Slice) : s.Subslice :=