feat: lemmas about String.Pos.nextn (#13106)

This PR verifies `String.Pos.nextn` by providing the low-level API
`nextn_zero`/`nextn_add_one` as well as a `Splits` lemma.

The `Splits` lemma trivially implies, for a string `s`, the statement
`(s.drop n).copy.toList = s.toList.drop n`, to be included in a later
PR.

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

@@ -7,6 +7,7 @@ module
 
 prelude
 public import Init.Data.String.Basic
+import all Init.Data.String.Basic
 import Init.Data.ByteArray.Lemmas
 import Init.Data.Nat.MinMax
 
@@ -56,6 +57,11 @@ theorem singleton_ne_empty {c : Char} : singleton c ≠ "" := by
 theorem empty_ne_singleton {c : Char} : "" ≠ singleton c := by
   simp
 
+@[simp]
+theorem ofList_cons {c : Char} {l : List Char} :
+    String.ofList (c :: l) = String.singleton c ++ String.ofList l := by
+  simp [← toList_inj]
+
 @[simp]
 theorem Slice.Pos.copy_inj {s : Slice} {p₁ p₂ : s.Pos} : p₁.copy = p₂.copy ↔ p₁ = p₂ := by
   simp [String.Pos.ext_iff, Pos.ext_iff]
@@ -244,4 +250,46 @@ theorem Pos.get_ofToSlice {s : String} {p : (s.toSlice).Pos} {h} :
 @[simp]
 theorem push_empty {c : Char} : "".push c = singleton c := rfl
 
+namespace Slice.Pos
+
+@[simp]
+theorem nextn_zero {s : Slice} {p : s.Pos} : p.nextn 0 = p := by
+  simp [nextn]
+
+theorem nextn_add_one {s : Slice} {p : s.Pos} :
+    p.nextn (n + 1) = if h : p = s.endPos then p else (p.next h).nextn n := by
+  simp [nextn]
+
+@[simp]
+theorem nextn_endPos {s : Slice} : s.endPos.nextn n = s.endPos := by
+  cases n <;> simp [nextn_add_one]
+
+end Slice.Pos
+
+namespace Pos
+
+theorem nextn_eq_nextn_toSlice {s : String} {p : s.Pos} : p.nextn n = Pos.ofToSlice (p.toSlice.nextn n) :=
+  (rfl)
+
+@[simp]
+theorem nextn_zero {s : String} {p : s.Pos} : p.nextn 0 = p := by
+  simp [nextn_eq_nextn_toSlice]
+
+theorem nextn_add_one {s : String} {p : s.Pos} :
+    p.nextn (n + 1) = if h : p = s.endPos then p else (p.next h).nextn n := by
+  simp only [nextn_eq_nextn_toSlice, Slice.Pos.nextn_add_one, endPos_toSlice, toSlice_inj]
+  split <;> simp [Pos.next_toSlice]
+
+theorem nextn_toSlice {s : String} {p : s.Pos} : p.toSlice.nextn n = (p.nextn n).toSlice := by
+  induction n generalizing p with simp_all [nextn_add_one, Slice.Pos.nextn_add_one, apply_dite Pos.toSlice, next_toSlice]
+
+theorem toSlice_nextn {s : String} {p : s.Pos} : (p.nextn n).toSlice = p.toSlice.nextn n :=
+  nextn_toSlice.symm
+
+@[simp]
+theorem nextn_endPos {s : String} : s.endPos.nextn n = s.endPos := by
+  cases n <;> simp [nextn_add_one]
+
+end Pos
+
 end String

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

@@ -496,4 +496,46 @@ theorem Pos.prev?_eq_none {s : String} {p : s.Pos} (h : p = s.startPos) : p.prev
 theorem Pos.prev?_startPos {s : String} : s.startPos.prev? = none := by
   simp
 
+namespace Slice.Pos
+
+@[simp]
+theorem prevn_zero {s : Slice} {p : s.Pos} : p.prevn 0 = p := by
+  simp [prevn]
+
+theorem prevn_add_one {s : Slice} {p : s.Pos} :
+    p.prevn (n + 1) = if h : p = s.startPos then p else (p.prev h).prevn n := by
+  simp [prevn]
+
+@[simp]
+theorem prevn_startPos {s : Slice} : s.startPos.prevn n = s.startPos := by
+  cases n <;> simp [prevn_add_one]
+
+end Slice.Pos
+
+namespace Pos
+
+theorem prevn_eq_prevn_toSlice {s : String} {p : s.Pos} : p.prevn n = Pos.ofToSlice (p.toSlice.prevn n) :=
+  (rfl)
+
+@[simp]
+theorem prevn_zero {s : String} {p : s.Pos} : p.prevn 0 = p := by
+  simp [prevn_eq_prevn_toSlice]
+
+theorem prevn_add_one {s : String} {p : s.Pos} :
+    p.prevn (n + 1) = if h : p = s.startPos then p else (p.prev h).prevn n := by
+  simp only [prevn_eq_prevn_toSlice, Slice.Pos.prevn_add_one, startPos_toSlice, toSlice_inj]
+  split <;> simp [Pos.prev_toSlice]
+
+theorem prevn_toSlice {s : String} {p : s.Pos} : p.toSlice.prevn n = (p.prevn n).toSlice := by
+  induction n generalizing p with simp_all [prevn_add_one, Slice.Pos.prevn_add_one, apply_dite Pos.toSlice, prev_toSlice]
+
+theorem toSlice_prevn {s : String} {p : s.Pos} : (p.prevn n).toSlice = p.toSlice.prevn n :=
+  prevn_toSlice.symm
+
+@[simp]
+theorem prevn_startPos {s : String} : s.startPos.prevn n = s.startPos := by
+  cases n <;> simp [prevn_add_one]
+
+end Pos
+
 end String

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

@@ -17,6 +17,8 @@ import Init.Data.String.OrderInstances
 import Init.Data.Nat.Order
 import Init.Omega
 import Init.Data.String.Lemmas.FindPos
+import Init.Data.List.TakeDrop
+import Init.Data.List.Nat.TakeDrop
 
 /-!
 # `Splits` predicates on `String.Pos` and `String.Slice.Pos`.
@@ -649,4 +651,51 @@ theorem Slice.splits_slice {s : Slice} {p₀ p₁ : s.Pos} (h) (p : (s.slice p
     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.Pos.Splits.nextn {s : Slice} {t₁ t₂ : String} {p : s.Pos} (h : p.Splits t₁ t₂) (n : Nat) :
+    (p.nextn n).Splits (t₁ ++ String.ofList (t₂.toList.take n)) (String.ofList (t₂.toList.drop n)) := by
+  induction n generalizing p t₁ t₂ with
+  | zero => simpa
+  | succ n ih =>
+    rw [Pos.nextn_add_one]
+    split
+    · simp_all
+    · obtain ⟨t₂, rfl⟩ := h.exists_eq_singleton_append ‹_›
+      simpa [← append_assoc] using ih h.next
+
+theorem Slice.splits_nextn_startPos (s : Slice) (n : Nat) :
+    (s.startPos.nextn n).Splits (String.ofList (s.copy.toList.take n)) (String.ofList (s.copy.toList.drop n)) := by
+  simpa using s.splits_startPos.nextn n
+
+theorem Pos.Splits.nextn {s t₁ t₂ : String} {p : s.Pos} (h : p.Splits t₁ t₂) (i : Nat) :
+    (p.nextn i).Splits (t₁ ++ String.ofList (t₂.toList.take i)) (String.ofList (t₂.toList.drop i)) := by
+  simpa [← splits_toSlice_iff, toSlice_nextn] using h.toSlice.nextn i
+
+theorem splits_nextn_startPos (s : String) (n : Nat) :
+    (s.startPos.nextn n).Splits (String.ofList (s.toList.take n)) (String.ofList (s.toList.drop n)) := by
+  simpa using s.splits_startPos.nextn n
+
+theorem Slice.Pos.Splits.prevn {s : Slice} {t₁ t₂ : String} {p : s.Pos} (h : p.Splits t₁ t₂) (n : Nat) :
+    (p.prevn n).Splits (String.ofList (t₁.toList.take (t₁.length - n))) (String.ofList (t₁.toList.drop (t₁.length - n)) ++ t₂) := by
+  induction n generalizing p t₁ t₂ with
+  | zero => simpa [← String.length_toList]
+  | succ n ih =>
+    rw [Pos.prevn_add_one]
+    split
+    · simp_all
+    · obtain ⟨t₂, rfl⟩ := h.exists_eq_append_singleton_of_ne_startPos ‹_›
+      simpa [Nat.add_sub_add_right, List.take_append, List.drop_append, ← append_assoc] using ih h.prev
+
+theorem Slice.splits_prevn_endPos (s : Slice) (n : Nat) :
+    (s.endPos.prevn n).Splits (String.ofList (s.copy.toList.take (s.copy.length - n)))
+      (String.ofList (s.copy.toList.drop (s.copy.length - n))) := by
+  simpa using s.splits_endPos.prevn n
+
+theorem Pos.Splits.prevn {s t₁ t₂ : String} {p : s.Pos} (h : p.Splits t₁ t₂) (n : Nat) :
+    (p.prevn n).Splits (String.ofList (t₁.toList.take (t₁.length - n))) (String.ofList (t₁.toList.drop (t₁.length - n)) ++ t₂) := by
+  simpa [← splits_toSlice_iff, toSlice_prevn] using h.toSlice.prevn n
+
+theorem splits_prevn_endPos (s : String) (n : Nat) :
+    (s.endPos.prevn n).Splits (String.ofList (s.toList.take (s.length - n))) (String.ofList (s.toList.drop (s.length - n))) := by
+  simpa using s.splits_endPos.prevn n
+
 end String