feat: verification of String.toInt? (#13003)

This PR reorganizes the instances `ToString Int` and `Repr Int` so that
they both point at a common definition `Int.repr` (the same setup is
used for `Nat`). It then verifies the functions `Int.repr`,
`String.isInt` and `String.toInt`.

In particular, for `a : Int` we get `a.repr.toInt? = some a`, which
implies that `Int.repr` is injective.

src/Init/Data/Int.lean

@@ -18,3 +18,4 @@ public import Init.Data.Int.Pow
 public import Init.Data.Int.Cooper
 public import Init.Data.Int.Linear
 public import Init.Data.Int.OfNat
+public import Init.Data.Int.ToString

src/Init/Data/Int/Repr.lean

@@ -0,0 +1,24 @@
+/-
+Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Leonardo de Moura
+-/
+module
+
+prelude
+public import Init.Data.Repr
+public import Init.Data.String.Defs
+
+namespace Int
+
+/--
+Returns the decimal string representation of an integer.
+-/
+public protected def repr : Int → String
+  | ofNat m   => Nat.repr m
+  | negSucc m => "-" ++ Nat.repr (Nat.succ m)
+
+public instance : Repr Int where
+  reprPrec i prec := if i < 0 then Repr.addAppParen i.repr prec else i.repr
+
+end Int

src/Init/Data/Int/ToString.lean

@@ -0,0 +1,23 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Julia Markus Himmel
+-/
+module
+
+prelude
+public import Init.Data.ToString.Extra
+import all Init.Data.Int.Repr
+import Init.Data.Int.Order
+import Init.Data.Int.LemmasAux
+
+namespace Int
+
+public theorem repr_eq_if {a : Int} :
+    a.repr = if 0 ≤ a then a.toNat.repr else "-" ++ (-a).toNat.repr := by
+  cases a <;> simp [Int.repr]
+
+@[simp]
+public theorem toString_eq_repr {a : Int} : toString a = a.repr := (rfl)
+
+end Int

src/Init/Data/Repr.lean

@@ -354,16 +354,6 @@ end Nat
 instance : Repr Nat where
   reprPrec n _ := Nat.repr n
 
-/--
-Returns the decimal string representation of an integer.
--/
-protected def Int.repr : Int → String
-    | ofNat m   => Nat.repr m
-    | negSucc m => String.Internal.append "-" (Nat.repr (succ m))
-
-instance : Repr Int where
-  reprPrec i prec := if i < 0 then Repr.addAppParen i.repr prec else i.repr
-
 def hexDigitRepr (n : Nat) : String :=
   String.singleton <| Nat.digitChar n
 

src/Init/Data/String/Lemmas/Pattern/TakeDrop/Char.lean

@@ -40,6 +40,16 @@ theorem startsWith_char_eq_head? {c : Char} {s : Slice} :
   simp only [← toList_inj, toList_append, toList_singleton, List.cons_append, List.nil_append]
   cases h : s.copy.toList <;> simp_all [← ofList_inj]
 
+theorem startsWith_char_iff_exists_append {c : Char} {s : Slice} :
+    s.startsWith c ↔ ∃ t, s.copy = singleton c ++ t := by
+  simp only [startsWith_char_eq_head?, beq_iff_eq, List.head?_eq_some_iff, ← toList_inj,
+    toList_append, toList_singleton, List.cons_append, List.nil_append]
+  exact ⟨fun ⟨t, ht⟩ => ⟨ofList t, by simp [ht]⟩, fun ⟨t, ht⟩ => ⟨t.toList, by simp [ht]⟩⟩
+
+theorem startsWith_char_eq_false_iff_forall_append {c : Char} {s : Slice} :
+    s.startsWith c = false ↔ ∀ t, s.copy ≠ singleton c ++ t := by
+  simp [← Bool.not_eq_true, startsWith_char_iff_exists_append]
+
 theorem eq_append_of_dropPrefix?_char_eq_some {c : Char} {s res : Slice} (h : s.dropPrefix? c = some res) :
     s.copy = singleton c ++ res.copy := by
   simpa [ForwardPatternModel.Matches] using Pattern.Model.eq_append_of_dropPrefix?_eq_some h
@@ -63,6 +73,14 @@ theorem startsWith_char_eq_head? {c : Char} {s : String} :
     s.startsWith c = (s.toList.head? == some c) := by
   simp [startsWith_eq_startsWith_toSlice, Slice.startsWith_char_eq_head?]
 
+theorem startsWith_char_iff_exists_append {c : Char} {s : String} :
+    s.startsWith c ↔ ∃ t, s = singleton c ++ t := by
+  simp [startsWith_eq_startsWith_toSlice, Slice.startsWith_char_iff_exists_append]
+
+theorem startsWith_char_eq_false_iff_forall_append {c : Char} {s : String} :
+    s.startsWith c = false ↔ ∀ t, s ≠ singleton c ++ t := by
+  simp [← Bool.not_eq_true, startsWith_char_iff_exists_append]
+
 theorem eq_append_of_dropPrefix?_char_eq_some {c : Char} {s : String} {res : Slice} (h : s.dropPrefix? c = some res) :
     s = singleton c ++ res.copy := by
   rw [dropPrefix?_eq_dropPrefix?_toSlice] at h

src/Init/Data/String/Slice.lean

@@ -945,7 +945,6 @@ Examples:
  * {lean}`"123_".toSlice.isNat = false`
  * {lean}`"12__34".toSlice.isNat = false`
 -/
-@[inline]
 def isNat (s : Slice) : Bool := Id.run do
   let mut lastWasDigit := false
 
@@ -1054,12 +1053,13 @@ Examples:
  * {lean}`" 5".toSlice.isInt = false`
  * {lean}`"2-3".toSlice.isInt = false`
  * {lean}`"0xff".toSlice.isInt = false`
+ * {lean}`"-0_1".toSlice.isInt = true`
+ * {lean}`"-_1".toSlice.isInt = false`
 -/
 def isInt (s : Slice) : Bool :=
-  if s.front = '-' then
-    (s.drop 1).isNat
-  else
-    s.isNat
+  match s.dropPrefix? '-' with
+  | some rest => rest.isNat
+  | none => s.isNat
 
 /--
 Interprets a slice as the decimal representation of an integer, returning it. Returns {lean}`none` if
@@ -1083,12 +1083,13 @@ Examples:
  * {lean}`" 5".toSlice.toInt? = none`
  * {lean}`"2-3".toSlice.toInt? = none`
  * {lean}`"0xff".toSlice.toInt? = none`
+ * {lean}`"-0_1".toSlice.toInt? = some (-1)`
+ * {lean}`"-_1".toSlice.toInt? = none`
 -/
 def toInt? (s : Slice) : Option Int :=
-  if s.front = '-' then
-    Int.negOfNat <$> (s.drop 1).toNat?
-  else
-   Int.ofNat <$> s.toNat?
+  match s.dropPrefix? '-' with
+  | some rest => rest.toNat?.map Int.negOfNat
+  | none => s.toNat?.map Int.ofNat
 
 /--
 Interprets a string as the decimal representation of an integer, returning it. Panics if the string

src/Init/Data/ToString/Extra.lean

@@ -7,6 +7,7 @@ module
 
 prelude
 public import Init.Data.String.Defs
+public import Init.Data.Int.Repr
 
 public section
 
@@ -38,6 +39,4 @@ instance [ToString α] : ToString (Array α) where
 instance : ToString ByteArray := ⟨fun bs => bs.toList.toString⟩
 
 instance : ToString Int where
-  toString
-    | Int.ofNat m   => toString m
-    | Int.negSucc m => "-" ++ toString (m + 1)
+  toString := Int.repr

src/Init/Grind/Ordered/Linarith.lean

@@ -17,6 +17,7 @@ import Init.Data.Nat.Lemmas
 import Init.Grind.Ordered.Order
 import Init.Omega
 import Init.WFTactics
+import Init.Data.Int.Repr
 
 @[expose] public section
 

src/Init/Grind/Ring/CommSolver.lean

@@ -22,6 +22,7 @@ import Init.Data.Nat.Linear
 import Init.Grind.Ordered.Order
 import Init.Omega
 import Init.WFTactics
+import Init.Data.Int.Repr
 
 @[expose] public section
 

src/Init/Omega/Constraint.lean

@@ -36,6 +36,17 @@ abbrev LowerBound.sat (b : LowerBound) (t : Int) := b.all fun x => x ≤ t
 /-- A upper bound at `y` is satisfied at `t` if `t ≤ y`. -/
 abbrev UpperBound.sat (b : UpperBound) (t : Int) := b.all fun y => t ≤ y
 
+private local instance : Append String where
+  append := String.Internal.append
+
+private local instance : ToString Int where
+  toString
+    | Int.ofNat m   => toString m
+    | Int.negSucc m => "-" ++ toString (m + 1)
+
+private local instance : Repr Int where
+  reprPrec i prec := if i < 0 then Repr.addAppParen (toString i) prec else toString i
+
 /--
 A `Constraint` consists of an optional lower and upper bound (inclusive),
 constraining a value to a set of the form `∅`, `{x}`, `[x, y]`, `[x, ∞)`, `(-∞, y]`, or `(-∞, ∞)`.
@@ -49,14 +60,6 @@ deriving BEq, DecidableEq, Repr
 
 namespace Constraint
 
-private local instance : Append String where
-  append := String.Internal.append
-
-private local instance : ToString Int where
-  toString
-    | Int.ofNat m   => toString m
-    | Int.negSucc m => "-" ++ toString (m + 1)
-
 instance : ToString Constraint where
   toString := private fun
   | ⟨none, none⟩ => "(-∞, ∞)"

src/Init/Omega/LinearCombo.lean

@@ -25,6 +25,20 @@ We use this data structure while processing hypotheses.
 
 namespace Lean.Omega
 
+private local instance : Append String where
+  append := String.Internal.append
+
+private local instance : ToString Int where
+  toString
+    | Int.ofNat m   => toString m
+    | Int.negSucc m => "-" ++ toString (m + 1)
+
+private local instance : Repr Int where
+  reprPrec i prec := if i < 0 then Repr.addAppParen (toString i) prec else toString i
+
+private local instance : Append String where
+  append := String.Internal.append
+
 /-- Internal representation of a linear combination of atoms, and a constant term. -/
 structure LinearCombo where
   /-- Constant term. -/
@@ -38,17 +52,6 @@ namespace LinearCombo
 private def join (l : List String) : String :=
   l.foldl (init := "") (fun sofar next => String.Internal.append sofar next)
 
-private local instance : Append String where
-  append := String.Internal.append
-
-private local instance : ToString Int where
-  toString
-    | Int.ofNat m   => toString m
-    | Int.negSucc m => "-" ++ toString (m + 1)
-
-private local instance : Append String where
-  append := String.Internal.append
-
 instance : ToString LinearCombo where
   toString lc := private
     s!"{lc.const}{join <| lc.coeffs.toList.zipIdx.map fun ⟨c, i⟩ => s!" + {c} * x{i+1}"}"

src/Init/System/IO.lean

@@ -17,6 +17,7 @@ import Init.Data.List.MapIdx
 import Init.Data.Ord.UInt
 import Init.Data.ToString.Macro
 import Init.Data.List.Impl
+import Init.Data.Int.Repr
 
 public section
 

src/Std/Data/String.lean

@@ -7,3 +7,4 @@ module
 
 prelude
 public import Std.Data.String.ToNat
+public import Std.Data.String.ToInt

src/Std/Data/String/ToInt.lean

@@ -0,0 +1,180 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Julia Markus Himmel
+-/
+module
+
+prelude
+public import Init.Data.String.Slice
+public import Init.Data.String.Search
+public import Init.Data.ToString.Extra
+public import Init.Data.String.TakeDrop
+import all Init.Data.String.Slice
+import all Init.Data.String.Search
+import Std.Data.String.ToNat
+import Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
+import Init.Data.String.Lemmas.Pattern.TakeDrop.Char
+import Init.Data.Int.ToString
+
+namespace String
+
+namespace Slice
+
+public theorem toInt?_eq_some_iff {s : String.Slice} {a : Int} :
+    s.toInt? = some a ↔ (∃ b, s.toNat? = some b ∧ a = (b : Int)) ∨ ∃ t, s.copy = "-" ++ t ∧ ∃ b, t.toNat? = some b ∧ a = -(b : Int) := by
+  rw [toInt?]
+  match h : s.dropPrefix? '-' with
+  | some rest =>
+    have heq := eq_append_of_dropPrefix?_char_eq_some h
+    suffices s.toNat? = none by
+      simp only [Option.map_eq_some_iff, this, reduceCtorEq, false_and, exists_const, heq,
+        ↓Char.isValue, String.reduceSingleton, append_right_inj, exists_eq_left', toNat?_copy,
+        false_or]
+      cases rest.toNat? <;> simp [Int.negOfNat_eq, eq_comm]
+    exact toNat?_eq_none (by simp [← Bool.not_eq_true, isNat_iff, heq])
+  | none =>
+    simp only [↓Char.isValue, dropPrefix?_eq_none_iff, startsWith_char_eq_false_iff_forall_append,
+      String.reduceSingleton, ne_eq] at h
+    simp only [Option.map_eq_some_iff, Int.ofNat_eq_natCast, eq_comm (a := a), iff_self_or,
+      forall_exists_index, and_imp]
+    exact fun t ht => (h _ ht).elim
+
+@[simp]
+public theorem isSome_toInt? {s : String.Slice} : s.toInt?.isSome = s.isInt := by
+  simp only [toInt?, ↓Char.isValue, isInt]
+  split <;> simp
+
+public theorem isInt_of_toInt?_eq_some {s : String.Slice} (h : s.toInt? = some a) : s.isInt = true := by
+  simp [← isSome_toInt?, h]
+
+@[simp]
+public theorem toInt?_eq_none_iff {s : String.Slice} : s.toInt? = none ↔ s.isInt = false := by
+  simp [← Option.isNone_iff_eq_none, ← Option.not_isSome, isSome_toInt?]
+
+public theorem toInt?_eq_none {s : String.Slice} (h : s.isInt = false) : s.toInt? = none :=
+  toInt?_eq_none_iff.2 h
+
+public theorem isInt_iff {s : String.Slice} :
+    s.isInt = true ↔ s.isNat = true ∨ ∃ t, s.copy = "-" ++ t ∧ t.isNat = true := by
+  simp only [← isSome_toInt?, Option.isSome_iff_exists, toInt?_eq_some_iff, ← isSome_toNat?,
+    ← String.isSome_toNat?]
+  refine ⟨?_, ?_⟩
+  · rintro ⟨a, (⟨b, ⟨h, rfl⟩⟩|⟨t, ⟨h₁, ⟨b, ⟨h₂, rfl⟩⟩⟩⟩)⟩
+    · simp [h]
+    · exact Or.inr ⟨t, by simp [h₁, h₂]⟩
+  · rintro (⟨a, h⟩|⟨t, h₁, ⟨b, h₂⟩⟩)
+    · simp [h]
+    · exact ⟨-(b : Int), Or.inr ⟨t, by simp [h₁, h₂]⟩⟩
+
+public theorem isInt_of_isNat {s : String.Slice} (h : s.isNat = true) : s.isInt = true :=
+  isInt_iff.2 (Or.inl h)
+
+public theorem toInt?_eq_toNat?_of_startsWith_eq_false {s : String.Slice} (h : s.startsWith '-' = false) :
+    s.toInt? = s.toNat?.map (fun (n : Nat) => (n : Int)) := by
+  rw [toInt?, dropPrefix?_eq_none_iff.2 h]
+  cases s.toNat? <;> simp
+
+public theorem toInt?_eq_of_eq_minus_append {s : String.Slice} {t : String} (h : s.copy = "-" ++ t) :
+    s.toInt? = t.toNat?.map (fun (n : Nat) => -(n : Int)) := by
+  apply Option.ext (fun a => ?_)
+  simp only [toInt?_eq_some_iff, h, append_right_inj, exists_eq_left']
+  suffices s.toNat? = none by cases t.toNat? <;> simp [this, eq_comm]
+  exact toNat?_eq_none (by simp [← Bool.not_eq_true, isNat_iff, h])
+
+public theorem toInt?_eq_some_of_toNat?_eq_some {s : String.Slice} {a : Nat}
+    (h : s.toNat? = some a) : s.toInt? = some (a : Int) :=
+  toInt?_eq_some_iff.2 (Or.inl ⟨a, h, rfl⟩)
+
+public theorem toInt?_congr {s t : String.Slice} (h : s.copy = t.copy) : s.toInt? = t.toInt? :=
+  Option.ext (fun a => by simp [toInt?_eq_some_iff, toNat?_congr h, h])
+
+public theorem isInt_congr {s t : String.Slice} (h : s.copy = t.copy) : s.isInt = t.isInt := by
+  simp only [← isSome_toInt?, toInt?_congr h]
+
+end Slice
+
+@[simp]
+public theorem isInt_toSlice {s : String} : s.toSlice.isInt = s.isInt :=
+  (rfl)
+
+@[simp]
+public theorem toInt?_toSlice {s : String} : s.toSlice.toInt? = s.toInt? :=
+  (rfl)
+
+@[simp]
+public theorem Slice.isInt_copy {s : Slice} : s.copy.isInt = s.isInt := by
+  simpa [← isInt_toSlice] using Slice.isInt_congr (by simp)
+
+@[simp]
+public theorem Slice.toInt?_copy {s : Slice} : s.copy.toInt? = s.toInt? := by
+  simpa [← isInt_toSlice] using Slice.toInt?_congr (by simp)
+
+public theorem toInt?_eq_some_iff {s : String} {a : Int} :
+    s.toInt? = some a ↔ (∃ b, s.toNat? = some b ∧ a = (b : Int)) ∨ ∃ t, s = "-" ++ t ∧ ∃ b, t.toNat? = some b ∧ a = -(b : Int) := by
+  simp [← toInt?_toSlice, Slice.toInt?_eq_some_iff]
+
+@[simp]
+public theorem isSome_toInt? {s : String} : s.toInt?.isSome = s.isInt := by
+  simp [← toInt?_toSlice, ← isInt_toSlice]
+
+public theorem isInt_of_toInt?_eq_some {s : String} (h : s.toInt? = some a) : s.isInt = true := by
+  rw [← isInt_toSlice, Slice.isInt_of_toInt?_eq_some (by simpa)]
+
+@[simp]
+public theorem toInt?_eq_none_iff {s : String} : s.toInt? = none ↔ s.isInt = false := by
+  simp [← Option.isNone_iff_eq_none, ← Option.not_isSome, isSome_toInt?]
+
+public theorem toInt?_eq_none {s : String} (h : s.isInt = false) : s.toInt? = none :=
+  toInt?_eq_none_iff.2 h
+
+public theorem isInt_iff {s : String} :
+    s.isInt = true ↔ s.isNat = true ∨ ∃ t, s = "-" ++ t ∧ t.isNat = true := by
+  simp [← isInt_toSlice, Slice.isInt_iff]
+
+public theorem isInt_of_isNat {s : String} (h : s.isNat = true) : s.isInt = true := by
+  rw [← isInt_toSlice, Slice.isInt_of_isNat (by simpa)]
+
+public theorem toInt?_eq_toNat?_of_startsWith_eq_false {s : String} (h : s.startsWith '-' = false) :
+    s.toInt? = s.toNat?.map (fun (a : Nat) => (a : Int)) := by
+  rw [← toInt?_toSlice, ← toNat?_toSlice,
+    Slice.toInt?_eq_toNat?_of_startsWith_eq_false (by simpa [← startsWith_eq_startsWith_toSlice])]
+
+@[simp]
+public theorem toInt?_minus_append {s : String} :
+    ("-" ++ s).toInt? = s.toNat?.map (fun (n : Nat) => -(n : Int)) := by
+  rw [← toInt?_toSlice, Slice.toInt?_eq_of_eq_minus_append]
+  simp
+
+public theorem toInt?_eq_some_of_toNat?_eq_some {s : String} {a : Nat} (h : s.toNat? = some a) :
+    s.toInt? = some (a : Int) :=
+  toInt?_eq_some_iff.2 (Or.inl ⟨a, h, rfl⟩)
+
+end String
+
+@[simp]
+public theorem Nat.toInt?_repr (n : Nat) : n.repr.toInt? = some (n : Int) :=
+  String.toInt?_eq_some_of_toNat?_eq_some (toNat?_repr _)
+
+@[simp]
+public theorem Nat.isInt_repr (n : Nat) : n.repr.isInt = true := by
+  simp [← String.isSome_toInt?]
+
+namespace Int
+
+@[simp]
+public theorem toInt?_repr (a : Int) : a.repr.toInt? = some a := by
+  rw [repr_eq_if]
+  split <;> (simp; omega)
+
+public theorem isInt?_repr (a : Int) : a.repr.isInt = true := by
+  simp [← String.isSome_toInt?]
+
+public theorem repr_injective {a b : Int} (h : Int.repr a = Int.repr b) : a = b := by
+  rw [← Option.some.injEq, ← toInt?_repr a, ← toInt?_repr b, h]
+
+@[simp]
+public theorem repr_inj {a b : Int} : Int.repr a = Int.repr b ↔ a = b :=
+  ⟨repr_injective, (· ▸ rfl)⟩
+
+end Int

src/Std/Data/String/ToNat.lean

@@ -204,6 +204,15 @@ public theorem toNat?_eq_some_ofDigitChars {s : String.Slice} (h : s.isNat = tru
   simp [Nat.ofDigitChars_eq_foldl, ↓Char.isValue, Char.reduceToNat, foldl_eq_foldl_toList, List.foldl_ite_right,
     bne_eq, Bool.beq_eq_decide_eq, Nat.mul_comm 10]
 
+public theorem isNat_congr {s t : String.Slice} (h : s.copy = t.copy) : s.isNat = t.isNat := by
+  rw [Bool.eq_iff_iff, isNat_iff, isNat_iff, ← isEmpty_copy]
+  simp [h]
+
+public theorem toNat?_congr {s t : String.Slice} (h : s.copy = t.copy) : s.toNat? = t.toNat? := by
+  match h' : s.isNat with
+  | false => rw [toNat?_eq_none h', toNat?_eq_none (isNat_congr h ▸ h')]
+  | true => rw [toNat?_eq_some_ofDigitChars h', toNat?_eq_some_ofDigitChars (isNat_congr h ▸ h'), h]
+
 end String.Slice
 
 namespace String
@@ -216,6 +225,14 @@ public theorem isNat_toSlice {s : String} : s.toSlice.isNat = s.isNat :=
 public theorem toNat?_toSlice {s : String} : s.toSlice.toNat? = s.toNat? :=
   (rfl)
 
+@[simp]
+public theorem Slice.isNat_copy {s : Slice} : s.copy.isNat = s.isNat := by
+  simpa [← isNat_toSlice] using Slice.isNat_congr (by simp)
+
+@[simp]
+public theorem Slice.toNat?_copy {s : Slice} : s.copy.toNat? = s.toNat? := by
+  simpa [← isNat_toSlice] using Slice.toNat?_congr (by simp)
+
 public theorem isNat_iff {s : String} :
     s.isNat = true ↔
       s ≠ "" ∧

src/Std/Time/Internal/Bounded.lean

@@ -8,6 +8,7 @@ module
 prelude
 public import Init.Data.Int.DivMod.Lemmas
 public import Init.Data.Order.Ord
+public import Init.Data.Int.Repr
 public import Init.Omega
 import Init.Ext
 

src/Std/Time/Zoned/Database/TzIf.lean

@@ -8,6 +8,7 @@ module
 prelude
 public import Init.Data.Range.Polymorphic.Iterators
 public import Std.Internal.Parsec
+import Init.Data.Int.Repr
 
 public section