From 71fad35e59f79948a8d5f42efb22f484bfb9398f Mon Sep 17 00:00:00 2001 From: Markus Himmel Date: Mon, 23 Feb 2026 09:20:52 +0100 Subject: [PATCH] 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 | 5 +-- src/Init/Data/Order/PackageFactories.lean | 4 ++- src/Init/Data/String.lean | 1 + src/Init/Data/String/Hashable.lean | 20 +++++++++++ src/Init/Data/String/OrderInstances.lean | 44 ++++++++++++----------- src/Init/Data/String/PosRaw.lean | 3 -- src/Init/Grind/Ring/CommSolver.lean | 1 + src/Lean/Elab/StructInstHint.lean | 1 + src/Lean/Parser/Types.lean | 1 + src/Lean/Server/FileWorker.lean | 2 ++ src/Lean/Syntax.lean | 1 + 11 files changed, 54 insertions(+), 29 deletions(-) create mode 100644 src/Init/Data/String/Hashable.lean diff --git a/src/Init/Data/Hashable.lean b/src/Init/Data/Hashable.lean index e9ca6110b8..5f97d41225 100644 --- a/src/Init/Data/Hashable.lean +++ b/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) diff --git a/src/Init/Data/Order/PackageFactories.lean b/src/Init/Data/Order/PackageFactories.lean index 6c89a54ba1..5b7b6eb159 100644 --- a/src/Init/Data/Order/PackageFactories.lean +++ 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`." diff --git a/src/Init/Data/String.lean b/src/Init/Data/String.lean index 8c61c85c79..d859797e13 100644 --- a/src/Init/Data/String.lean +++ b/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 diff --git a/src/Init/Data/String/Hashable.lean b/src/Init/Data/String/Hashable.lean new file mode 100644 index 0000000000..1925ae03e4 --- /dev/null +++ b/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 diff --git a/src/Init/Data/String/OrderInstances.lean b/src/Init/Data/String/OrderInstances.lean index 2cd0dd2970..821d9d3b46 100644 --- a/src/Init/Data/String/OrderInstances.lean +++ b/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 diff --git a/src/Init/Data/String/PosRaw.lean b/src/Init/Data/String/PosRaw.lean index 2517bc2071..505515150d 100644 --- a/src/Init/Data/String/PosRaw.lean +++ b/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 diff --git a/src/Init/Grind/Ring/CommSolver.lean b/src/Init/Grind/Ring/CommSolver.lean index 9ab3fce34d..c02d1a75ee 100644 --- a/src/Init/Grind/Ring/CommSolver.lean +++ b/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 diff --git a/src/Lean/Elab/StructInstHint.lean b/src/Lean/Elab/StructInstHint.lean index 1d55a047cc..3d0a6dcf82 100644 --- a/src/Lean/Elab/StructInstHint.lean +++ b/src/Lean/Elab/StructInstHint.lean @@ -8,6 +8,7 @@ module prelude public import Lean.Meta.Hint +import Init.Data.String.OrderInstances public section diff --git a/src/Lean/Parser/Types.lean b/src/Lean/Parser/Types.lean index 2c6f34796a..445afdff00 100644 --- a/src/Lean/Parser/Types.lean +++ b/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 diff --git a/src/Lean/Server/FileWorker.lean b/src/Lean/Server/FileWorker.lean index ff45659c65..1a28a4aa18 100644 --- a/src/Lean/Server/FileWorker.lean +++ b/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 /-! diff --git a/src/Lean/Syntax.lean b/src/Lean/Syntax.lean index 627090cb9a..186ff6f39b 100644 --- a/src/Lean/Syntax.lean +++ b/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