chore: rename String.ValidPos to String.Pos (#11240)

This PR renames `String.ValidPos` to `String.Pos`, `String.endValidPos`
to `String.endPos` and `String.startValidPos` to `String.startPos`.

Accordingly, the deprecations of `String.Pos` to `String.Pos.Raw` and
`String.endPos` to `String.rawEndPos` are removed early, after an
abbreviated deprecation cycle of two releases.

Author: TwoFX

script/Shake.lean

@@ -300,7 +300,7 @@ def parseHeaderFromString (text path : String) :
     throw <| .userError "parse errors in file"
   -- the insertion point for `add` is the first newline after the imports
   let insertion := header.raw.getTailPos?.getD parserState.pos
-  let insertion := text.findAux (· == '\n') text.endPos insertion + '\n'
+  let insertion := text.findAux (· == '\n') text.rawEndPos insertion + '\n'
   pure (path, inputCtx, header, insertion)
 
 /-- Parse a source file to extract the location of the import lines, for edits and error messages.
@@ -593,16 +593,16 @@ def main (args : List String) : IO UInt32 := do
     for stx in imports do
       let mod := decodeImport stx
       if remove.contains mod || seen.contains mod then
-        out := out ++ text.extract pos stx.raw.getPos?.get!
+        out := out ++ String.Pos.Raw.extract text pos stx.raw.getPos?.get!
         -- We use the end position of the syntax, but include whitespace up to the first newline
         pos := text.findAux (· == '\n') text.rawEndPos stx.raw.getTailPos?.get! + '\n'
       seen := seen.insert mod
-    out := out ++ text.extract pos insertion
+    out := out ++ String.Pos.Raw.extract text pos insertion
     for mod in add do
       if !seen.contains mod then
         seen := seen.insert mod
         out := out ++ s!"{mod}\n"
-    out := out ++ text.extract insertion text.rawEndPos
+    out := out ++ String.Pos.Raw.extract text insertion text.rawEndPos
 
     IO.FS.writeFile path out
     count := count + 1

src/Init/Data/String/Basic.lean

@@ -13,9 +13,6 @@ public section
 
 namespace String
 
-@[deprecated Pos.Raw (since := "2025-09-30")]
-abbrev Pos := Pos.Raw
-
 instance : OfNat String.Pos.Raw (nat_lit 0) where
   ofNat := {}
 

src/Init/Data/String/Bootstrap.lean

@@ -142,10 +142,6 @@ theorem String.bytes_push {s : String} {c : Char} : (s.push c).bytes = s.bytes +
 
 namespace String
 
-@[deprecated rawEndPos (since := "2025-10-20")]
-def endPos (s : String) : String.Pos.Raw :=
-  s.rawEndPos
-
 /-- The start position of the string, as a `String.Pos.Raw.` -/
 def rawStartPos (_s : String) : String.Pos.Raw :=
   0
@@ -341,55 +337,55 @@ theorem Pos.Raw.isValid_empty_iff {p : Pos.Raw} : p.IsValid "" ↔ p = 0 := by
     simp
 
 /--
-A `ValidPos s` is a byte offset in `s` together with a proof that this position is at a UTF-8
+A `Pos s` is a byte offset in `s` together with a proof that this position is at a UTF-8
 character boundary.
 -/
 @[ext]
-structure ValidPos (s : String) where
-  /-- The underlying byte offset of the `ValidPos`. -/
+structure Pos (s : String) where
+  /-- The underlying byte offset of the `Pos`. -/
   offset : Pos.Raw
   /-- The proof that `offset` is valid for the string `s`. -/
   isValid : offset.IsValid s
 deriving @[expose] DecidableEq
 
-/-- The start position of `s`, as an `s.ValidPos`. -/
+/-- The start position of `s`, as an `s.Pos`. -/
 @[inline, expose]
-def startValidPos (s : String) : s.ValidPos where
+def startPos (s : String) : s.Pos where
   offset := 0
   isValid := by simp
 
 @[simp]
-theorem offset_startValidPos {s : String} : s.startValidPos.offset = 0 := (rfl)
+theorem offset_startPos {s : String} : s.startPos.offset = 0 := (rfl)
 
-instance {s : String} : Inhabited s.ValidPos where
-  default := s.startValidPos
+instance {s : String} : Inhabited s.Pos where
+  default := s.startPos
 
-/-- The past-the-end position of `s`, as an `s.ValidPos`. -/
+/-- The past-the-end position of `s`, as an `s.Pos`. -/
 @[inline, expose]
-def endValidPos (s : String) : s.ValidPos where
+def endPos (s : String) : s.Pos where
   offset := s.rawEndPos
   isValid := by simp
 
 @[simp]
-theorem offset_endValidPos {s : String} : s.endValidPos.offset = s.rawEndPos := (rfl)
+theorem offset_endPos {s : String} : s.endPos.offset = s.rawEndPos := (rfl)
 
-instance {s : String} : LE s.ValidPos where
+instance {s : String} : LE s.Pos where
   le l r := l.offset ≤ r.offset
 
-instance {s : String} : LT s.ValidPos where
+instance {s : String} : LT s.Pos where
   lt l r := l.offset < r.offset
 
-theorem ValidPos.le_iff {s : String} {l r : s.ValidPos} : l ≤ r ↔ l.offset ≤ r.offset :=
+theorem Pos.le_iff {s : String} {l r : s.Pos} : l ≤ r ↔ l.offset ≤ r.offset :=
   Iff.rfl
 
-theorem ValidPos.lt_iff {s : String} {l r : s.ValidPos} : l < r ↔ l.offset < r.offset :=
+theorem Pos.lt_iff {s : String} {l r : s.Pos} : l < r ↔ l.offset < r.offset :=
   Iff.rfl
 
-instance {s : String} (l r : s.ValidPos) : Decidable (l ≤ r) :=
-  decidable_of_iff' _ ValidPos.le_iff
+instance {s : String} (l r : s.Pos) : Decidable (l ≤ r) :=
+  decidable_of_iff' _ Pos.le_iff
 
-instance {s : String} (l r : s.ValidPos) : Decidable (l < r) :=
-decidable_of_iff' _ ValidPos.lt_iff
+instance {s : String} (l r : s.Pos) : Decidable (l < r) :=
+decidable_of_iff' _ Pos.lt_iff
 
 /--
 A region or slice of some underlying string.
@@ -406,30 +402,30 @@ structure Slice where
   /-- The underlying strings. -/
   str : String
   /-- The byte position of the start of the string slice. -/
-  startInclusive : str.ValidPos
+  startInclusive : str.Pos
   /-- The byte position of the end of the string slice. -/
-  endExclusive : str.ValidPos
+  endExclusive : str.Pos
   /-- The slice is not degenerate (but it may be empty). -/
   startInclusive_le_endExclusive : startInclusive ≤ endExclusive
 
 instance : Inhabited Slice where
-  default := ⟨"", "".startValidPos, "".startValidPos, by simp [ValidPos.le_iff]⟩
+  default := ⟨"", "".startPos, "".startPos, by simp [Pos.le_iff]⟩
 
 /--
 Returns a slice that contains the entire string.
 -/
 @[inline, expose] -- expose for the defeq `s.toSlice.str = s`.
 def toSlice (s : String) : Slice where
   str := s
-  startInclusive := s.startValidPos
-  endExclusive := s.endValidPos
-  startInclusive_le_endExclusive := by simp [ValidPos.le_iff, Pos.Raw.le_iff]
+  startInclusive := s.startPos
+  endExclusive := s.endPos
+  startInclusive_le_endExclusive := by simp [Pos.le_iff, Pos.Raw.le_iff]
 
 @[simp]
-theorem startInclusive_toSlice {s : String} : s.toSlice.startInclusive = s.startValidPos := rfl
+theorem startInclusive_toSlice {s : String} : s.toSlice.startInclusive = s.startPos := rfl
 
 @[simp]
-theorem endExclusive_toSlice {s : String} : s.toSlice.endExclusive = s.endValidPos := rfl
+theorem endExclusive_toSlice {s : String} : s.toSlice.endExclusive = s.endPos := rfl
 
 @[simp]
 theorem str_toSlice {s : String} : s.toSlice.str = s := rfl
@@ -532,7 +528,7 @@ instance {s : Slice} : Inhabited s.Pos where
 theorem Slice.offset_startInclusive_add_self {s : Slice} :
     s.startInclusive.offset + s = s.endExclusive.offset := by
   have := s.startInclusive_le_endExclusive
-  simp_all [String.Pos.Raw.ext_iff, ValidPos.le_iff, Pos.Raw.le_iff, utf8ByteSize_eq]
+  simp_all [String.Pos.Raw.ext_iff, Pos.le_iff, Pos.Raw.le_iff, utf8ByteSize_eq]
 
 @[simp]
 theorem Pos.Raw.offsetBy_rawEndPos_left {p : Pos.Raw} {s : String} :
@@ -591,18 +587,18 @@ instance {s : Slice} (l r : s.Pos) : Decidable (l < r) :=
   decidable_of_iff' _ Slice.Pos.lt_iff
 
 /--
-`pos.IsAtEnd` is just shorthand for `pos = s.endValidPos` that is easier to write if `s` is long.
+`pos.IsAtEnd` is just shorthand for `pos = s.endPos` that is easier to write if `s` is long.
 -/
-abbrev ValidPos.IsAtEnd {s : String} (pos : s.ValidPos) : Prop :=
-  pos = s.endValidPos
+abbrev Pos.IsAtEnd {s : String} (pos : s.Pos) : Prop :=
+  pos = s.endPos
 
 @[simp]
-theorem ValidPos.isAtEnd_iff {s : String} {pos : s.ValidPos} :
-    pos.IsAtEnd ↔ pos = s.endValidPos := Iff.rfl
+theorem Pos.isAtEnd_iff {s : String} {pos : s.Pos} :
+    pos.IsAtEnd ↔ pos = s.endPos := Iff.rfl
 
 @[inline]
-instance {s : String} {pos : s.ValidPos} : Decidable pos.IsAtEnd :=
-  decidable_of_iff _ ValidPos.isAtEnd_iff
+instance {s : String} {pos : s.Pos} : Decidable pos.IsAtEnd :=
+  decidable_of_iff _ Pos.isAtEnd_iff
 
 /--
 `pos.IsAtEnd` is just shorthand for `pos = s.endPos` that is easier to write if `s` is long.
@@ -639,4 +635,16 @@ def toSubstring (s : String) : Substring.Raw :=
 def toSubstring' (s : String) : Substring.Raw :=
   s.toRawSubstring'
 
+@[deprecated String.Pos (since := "2025-11-24")]
+abbrev ValidPos (s : String) : Type :=
+  s.Pos
+
+@[deprecated String.startPos (since := "2025-11-24")]
+abbrev startValidPos (s : String) : s.Pos :=
+  s.startPos
+
+@[deprecated String.endPos (since := "2025-11-24")]
+abbrev endValidPos (s : String) : s.Pos :=
+  s.endPos
+
 end String

src/Init/Data/String/Defs.lean

@@ -29,36 +29,36 @@ abbrev validateUTF8 (a : ByteArray) : Bool :=
   a.validateUTF8
 
 private def findLeadingSpacesSize (s : String) : Nat :=
-  let it := s.startValidPos
-  let it := it.find? (· == '\n') |>.bind String.ValidPos.next?
+  let it := s.startPos
+  let it := it.find? (· == '\n') |>.bind String.Pos.next?
   match it with
   | some it => consumeSpaces it 0 s.length
   | none => 0
 where
-  consumeSpaces {s : String} (it : s.ValidPos) (curr min : Nat) : Nat :=
+  consumeSpaces {s : String} (it : s.Pos) (curr min : Nat) : Nat :=
     if h : it.IsAtEnd then min
     else if it.get h == ' ' || it.get h == '\t' then consumeSpaces (it.next h) (curr + 1) min
     else if it.get h == '\n' then findNextLine (it.next h) min
     else findNextLine (it.next h) (Nat.min curr min)
   termination_by it
-  findNextLine {s : String} (it : s.ValidPos) (min : Nat) : Nat :=
+  findNextLine {s : String} (it : s.Pos) (min : Nat) : Nat :=
     if h : it.IsAtEnd then min
     else if it.get h == '\n' then consumeSpaces (it.next h) 0 min
     else findNextLine (it.next h) min
   termination_by it
 
 private def removeNumLeadingSpaces (n : Nat) (s : String) : String :=
-  consumeSpaces n s.startValidPos ""
+  consumeSpaces n s.startPos ""
 where
-  consumeSpaces (n : Nat) {s : String} (it : s.ValidPos) (r : String) : String :=
+  consumeSpaces (n : Nat) {s : String} (it : s.Pos) (r : String) : String :=
      match n with
      | 0 => saveLine it r
      | n+1 =>
        if h : it.IsAtEnd then r
        else if it.get h == ' ' || it.get h == '\t' then consumeSpaces n (it.next h) r
        else saveLine it r
   termination_by (it, 1)
-  saveLine {s : String} (it : s.ValidPos) (r : String) : String :=
+  saveLine {s : String} (it : s.Pos) (r : String) : String :=
     if h : it.IsAtEnd then r
     else if it.get h  == '\n' then consumeSpaces n (it.next h) (r.push '\n')
     else saveLine (it.next h) (r.push (it.get h))

src/Init/Data/String/Extra.lean

@@ -25,9 +25,9 @@ An iterator over the characters (Unicode code points) in a `String`. Typically c
 `String.iter`.
 
 This is a no-longer-supported legacy API that will be removed in a future release. You should use
-`String.ValidPos` instead, which is similar, but safer. To iterate over a string `s`, start with
-`p : s.startValidPos`, advance it using `p.next`, access the current character using `p.get` and
-check if the position is at the end using `p = s.endValidPos` or `p.IsAtEnd`.
+`String.Pos` instead, which is similar, but safer. To iterate over a string `s`, start with
+`p : s.startPos`, advance it using `p.next`, access the current character using `p.get` and
+check if the position is at the end using `p = s.endPos` or `p.IsAtEnd`.
 
 String iterators pair a string with a valid byte index. This allows efficient character-by-character
 processing of strings while avoiding the need to manually ensure that byte indices are used with the
@@ -57,9 +57,9 @@ structure Iterator where
 /-- Creates an iterator at the beginning of the string.
 
 This is a no-longer-supported legacy API that will be removed in a future release. You should use
-`String.ValidPos` instead, which is similar, but safer. To iterate over a string `s`, start with
-`p : s.startValidPos`, advance it using `p.next`, access the current character using `p.get` and
-check if the position is at the end using `p = s.endValidPos` or `p.IsAtEnd`.
+`String.Pos` instead, which is similar, but safer. To iterate over a string `s`, start with
+`p : s.startPos`, advance it using `p.next`, access the current character using `p.get` and
+check if the position is at the end using `p = s.endPos` or `p.IsAtEnd`.
 -/
 @[inline] def mkIterator (s : String) : Iterator :=
   ⟨s, 0⟩
@@ -95,9 +95,9 @@ def pos := Iterator.i
 Gets the character at the iterator's current position.
 
 This is a no-longer-supported legacy API that will be removed in a future release. You should use
-`String.ValidPos` instead, which is similar, but safer. To iterate over a string `s`, start with
-`p : s.startValidPos`, advance it using `p.next`, access the current character using `p.get` and
-check if the position is at the end using `p = s.endValidPos` or `p.IsAtEnd`.
+`String.Pos` instead, which is similar, but safer. To iterate over a string `s`, start with
+`p : s.startPos`, advance it using `p.next`, access the current character using `p.get` and
+check if the position is at the end using `p = s.endPos` or `p.IsAtEnd`.
 
 A run-time bounds check is performed. Use `String.Iterator.curr'` to avoid redundant bounds checks.
 
@@ -110,9 +110,9 @@ If the position is invalid, returns `(default : Char)`.
 Moves the iterator's position forward by one character, unconditionally.
 
 This is a no-longer-supported legacy API that will be removed in a future release. You should use
-`String.ValidPos` instead, which is similar, but safer. To iterate over a string `s`, start with
-`p : s.startValidPos`, advance it using `p.next`, access the current character using `p.get` and
-check if the position is at the end using `p = s.endValidPos` or `p.IsAtEnd`.
+`String.Pos` instead, which is similar, but safer. To iterate over a string `s`, start with
+`p : s.startPos`, advance it using `p.next`, access the current character using `p.get` and
+check if the position is at the end using `p = s.endPos` or `p.IsAtEnd`.
 
 It is only valid to call this function if the iterator is not at the end of the string (i.e.
 if `Iterator.atEnd` is `false`); otherwise, the resulting iterator will be invalid.

src/Init/Data/String/Iterator.lean

@@ -41,11 +41,11 @@ theorem singleton_ne_empty {c : Char} : singleton c ≠ "" := by
 
 @[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]
+  simp [String.Pos.ext_iff, Pos.ext_iff]
 
 @[simp]
-theorem ValidPos.startValidPos_le {s : String} (p : s.ValidPos) : s.startValidPos ≤ p := by
-  simp [ValidPos.le_iff, Pos.Raw.le_iff]
+theorem Pos.startPos_le {s : String} (p : s.Pos) : s.startPos ≤ p := by
+  simp [Pos.le_iff, Pos.Raw.le_iff]
 
 @[simp]
 theorem Slice.Pos.startPos_le {s : Slice} (p : s.Pos) : s.startPos ≤ p := by

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

@@ -22,22 +22,22 @@ 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}
+/-- You might want to invoke `Pos.Splits.exists_eq_singleton_append` to be able to apply this. -/
+theorem Pos.Splits.pastSet {s : String} {p : s.Pos} {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
+    (p.pastSet d h.ne_endPos_of_singleton).Splits (t₁ ++ singleton d) t₂ := by
+  generalize h.ne_endPos_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}
+/-- You might want to invoke `Pos.Splits.exists_eq_singleton_append` to be able to apply this. -/
+theorem Pos.Splits.pastModify {s : String} {p : s.Pos} {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₂ :=
+    (p.pastModify f h.ne_endPos_of_singleton).Splits
+    (t₁ ++ singleton (f (p.get h.ne_endPos_of_singleton))) t₂ :=
   h.pastSet
 
-theorem toList_mapAux {f : Char → Char} {s : String} {p : s.ValidPos}
+theorem toList_mapAux {f : Char → Char} {s : String} {p : s.Pos}
     (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
@@ -47,7 +47,7 @@ theorem toList_mapAux {f : Char → Char} {s : String} {p : s.ValidPos}
 
 @[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 [map, toList_mapAux s.splits_startPos]
 
 @[simp]
 theorem length_map {f : Char → Char} {s : String} : (s.map f).length = s.length := by