From 5fb25fff0699c09ae5cf9684dda914b43362ded4 Mon Sep 17 00:00:00 2001
From: Markus Himmel <markus@lean-fro.org>
Date: Wed, 26 Nov 2025 14:59:01 +0100
Subject: [PATCH] feat: `grind` instances for `String.Pos` and variants
 (#11384)

This PR adds the necessary instances for `grind` to reason about
`String.Pos.Raw`, `String.Pos` and `String.Slice.Pos`.
---
 src/Init/Data/String.lean            |   1 +
 src/Init/Data/String/Grind.lean      | 112 +++++++++++++++++++++++++++
 tests/lean/run/string_pos_grind.lean |  13 ++++
 3 files changed, 126 insertions(+)
 create mode 100644 src/Init/Data/String/Grind.lean
 create mode 100644 tests/lean/run/string_pos_grind.lean

diff --git a/src/Init/Data/String.lean b/src/Init/Data/String.lean
index 32b65b317f..0a223710b9 100644
--- a/src/Init/Data/String.lean
+++ b/src/Init/Data/String.lean
@@ -25,3 +25,4 @@ public import Init.Data.String.Termination
 public import Init.Data.String.ToSlice
 public import Init.Data.String.Search
 public import Init.Data.String.Legacy
+public import Init.Data.String.Grind
diff --git a/src/Init/Data/String/Grind.lean b/src/Init/Data/String/Grind.lean
new file mode 100644
index 0000000000..51ac6f6097
--- /dev/null
+++ b/src/Init/Data/String/Grind.lean
@@ -0,0 +1,112 @@
+/-
+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.Defs
+public import Init.Grind.ToInt
+
+public section
+
+/-!
+# Register string positions with `grind`.
+-/
+
+namespace String
+
+namespace Internal
+
+scoped macro "order" : tactic => `(tactic| {
+    simp [Pos.Raw.lt_iff, Pos.Raw.le_iff, String.Pos.lt_iff, String.Pos.le_iff, Slice.Pos.lt_iff,
+      Slice.Pos.le_iff, Pos.Raw.ext_iff, String.Pos.ext_iff, Slice.Pos.ext_iff] at *;
+    try omega })
+
+end Internal
+
+open Internal
+
+namespace Pos.Raw
+
+instance : Lean.Grind.ToInt String.Pos.Raw (.ci 0) where
+  toInt p := p.byteIdx
+  toInt_inj p q := by simp [Pos.Raw.ext_iff, ← Int.ofNat_inj]
+  toInt_mem := by simp
+
+@[simp]
+theorem toInt_eq {p : Pos.Raw} : Lean.Grind.ToInt.toInt p = p.byteIdx := rfl
+
+instance : Lean.Grind.ToInt.LE String.Pos.Raw (.ci 0) where
+  le_iff := by simp [Pos.Raw.le_iff]
+
+instance : Lean.Grind.ToInt.LT String.Pos.Raw (.ci 0) where
+  lt_iff := by simp [Pos.Raw.lt_iff]
+
+instance : Std.LawfulOrderLT String.Pos.Raw where
+  lt_iff := by order
+
+instance : Std.IsLinearOrder String.Pos.Raw where
+  le_refl := by order
+  le_trans := by order
+  le_antisymm := by order
+  le_total := by order
+
+end Pos.Raw
+
+namespace Pos
+
+instance {s : String} : Lean.Grind.ToInt s.Pos (.co 0 (s.utf8ByteSize + 1)) where
+  toInt p := p.offset.byteIdx
+  toInt_inj p q := by simp [Pos.ext_iff, Pos.Raw.ext_iff, ← Int.ofNat_inj]
+  toInt_mem p := by have := p.isValid.le_utf8ByteSize; simp; omega
+
+@[simp]
+theorem toInt_eq {s : String} {p : s.Pos} : Lean.Grind.ToInt.toInt p = p.offset.byteIdx := rfl
+
+instance {s : String} : Lean.Grind.ToInt.LE s.Pos (.co 0 (s.utf8ByteSize + 1)) where
+  le_iff := by simp [Pos.le_iff, Pos.Raw.le_iff]
+
+instance {s : String} : Lean.Grind.ToInt.LT s.Pos (.co 0 (s.utf8ByteSize + 1)) where
+  lt_iff := by simp [Pos.lt_iff, Pos.Raw.lt_iff]
+
+instance {s : String} : Std.LawfulOrderLT s.Pos where
+  lt_iff := by order
+
+instance {s : String} : Std.IsLinearOrder s.Pos where
+  le_refl := by order
+  le_trans := by order
+  le_antisymm := by order
+  le_total := by order
+
+end Pos
+
+namespace Slice.Pos
+
+instance {s : Slice} : Lean.Grind.ToInt s.Pos (.co 0 (s.utf8ByteSize + 1)) where
+  toInt p := p.offset.byteIdx
+  toInt_inj p q := by simp [Pos.ext_iff, Pos.Raw.ext_iff, ← Int.ofNat_inj]
+  toInt_mem p := by have := p.isValidForSlice.le_utf8ByteSize; simp; omega
+
+@[simp]
+theorem toInt_eq {s : Slice} {p : s.Pos} : Lean.Grind.ToInt.toInt p = p.offset.byteIdx := rfl
+
+instance {s : Slice} : Lean.Grind.ToInt.LE s.Pos (.co 0 (s.utf8ByteSize + 1)) where
+  le_iff := by simp [Pos.le_iff, Pos.Raw.le_iff]
+
+instance {s : Slice} : Lean.Grind.ToInt.LT s.Pos (.co 0 (s.utf8ByteSize + 1)) where
+  lt_iff := by simp [Pos.lt_iff, Pos.Raw.lt_iff]
+
+instance {s : Slice} : Std.LawfulOrderLT s.Pos where
+  lt_iff := by order
+
+instance {s : Slice} : Std.IsLinearOrder s.Pos where
+  le_refl := by order
+  le_trans := by order
+  le_antisymm := by order
+  le_total := by order
+
+end Slice.Pos
+
+end String
diff --git a/tests/lean/run/string_pos_grind.lean b/tests/lean/run/string_pos_grind.lean
new file mode 100644
index 0000000000..e16af5a59e
--- /dev/null
+++ b/tests/lean/run/string_pos_grind.lean
@@ -0,0 +1,13 @@
+module
+
+example {p q r : String.Pos.Raw} : p < q → q ≤ r → p < r := by
+  lia
+
+example {s : String} {p q r : s.Pos} : p < q → q ≤ r → p < r := by
+  lia
+
+example {s : String.Slice} {p q r : s.Pos} : p < q → q ≤ r → p < r := by
+  lia
+
+example {s : String} {p q : s.Pos} : p ≤ q ↔ p = q ∨ p < q := by
+  lia