feat: String.toList_map (#11021)

This PR adds more theory about `Splits` for strings and deduces the
first user-facing `String` lemma, `String.toList_map`.

Author: TwoFX

doc/examples/palindromes.lean

@@ -94,10 +94,8 @@ theorem List.palindrome_of_eq_reverse (h : as.reverse = as) : Palindrome as := b
   next   => exact Palindrome.nil
   next a => exact Palindrome.single a
   next a b as ih =>
-    have : a = b := by simp_all
-    subst this
-    have : as.reverse = as := by simp_all
-    exact Palindrome.sandwich a (ih this)
+    obtain ⟨rfl, h, -⟩ := by simpa using h
+    exact Palindrome.sandwich b (ih h)
 
 /-!
 We now define a function that returns `true` iff `as` is a palindrome.

src/Init/Data/Array/Lemmas.lean

@@ -245,26 +245,20 @@ theorem back_eq_of_push_eq {a b : α} {xs ys : Array α} (h : xs.push a = ys.pus
   replace h := List.append_inj_right' h (by simp)
   simpa using h
 
-theorem pop_eq_of_push_eq {a b : α} {xs ys : Array α} (h : xs.push a = ys.push b) : xs = ys := by
+theorem push_eq_push {a b : α} {xs ys : Array α} : xs.push a = ys.push b ↔ a = b ∧ xs = ys := by
   cases xs
   cases ys
-  simp at h
-  replace h := List.append_inj_left' h (by simp)
-  simp [h]
+  simp [And.comm]
+
+theorem pop_eq_of_push_eq {a b : α} {xs ys : Array α} (h : xs.push a = ys.push b) : xs = ys :=
+  (push_eq_push.1 h).2
 
 theorem push_inj_left {a : α} {xs ys : Array α} : xs.push a = ys.push a ↔ xs = ys :=
   ⟨pop_eq_of_push_eq, fun h => by simp [h]⟩
 
 theorem push_inj_right {a b : α} {xs : Array α} : xs.push a = xs.push b ↔ a = b :=
   ⟨back_eq_of_push_eq, fun h => by simp [h]⟩
 
-theorem push_eq_push {a b : α} {xs ys : Array α} : xs.push a = ys.push b ↔ a = b ∧ xs = ys := by
-  constructor
-  · intro h
-    exact ⟨back_eq_of_push_eq h, pop_eq_of_push_eq h⟩
-  · rintro ⟨rfl, rfl⟩
-    rfl
-
 theorem exists_push_of_ne_empty {xs : Array α} (h : xs ≠ #[]) :
     ∃ (ys : Array α) (a : α), xs = ys.push a := by
   rcases xs with ⟨xs⟩

src/Init/Data/List/Lemmas.lean

@@ -2494,6 +2494,9 @@ theorem flatten_reverse {L : List (List α)} :
     ⟨by rw [length_reverse, length_replicate],
      fun _ h => eq_of_mem_replicate (mem_reverse.1 h)⟩
 
+@[simp]
+theorem append_singleton_inj {as bs : List α} : as ++ [a] = bs ++ [b] ↔ as = bs ∧ a = b := by
+  rw [← List.reverse_inj, And.comm]; simp
 
 /-! ### foldlM and foldrM -/
 

src/Init/Data/String/Basic.lean

@@ -634,6 +634,7 @@ theorem utf8ByteSize_push {s : String} {c : Char} :
     (s.push c).utf8ByteSize = s.utf8ByteSize + c.utf8Size := by
   simp [← size_bytes, List.utf8Encode_singleton]
 
+@[simp]
 theorem rawEndPos_push {s : String} {c : Char} : (s.push c).rawEndPos = s.rawEndPos + c := by
   simp [Pos.Raw.ext_iff]
 
@@ -1130,6 +1131,11 @@ theorem Slice.Pos.get_eq_utf8DecodeChar {s : Slice} (pos : s.Pos) (h : pos ≠ s
     pos.get h = s.str.bytes.utf8DecodeChar (s.startInclusive.offset.byteIdx + pos.offset.byteIdx)
       ((Pos.Raw.isValidForSlice_iff_isSome_utf8DecodeChar?.1 pos.isValidForSlice).elim (by simp_all [Pos.ext_iff]) (·.2)) := (rfl)
 
+theorem Slice.Pos.utf8Encode_get_eq_extract {s : Slice} (pos : s.Pos) (h : pos ≠ s.endPos) :
+    List.utf8Encode [pos.get h] = s.str.bytes.extract (s.startInclusive.offset.byteIdx + pos.offset.byteIdx)
+      (s.startInclusive.offset.byteIdx + pos.offset.byteIdx + (pos.get h).utf8Size) := by
+  rw [get_eq_utf8DecodeChar pos h, List.utf8Encode_singleton, ByteArray.utf8EncodeChar_utf8DecodeChar]
+
 /-- Returns the byte at the given position in the string, or `none` if the position is the end
 position. -/
 @[expose]
@@ -1495,6 +1501,14 @@ theorem Slice.Pos.lt_next {s : Slice} {pos : s.Pos} {h : pos ≠ s.endPos} :
     pos < pos.next h := by
   simp [Pos.lt_iff, Pos.Raw.lt_iff, Char.utf8Size_pos]
 
+theorem Slice.Pos.copy_eq_copy_replaceEnd_append_get {s : Slice} {pos : s.Pos} (h : pos ≠ s.endPos) :
+    s.copy = (s.replaceEnd pos).copy ++ singleton (pos.get h) ++ (s.replaceStart (pos.next h)).copy := by
+  suffices (max (s.startInclusive.offset.byteIdx + (pos.offset.byteIdx + (pos.get h).utf8Size)) s.endExclusive.offset.byteIdx)
+      = s.endExclusive.offset.byteIdx by
+    simp [← bytes_inj, bytes_copy, utf8Encode_get_eq_extract, Nat.add_assoc, this]
+  rw [Nat.max_eq_right]
+  simpa [Pos.Raw.le_iff] using (pos.next h).offset_str_le_offset_endExclusive
+
 @[inline, expose]
 def Slice.Pos.prevAux {s : Slice} (pos : s.Pos) (h : pos ≠ s.startPos) : String.Pos.Raw :=
   go (pos.offset.byteIdx - 1) (by
@@ -1861,10 +1875,13 @@ abbrev utf8SetAux (c' : Char) : List Char → Pos.Raw → Pos.Raw → List Char
   Pos.Raw.utf8SetAux c'
 
 @[simp]
-theorem ValidPos.toSlice_get {s : String} {p : s.ValidPos} {h} :
+theorem ValidPos.get_toSlice {s : String} {p : s.ValidPos} {h} :
     p.toSlice.get h = p.get (ne_of_apply_ne (·.toSlice) (by simp_all)) := by
   rfl
 
+theorem ValidPos.get_eq_get_toSlice {s : String} {p : s.ValidPos} {h}  :
+    p.get h = p.toSlice.get (ne_of_apply_ne Slice.Pos.ofSlice (by simp [h])) := rfl
+
 @[simp]
 theorem ValidPos.offset_next {s : String} (p : s.ValidPos) (h : p ≠ s.endValidPos) :
     (p.next h).offset = p.offset + p.get h := by
@@ -1943,6 +1960,14 @@ theorem Pos.Raw.isValidForSlice_stringReplaceStart {s : String} {p : s.ValidPos}
   rw [replaceStart, isValidForSlice_replaceStart, isValidForSlice_toSlice_iff,
     ValidPos.offset_toSlice]
 
+theorem ValidPos.utf8Encode_get_eq_extract {s : String} (pos : s.ValidPos) (h : pos ≠ s.endValidPos) :
+    List.utf8Encode [pos.get h] = s.bytes.extract pos.offset.byteIdx (pos.offset.byteIdx + (pos.get h).utf8Size) := by
+  rw [get_eq_get_toSlice, Slice.Pos.utf8Encode_get_eq_extract]
+  simp
+
+theorem ValidPos.eq_copy_replaceEnd_append_get {s : String} {pos : s.ValidPos} (h : pos ≠ s.endValidPos) :
+    s = (s.replaceEnd pos).copy ++ singleton (pos.get h) ++ (s.replaceStart (pos.next h)).copy := by
+  simp [← bytes_inj, utf8Encode_get_eq_extract pos h, Slice.bytes_copy, ← size_bytes]
 
 /--
 Returns the next position in a string after position `p`. If `p` is not a valid position or

src/Init/Data/String/Lemmas.lean

@@ -7,6 +7,7 @@ module
 
 prelude
 public import Init.Data.String.Lemmas.Splits
+public import Init.Data.String.Lemmas.Modify
 public import Init.Data.Char.Order
 public import Init.Data.Char.Lemmas
 public import Init.Data.List.Lex

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

@@ -0,0 +1,46 @@
+/-
+Copyright (c) 2025 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
+
+/-!
+# Basic lemmas about strings
+
+This file contains lemmas that could be in `Init.Data.String.Basic` but are not because they are
+not needed to define basic string operations.
+-/
+
+public section
+
+namespace String
+
+@[simp]
+theorem singleton_append_inj : singleton c ++ s = singleton d ++ t ↔ c = d ∧ s = t := by
+  simp [← toList_inj]
+
+@[simp]
+theorem push_inj : push s c = push t d ↔ s = t ∧ c = d := by
+  simp [← toList_inj]
+
+@[simp]
+theorem append_eq_empty_iff {s t : String} : s ++ t = "" ↔ s = "" ∧ t = "" := by
+  rw [← toList_inj]; simp
+
+@[simp]
+theorem push_ne_empty : push s c ≠ "" := by
+  rw [ne_eq, ← toList_inj]; simp
+
+@[simp]
+theorem singleton_ne_empty {c : Char} : singleton c ≠ "" := by
+  simp [singleton]
+
+@[simp]
+theorem Slice.Pos.toCopy_inj {s : Slice} {p₁ p₂ : s.Pos} : p₁.toCopy = p₂.toCopy ↔ p₁ = p₂ := by
+  simp [Pos.ext_iff, ValidPos.ext_iff]
+
+end String

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

@@ -0,0 +1,60 @@
+/-
+Copyright (c) 2025 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.Modify
+import all Init.Data.String.Modify
+import Init.Data.String.Lemmas.Basic
+
+/-!
+# Lemmas for `Init.Data.String.Modify`
+
+This file contains lemmas for the operations defined in `Init.Data.String.Modify`.
+
+Note that `Init.Data.String.Modify` already proves a few lemmas which are needed immediately.
+-/
+
+public section
+
+namespace String
+
+/-- You might want to invoke `ValidPos.Splits.exists_eq_singleton_append` to be able to apply this. -/
+theorem ValidPos.Splits.pastSet {s : String} {p : s.ValidPos} {t₁ t₂ : String}
+    {c d : Char} (h : p.Splits t₁ (singleton c ++ t₂)) :
+    (p.pastSet d h.ne_endValidPos_of_singleton).Splits (t₁ ++ singleton d) t₂ := by
+  generalize h.ne_endValidPos_of_singleton = hp
+  obtain ⟨rfl, rfl, rfl⟩ := by simpa using h.eq (p.splits_next_right hp)
+  apply splits_pastSet
+
+/-- You might want to invoke `ValidPos.Splits.exists_eq_singleton_append` to be able to apply this. -/
+theorem ValidPos.Splits.pastModify {s : String} {p : s.ValidPos} {t₁ t₂ : String}
+    {c : Char} (h : p.Splits t₁ (singleton c ++ t₂)) :
+    (p.pastModify f h.ne_endValidPos_of_singleton).Splits
+    (t₁ ++ singleton (f (p.get h.ne_endValidPos_of_singleton))) t₂ :=
+  h.pastSet
+
+theorem toList_mapAux {f : Char → Char} {s : String} {p : s.ValidPos}
+    (h : p.Splits t₁ t₂) : (mapAux f s p).toList = t₁.toList ++ t₂.toList.map f := by
+  fun_induction mapAux generalizing t₁ t₂ with
+  | case1 s => simp_all
+  | case2 s p hp ih =>
+    obtain ⟨c, rfl⟩ := h.exists_eq_singleton_append hp
+    simp [ih h.pastModify]
+
+@[simp]
+theorem toList_map {f : Char → Char} {s : String} : (s.map f).toList = s.toList.map f := by
+  simp [map, toList_mapAux s.splits_startValidPos]
+
+@[simp]
+theorem length_map {f : Char → Char} {s : String} : (s.map f).length = s.length := by
+  simp [← length_toList]
+
+@[simp]
+theorem map_eq_empty {f : Char → Char} {s : String} : s.map f = "" ↔ s = "" := by
+  simp [← toList_eq_nil_iff]
+
+end String