feat: order instances for string positions (#12641)

This PR derives the linear order on string positions (`String.Pos.Raw`,
`String.Pos`, `String.Slice.Pos`) via `Std.LinearOrderPackage`, which
ensures that all data-carrying and propositional instances are present.

Previously, we were misssing some, like `Ord`.

src/Init/Data/Hashable.lean

@@ -6,7 +6,7 @@ Authors: Leonardo de Moura
 module
 
 prelude
-public import Init.Data.String.PosRaw
+import Init.Data.Array.Basic
 public import Init.Data.UInt.Basic
 
 public section
@@ -15,9 +15,6 @@ universe u
 instance : Hashable Nat where
   hash n := UInt64.ofNat n
 
-instance : Hashable String.Pos.Raw where
-  hash p := UInt64.ofNat p.byteIdx
-
 instance [Hashable α] [Hashable β] : Hashable (α × β) where
   hash | (a, b) => mixHash (hash a) (hash b)
 

src/Init/Data/Order/PackageFactories.lean

@@ -8,6 +8,7 @@ module
 prelude
 public import Init.Data.Order.LemmasExtra  -- shake: keep (instance inlined by `haveI`)
 public import Init.Data.Order.FactoriesExtra
+public import Init.Data.Order.Factories -- shake: keep (autoparam filling `Min.leftLeaningOfLE`)
 import Init.Data.Bool
 import Init.Data.Order.Lemmas
 
@@ -91,10 +92,11 @@ public structure Packages.PreorderOfLEArgs (α : Type u) where
       have := lt_iff
       DecidableLT α := by
     extract_lets
-    haveI := @_root_.Std.LawfulOrderLT.mk (lt_iff := by assumption) ..
     first
     | infer_instance
+    | (haveI := @_root_.Std.LawfulOrderLT.mk (lt_iff := by assumption) ..; infer_instance)
     | exact _root_.Std.FactoryInstances.decidableLTOfLE
+    | (haveI := @_root_.Std.LawfulOrderLT.mk (lt_iff := by assumption) ..; exact _root_.Std.FactoryInstances.decidableLTOfLE)
     | fail "Failed to automatically derive that `LT` is decidable. \
             Please ensure that a `DecidableLT` instance can be synthesized or \
             manually provide the field `decidableLT`."

src/Init/Data/String.lean

@@ -30,3 +30,4 @@ public import Init.Data.String.FindPos
 public import Init.Data.String.Subslice
 public import Init.Data.String.Iter
 public import Init.Data.String.Iterate
+public import Init.Data.String.Hashable

src/Init/Data/String/Hashable.lean

@@ -0,0 +1,20 @@
+/-
+Copyright (c) 2026 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.Hashable
+public import Init.Data.String.Defs
+
+public section
+
+namespace String
+
+deriving instance Hashable for String.Pos.Raw
+deriving instance Hashable for String.Pos
+deriving instance Hashable for String.Slice.Pos
+
+end String

src/Init/Data/String/OrderInstances.lean

@@ -9,7 +9,9 @@ prelude
 public import Init.Data.String.Defs
 public import Init.Grind.ToInt
 public import Init.Data.Order.Classes
+import Init.Data.Order.PackageFactories
 import Init.Omega
+public import Init.Data.Order.PackageFactories
 
 public section
 
@@ -46,14 +48,14 @@ instance : Lean.Grind.ToInt.LE String.Pos.Raw (.ci 0) where
 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.Total (α := String.Pos.Raw) (· ≤ ·) := ⟨fun _ _ => by order⟩
+instance : Trans (α := String.Pos.Raw) (· ≤ ·) (· ≤ ·) (· ≤ ·) := ⟨fun _ _ => by order⟩
+instance : Std.Antisymm (α := String.Pos.Raw) (· ≤ ·) := ⟨fun _ _ => 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
+instance : Std.LawfulOrderBEq String.Pos.Raw := ⟨fun _ _ => by order⟩
+instance : Std.LawfulOrderLT String.Pos.Raw := ⟨fun _ _ => by order⟩
+
+instance : Std.LinearOrderPackage String.Pos.Raw := .ofLE _
 
 end Pos.Raw
 
@@ -73,14 +75,14 @@ instance {s : String} : Lean.Grind.ToInt.LE s.Pos (.co 0 (s.utf8ByteSize + 1)) w
 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.Total (α := s.Pos) (· ≤ ·) := ⟨fun _ _ => by order⟩
+instance {s : String} : Trans (α := s.Pos) (· ≤ ·) (· ≤ ·) (· ≤ ·) := ⟨fun _ _ => by order⟩
+instance {s : String} : Std.Antisymm (α := s.Pos) (· ≤ ·) := ⟨fun _ _ => 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
+instance {s : String} : Std.LawfulOrderBEq s.Pos := ⟨fun _ _ => by order⟩
+instance {s : String} : Std.LawfulOrderLT s.Pos := ⟨fun _ _ => by order⟩
+
+instance {s : String} : Std.LinearOrderPackage s.Pos := .ofLE _
 
 end Pos
 
@@ -100,14 +102,14 @@ instance {s : Slice} : Lean.Grind.ToInt.LE s.Pos (.co 0 (s.utf8ByteSize + 1)) wh
 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.Total (α := s.Pos) (· ≤ ·) := ⟨fun _ _ => by order⟩
+instance {s : Slice} : Trans (α := s.Pos) (· ≤ ·) (· ≤ ·) (· ≤ ·) := ⟨fun _ _ => by order⟩
+instance {s : Slice} : Std.Antisymm (α := s.Pos) (· ≤ ·) := ⟨fun _ _ => 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
+instance {s : Slice} : Std.LawfulOrderBEq s.Pos := ⟨fun _ _ => by order⟩
+instance {s : Slice} : Std.LawfulOrderLT s.Pos := ⟨fun _ _ => by order⟩
+
+instance {s : Slice} : Std.LinearOrderPackage s.Pos := .ofLE _
 
 end Slice.Pos
 

src/Init/Data/String/PosRaw.lean

@@ -57,9 +57,6 @@ instance (p₁ p₂ : String.Pos.Raw) : Decidable (p₁ ≤ p₂) :=
 instance (p₁ p₂ : String.Pos.Raw) : Decidable (p₁ < p₂) :=
   inferInstanceAs (Decidable (p₁.byteIdx < p₂.byteIdx))
 
-instance : Min String.Pos.Raw := minOfLe
-instance : Max String.Pos.Raw := maxOfLe
-
 @[simp]
 theorem Pos.Raw.byteIdx_sub_char {p : Pos.Raw} {c : Char} : (p - c).byteIdx = p.byteIdx - c.utf8Size := rfl
 

src/Init/Grind/Ring/CommSolver.lean

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

src/Lean/Elab/StructInstHint.lean

@@ -8,6 +8,7 @@ module
 
 prelude
 public import Lean.Meta.Hint
+import Init.Data.String.OrderInstances
 
 public section
 

src/Lean/Parser/Types.lean

@@ -8,6 +8,7 @@ module
 prelude
 public import Lean.Data.Trie
 public import Lean.DocString.Extension
+import Init.Data.String.OrderInstances
 
 public section
 

src/Lean/Server/FileWorker.lean

@@ -21,6 +21,8 @@ public import Lean.Server.FileWorker.SetupFile
 public import Lean.Server.Completion.ImportCompletion
 public import Lean.Server.CodeActions.UnknownIdentifier
 
+import Init.Data.String.OrderInstances
+
 public section
 
 /-!

src/Lean/Syntax.lean

@@ -10,6 +10,7 @@ public import Init.Data.Slice
 public import Init.Data.Hashable
 public import Lean.Data.Format
 public import Init.Data.Option.Coe
+public import Init.Data.String.Hashable
 import Init.Data.Range.Polymorphic.Iterators
 import Init.Data.ToString.Macro
 import Init.Omega