Sorry-free

Author: TwoFX

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/Map.lean

@@ -0,0 +1,51 @@
+/-
+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
+
+/-!
+# 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
+
+-- TODO: `hp` actually follows from `h`.
+/-- 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} (hp : p ≠ s.endValidPos)
+    {c d : Char} (h : p.Splits t₁ (singleton c ++ t₂)) :
+    (p.pastSet d hp).Splits (t₁ ++ singleton d) t₂ := by
+  obtain ⟨rfl, rfl, rfl⟩ := by simpa using h.eq (p.splits_next_right hp)
+  apply splits_pastSet
+
+-- TODO: `hp` actually follows from `h`.
+/-- 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} (hp : p ≠ s.endValidPos)
+    {c : Char} (h : p.Splits t₁ (singleton c ++ t₂)) :
+    (p.pastModify f hp).Splits (t₁ ++ singleton (f (p.get hp))) t₂ :=
+  h.pastSet hp
+
+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 hp)]
+
+@[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]
+
+end String

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

@@ -89,11 +89,25 @@ theorem Slice.Pos.splits {s : Slice} (p : s.Pos) :
   eq_append := copy_eq_copy_replaceEnd
   offset_eq_rawEndPos := by simp
 
+theorem ValidPos.Splits.bytes_left_eq {s : String} {p : s.ValidPos} {t₁ t₂}
+    (h : p.Splits t₁ t₂) : t₁.bytes = s.bytes.extract 0 p.offset.byteIdx := by
+  simp [h.eq_append, h.offset_eq_rawEndPos, ByteArray.extract_append_eq_left]
+
+theorem ValidPos.Splits.bytes_right_eq {s : String} {p : s.ValidPos} {t₁ t₂}
+    (h : p.Splits t₁ t₂) : t₂.bytes = s.bytes.extract p.offset.byteIdx s.utf8ByteSize := by
+  simp [h.eq_append, h.offset_eq_rawEndPos, ByteArray.extract_append_eq_right]
+
 theorem ValidPos.Splits.eq_left {s : String} {p : s.ValidPos} {t₁ t₂ t₃ t₄}
-    (h₁ : p.Splits t₁ t₂) (h₂ : p.Splits t₃ t₄) : t₁ = t₃ := sorry
+    (h₁ : p.Splits t₁ t₂) (h₂ : p.Splits t₃ t₄) : t₁ = t₃ := by
+  rw [← String.bytes_inj, h₁.bytes_left_eq, h₂.bytes_left_eq]
 
 theorem ValidPos.Splits.eq_right {s : String} {p : s.ValidPos} {t₁ t₂ t₃ t₄}
-    (h₁ : p.Splits t₁ t₂) (h₂ : p.Splits t₃ t₄) : t₂ = t₄ := sorry
+    (h₁ : p.Splits t₁ t₂) (h₂ : p.Splits t₃ t₄) : t₂ = t₄ := by
+  rw [← String.bytes_inj, h₁.bytes_right_eq, h₂.bytes_right_eq]
+
+theorem ValidPos.Splits.eq {s : String} {p : s.ValidPos} {t₁ t₂ t₃ t₄}
+    (h₁ : p.Splits t₁ t₂) (h₂ : p.Splits t₃ t₄) : t₁ = t₃ ∧ t₂ = t₄ :=
+  ⟨h₁.eq_left h₂, h₁.eq_right h₂⟩
 
 @[simp]
 theorem splits_endValidPos (s : String) : s.endValidPos.Splits s "" where
@@ -111,9 +125,43 @@ theorem splits_startValidPos (s : String) : s.startValidPos.Splits "" s where
   offset_eq_rawEndPos := by simp
 
 theorem ValidPos.splits_next_right {s : String} (p : s.ValidPos) (hp : p ≠ s.endValidPos) :
-    p.Splits (s.replaceEnd p).copy (singleton (p.get hp) ++ (s.replaceStart (p.next hp)).copy) := sorry
+    p.Splits (s.replaceEnd p).copy (singleton (p.get hp) ++ (s.replaceStart (p.next hp)).copy) where
+  eq_append := by simpa [← append_assoc] using p.eq_copy_replaceEnd_append_get hp
+  offset_eq_rawEndPos := by simp
 
 theorem ValidPos.splits_next {s : String} (p : s.ValidPos) (hp : p ≠ s.endValidPos) :
-    (p.next hp).Splits ((s.replaceEnd p).copy ++ singleton (p.get hp)) (s.replaceStart (p.next hp)).copy := sorry
+    (p.next hp).Splits ((s.replaceEnd p).copy ++ singleton (p.get hp)) (s.replaceStart (p.next hp)).copy where
+  eq_append := p.eq_copy_replaceEnd_append_get hp
+  offset_eq_rawEndPos := by simp
+
+theorem ValidPos.Splits.exists_eq_singleton_append {s : String} {p : s.ValidPos}
+    (hp : p ≠ s.endValidPos) (h : p.Splits t₁ t₂) : ∃ t₂', t₂ = singleton (p.get hp) ++ t₂' :=
+  ⟨(s.replaceStart (p.next hp)).copy, h.eq_right (p.splits_next_right hp)⟩
+
+theorem ValidPos.Splits.exists_eq_append_singleton {s : String} {p : s.ValidPos}
+    (hp : p ≠ s.endValidPos) (h : (p.next hp).Splits t₁ t₂) : ∃ t₁', t₁ = t₁' ++ singleton (p.get hp) :=
+  ⟨(s.replaceEnd p).copy, h.eq_left (p.splits_next hp)⟩
+
+-- TODO: move
+@[simp]
+theorem singleton_append_inj : singleton c ++ s = singleton d ++ t ↔ c = d ∧ s = t := by
+  simp [← toList_inj]
+
+-- TODO: move
+@[simp]
+theorem _root_.List.append_singleton_inj {l m : List α} : l ++ [a] = m ++ [b] ↔ l = m ∧ a = b := by
+  rw [← List.reverse_inj, And.comm]; simp
+
+-- TODO: move
+@[simp]
+theorem push_append_inj : push s c = push t d ↔ s = t ∧ c = d := by
+  simp [← toList_inj]
+
+-- TODO: `hp` actually follows from `h`.
+/-- You might want to invoke `ValidPos.Splits.exists_eq_singleton_append` to be able to apply this. -/
+theorem ValidPos.Splits.next {s : String} {p : s.ValidPos} (h : p.Splits t₁ (singleton c ++ t₂))
+    (hp : p ≠ s.endValidPos) : (p.next hp).Splits (t₁ ++ singleton c) t₂ := by
+  obtain ⟨rfl, rfl, rfl⟩ := by simpa using h.eq (splits_next_right p hp)
+  exact splits_next p hp
 
 end String