feat: infrastructure for grind order (#10553)

This PR implements infrastructure for the new `grind order` module.

src/Init/Grind.lean

@@ -24,3 +24,4 @@ public import Init.Grind.Attr
 public import Init.Data.Int.OfNat -- This may not have otherwise been imported, breaking `grind` proofs.
 public import Init.Grind.AC
 public import Init.Grind.Injective
+public import Init.Grind.Order

src/Init/Grind/Order.lean

@@ -0,0 +1,299 @@
+/-
+Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+module
+prelude
+public import Init.Grind.Ordered.Ring
+public import Init.Grind.Ring.CommSolver
+import Init.Grind.Ring
+@[expose] public section
+namespace Lean.Grind.Order
+
+/- **TODO**: remove this file to `Offset.lean` after we remove the old offset module that supports only `Nat`. -/
+
+/-- A `Weight` is just an linear ordered additive commutative group. -/
+class Weight (ω : Type v) extends Add ω, LE ω, LT ω, BEq ω, LawfulBEq ω where
+  [decLe : DecidableLE ω]
+  [decLt : DecidableLT ω]
+
+/--
+An `Offset` type `α` with weight `ω`.
+-/
+class Offset (α : Type u) (ω : Type v) [Weight ω] extends LE α, LT α, Std.IsPreorder α, Std.LawfulOrderLT α where
+  offset      : α → ω → α
+  offset_add  : ∀ (a : α) (k₁ k₂ : ω), offset (offset a k₁) k₂ = offset a (k₁ + k₂)
+  offset_le   : ∀ (a b : α) (k : ω),   offset a k ≤ offset b k ↔ a ≤ b
+  weight_le   : ∀ (a : α) (k₁ k₂ : ω), offset a k₁ ≤ offset a k₂ → k₁ ≤ k₂
+  weight_lt   : ∀ (a : α) (k₁ k₂ : ω), offset a k₁ < offset a k₂ → k₁ < k₂
+
+local instance : Weight Nat where
+local instance : Weight Int where
+
+def Unit.weight : Weight Unit where
+  add := fun _ _ => ()
+  le := fun _ _ => True
+  lt := fun _ _ => False
+  decLe := fun _ _ => inferInstanceAs (Decidable True)
+  decLt := fun _ _ => inferInstanceAs (Decidable False)
+
+attribute [local instance] Ring.intCast Semiring.natCast in
+local instance {α} [LE α] [LT α] [Std.LawfulOrderLT α] [Ring α] [Std.IsPreorder α] [OrderedRing α] : Offset α Int where
+  offset a k    := a + k
+  offset_add    := by intros; rw [Ring.intCast_add, Semiring.add_assoc]
+  offset_le     := by intros; rw [← OrderedAdd.add_le_left_iff]
+  weight_le     := by
+    intro _ _ _ h; replace h := OrderedAdd.add_le_right_iff _ |>.mpr h
+    exact OrderedRing.le_of_intCast_le_intCast _ _ h
+  weight_lt     := by
+    intro _ _ _ h; replace h := OrderedAdd.add_lt_right_iff _ |>.mpr h
+    exact OrderedRing.lt_of_intCast_lt_intCast _ _ h
+
+local instance : Offset Int Int where
+  offset a k    := a + k
+  offset_add    := by omega
+  offset_le     := by simp
+  weight_le     := by simp
+  weight_lt     := by simp
+
+local instance : Offset Nat Nat where
+  offset a k    := a + k
+  offset_add    := by omega
+  offset_le     := by simp
+  weight_le     := by simp
+  weight_lt     := by simp
+  -- TODO: why did we have to provide the following three fields manually?
+  le_refl       := by apply Std.IsPreorder.le_refl
+  le_trans      := by apply Std.IsPreorder.le_trans
+  lt_iff        := by apply Std.LawfulOrderLT.lt_iff
+
+attribute [local instance] Unit.weight
+
+/-- Dummy `Offset` instance for orders that do not support offsets. -/
+def dummyOffset (α : Type u) [LE α] [LT α] [Std.IsPreorder α] [Std.LawfulOrderLT α] : Offset α Unit where
+  offset a _ := a
+  offset_add _ _ _ := rfl
+  offset_le _ _ _ := Iff.rfl
+  weight_le _ _ _ _ := True.intro
+  weight_lt x _ _ h := by exfalso; exact Preorder.lt_irrefl x h
+
+/-- Dummy `Offset` instance for orders that do not support offsets nor `LT` -/
+def dummyOffset' (α : Type u) [LE α] [Std.IsPreorder α] : Offset α Unit where
+  lt a b := a ≤ b ∧ ¬ b ≤ a
+  lt_iff _ _ := Iff.rfl
+  offset a _ := a
+  offset_add _ _ _ := rfl
+  offset_le _ _ _ := Iff.rfl
+  weight_le _ _ _ _ := True.intro
+  weight_lt _ _ _ h := by cases h; contradiction
+
+namespace Offset
+
+theorem offset_lt {α ω} [Weight ω] [Offset α ω]
+    (a b : α) (k : ω) : offset a k < offset b k ↔ a < b := by
+  simp only [Std.LawfulOrderLT.lt_iff]
+  constructor
+  next =>
+    intro ⟨h₁, h₂⟩
+    constructor
+    next => apply offset_le _ _ _ |>.mp h₁
+    next => intro h; have := offset_le _ _ k |>.mpr h; contradiction
+  next =>
+    intro ⟨h₁, h₂⟩
+    constructor
+    next => apply offset_le _ _ _ |>.mpr h₁
+    next => intro h; have := offset_le _ _ k |>.mp h; contradiction
+
+private theorem add_le_add' {α ω} [Weight ω] [Offset α ω]
+    {a b : α} {k₁ k₂ : ω} (k : ω) :
+    offset a k₁ ≤ offset b k₂ → offset a (k₁ + k) ≤ offset b (k₂ + k) := by
+  intro h; replace h := offset_le _ _ k |>.mpr h
+  simp [offset_add] at h; assumption
+
+private theorem add_lt_add' {α ω} [Weight ω] [Offset α ω]
+    {a b : α} {k₁ k₂ : ω} (k : ω) :
+    offset a k₁ < offset b k₂ → offset a (k₁ + k) < offset b (k₂ + k) := by
+  intro h; replace h := offset_lt _ _ k |>.mpr h
+  simp [offset_add] at h; assumption
+
+/-!
+Helper theorems for asserting equalities, negations
+
+**Note**: for negations if the order is not a linear preorder, the solver just
+saves the negated inequality, and tries to derive contradiction if the inequality is implied
+by other constraints.
+-/
+theorem le_of_eq {α} [LE α] [Std.IsPreorder α]
+    (a b : α) : a = b → a ≤ b := by
+  intro h; subst a; apply Std.IsPreorder.le_refl
+
+theorem le_of_not_le {α} [LE α] [Std.IsLinearPreorder α]
+    (a b : α) : ¬ a ≤ b → b ≤ a := by
+  intro h
+  have := Std.IsLinearPreorder.le_total a b
+  cases this; contradiction; assumption
+
+theorem lt_of_not_le {α} [LE α] [LT α] [Std.IsLinearPreorder α] [Std.LawfulOrderLT α]
+    (a b : α) : ¬ a ≤ b → b < a := by
+  intro h
+  rw [Std.LawfulOrderLT.lt_iff]
+  have := Std.IsLinearPreorder.le_total a b
+  cases this; contradiction; simp [*]
+
+theorem le_of_not_lt {α} [LE α] [LT α] [Std.IsLinearPreorder α] [Std.LawfulOrderLT α]
+    (a b : α) : ¬ a < b → b ≤ a := by
+  rw [Std.LawfulOrderLT.lt_iff]
+  open Classical in
+  rw [Classical.not_and_iff_not_or_not, Classical.not_not]
+  intro h; cases h
+  next =>
+    have := Std.IsLinearPreorder.le_total a b
+    cases this; contradiction; assumption
+  next => assumption
+
+-- **Note**: We hard coded the `Nat` and `Int` cases for `lt` => `le`. If users want support for other types, we can add a type class.
+theorem Int.lt (x y k₁ k₂ : Int) : offset x k₁ < offset y k₂ → offset x (k₁+1) ≤ offset y k₂ := by
+  simp [offset]; omega
+
+theorem Nat.lt (x y k₁ k₂ : Nat) : offset x k₁ < offset y k₂ → offset x (k₁+1) ≤ offset y k₂ := by
+  simp [offset]; omega
+
+/-!
+Transitivity theorems
+-/
+theorem le_offset_trans₁ {α ω} [Weight ω] [Offset α ω]
+    (a b c : α) (k₁ k₂ k₃ k₄ k : ω) :
+    k₃ == k₂ + k → offset a k₁ ≤ offset b k₂ → offset b k₃ ≤ offset c k₄ → offset a (k₁ + k) ≤ offset c k₄ := by
+  intro h h₁ h₂; simp at h; subst k₃
+  replace h₁ := add_le_add' k h₁
+  exact Std.le_trans h₁ h₂
+
+theorem le_offset_trans₂ {α ω} [Weight ω] [Offset α ω]
+    (a b c : α) (k₁ k₂ k₃ k₄ k : ω) :
+    k₂ == k₃ + k → offset a k₁ ≤ offset b k₂ → offset b k₃ ≤ offset c k₄ → offset a k₁ ≤ offset c (k₄ + k) := by
+  intro h h₁ h₂; simp at h; subst k₂
+  replace h₂ := add_le_add' k h₂
+  exact Std.le_trans h₁ h₂
+
+theorem lt_offset_trans₁ {α ω} [Weight ω] [Offset α ω]
+    (a b c : α) (k₁ k₂ k₃ k₄ k : ω) :
+    k₃ == k₂ + k → offset a k₁ < offset b k₂ → offset b k₃ < offset c k₄ → offset a (k₁ + k) < offset c k₄ := by
+  intro h h₁ h₂; simp at h; subst k₃
+  replace h₁ := add_lt_add' k h₁
+  exact Preorder.lt_trans h₁ h₂
+
+theorem lt_offset_trans₂ {α ω} [Weight ω] [Offset α ω]
+    (a b c : α) (k₁ k₂ k₃ k₄ k : ω) :
+    k₂ == k₃ + k → offset a k₁ < offset b k₂ → offset b k₃ < offset c k₄ → offset a k₁ < offset c (k₄ + k) := by
+  intro h h₁ h₂; simp at h; subst k₂
+  replace h₂ := add_lt_add' k h₂
+  exact Preorder.lt_trans h₁ h₂
+
+theorem le_lt_offset_trans₁ {α ω} [Weight ω] [Offset α ω]
+    (a b c : α) (k₁ k₂ k₃ k₄ k : ω) :
+    k₃ == k₂ + k → offset a k₁ ≤ offset b k₂ → offset b k₃ < offset c k₄ → offset a (k₁ + k) < offset c k₄ := by
+  intro h h₁ h₂; simp at h; subst k₃
+  replace h₁ := add_le_add' k h₁
+  exact Preorder.lt_of_le_of_lt h₁ h₂
+
+theorem le_lt_offset_trans₂ {α ω} [Weight ω] [Offset α ω]
+    (a b c : α) (k₁ k₂ k₃ k₄ k : ω) :
+    k₂ == k₃ + k → offset a k₁ ≤ offset b k₂ → offset b k₃ < offset c k₄ → offset a k₁ < offset c (k₄ + k) := by
+  intro h h₁ h₂; simp at h; subst k₂
+  replace h₂ := add_lt_add' k h₂
+  exact Preorder.lt_of_le_of_lt h₁ h₂
+
+theorem lt_le_offset_trans₁ {α ω} [Weight ω] [Offset α ω]
+    (a b c : α) (k₁ k₂ k₃ k₄ k : ω) :
+    k₃ == k₂ + k → offset a k₁ < offset b k₂ → offset b k₃ ≤ offset c k₄ → offset a (k₁ + k) < offset c k₄ := by
+  intro h h₁ h₂; simp at h; subst k₃
+  replace h₁ := add_lt_add' k h₁
+  exact Preorder.lt_of_lt_of_le h₁ h₂
+
+theorem lt_le_offset_trans₂ {α ω} [Weight ω] [Offset α ω]
+    (a b c : α) (k₁ k₂ k₃ k₄ k : ω) :
+    k₂ == k₃ + k → offset a k₁ < offset b k₂ → offset b k₃ ≤ offset c k₄ → offset a k₁ < offset c (k₄ + k) := by
+  intro h h₁ h₂; simp at h; subst k₂
+  replace h₂ := add_le_add' k h₂
+  exact Preorder.lt_of_lt_of_le h₁ h₂
+
+/-!
+Unsat theorems
+-/
+attribute [local instance] Weight.decLe Weight.decLt
+
+theorem le_unsat {α ω} [Weight ω] [Offset α ω]
+    (a : α) (k₁ k₂ : ω) : offset a k₁ ≤ offset a k₂ → (k₁ ≤ k₂) == false → False := by
+  simp; apply weight_le
+
+theorem lt_unsat {α ω} [Weight ω] [Offset α ω]
+    (a : α) (k₁ k₂ : ω) : offset a k₁ < offset a k₂ → (k₁ < k₂) == false → False := by
+  simp; apply weight_lt
+
+/-!
+`Int` internalization theorems
+-/
+
+-- **Note**: We use `cutsat` normalizer to "rewrite" `Int` inequalities before converting into offsets.
+
+theorem Int.le (x y k : Int) : x + k ≤ y ↔ offset x k ≤ offset y (0:Int) := by
+  simp [offset]
+
+theorem Int.eq (x y k : Int) : x + k = y ↔ offset x k = offset y (0:Int) := by
+  simp [offset]
+
+/-!
+`Nat` internalization theorems
+-/
+
+-- **Note**: We use the `Nat` normalizer to "rewrite" `Nat` inequalities before converting into offsets.
+
+theorem Nat.le (x y k₁ k₂ : Nat) : x + k₁ ≤ y + k₂ ↔ offset x k₁ ≤ offset y k₂ := by
+  simp [offset]
+
+theorem Nat.eq (x y k₁ k₂ : Nat) : x + k₁ = y + k₂ ↔ offset x k₁ = offset y k₂ := by
+  simp [offset]
+
+/-!
+Types without `Offset` internalization theorems
+-/
+attribute [local instance] dummyOffset in
+theorem Dummy.le {α : Type u} [LE α] [LT α] [Std.IsPreorder α] [Std.LawfulOrderLT α] (x y : α) : x ≤ y ↔ offset x () ≤ offset y () := by
+  simp [offset]
+
+attribute [local instance] dummyOffset in
+theorem Dummy.lt {α : Type u} [LE α] [LT α] [Std.IsPreorder α] [Std.LawfulOrderLT α] (x y : α) : x < y ↔ offset x () < offset y () := by
+  simp [offset]
+
+attribute [local instance] dummyOffset' in
+theorem Dummy'.le {α : Type u} [LE α] [Std.IsPreorder α] (x y : α) : x ≤ y ↔ offset x () ≤ offset y () := by
+  simp [offset]
+
+attribute [local instance] dummyOffset' in
+theorem Dummy'.lt {α : Type u} [LE α] [Std.IsPreorder α] (x y : α) : x < y ↔ offset x () < offset y () := by
+  simp [offset]
+
+/-!
+Ring internalization theorems
+-/
+section
+
+variable {α} [Ring α] [instLe : LE α] [LT α] [instOrdLt : Std.LawfulOrderLT α] [Std.IsPreorder α] [OrderedRing α]
+attribute [local instance] Ring.intCast Semiring.natCast
+
+-- **Note**: We use `ring` normalizer to "rewrite" ring inequalities before converting into offsets.
+
+theorem Ring.le (x y : α) (k : Int) : x + k ≤ y ↔ offset x k ≤ offset y (0:Int) := by
+  simp [offset, Ring.intCast_zero, Semiring.add_zero]
+
+theorem Ring.lt (x y : α) (k : Int) : x + k < y ↔ offset x k < offset y (0:Int) := by
+  simp [offset, Ring.intCast_zero, Semiring.add_zero]
+
+theorem Ring.eq (x y : α) (k : Int) : x + k = y ↔ offset x k = offset y (0:Int) := by
+  simp [offset, Ring.intCast_zero, Semiring.add_zero]
+
+end
+
+end Offset
+end Lean.Grind.Order

src/Init/Grind/Tactics.lean

@@ -144,6 +144,11 @@ structure Config where
   ```
   -/
   inj := true
+  /--
+  When `true` (default: `true`), enables the procedure for handling orders that implement
+  at least `Std.IsPreorder`
+  -/
+  order := true
   deriving Inhabited, BEq
 
 /--

src/Lean/Meta/Tactic/Grind.lean

@@ -40,6 +40,7 @@ public import Lean.Meta.Tactic.Grind.AC
 public import Lean.Meta.Tactic.Grind.VarRename
 public import Lean.Meta.Tactic.Grind.ProofUtil
 public import Lean.Meta.Tactic.Grind.PropagateInj
+public import Lean.Meta.Tactic.Grind.Order
 
 public section
 

src/Lean/Meta/Tactic/Grind/Arith/Linear/StructId.lean

@@ -8,6 +8,7 @@ prelude
 public import Lean.Meta.Tactic.Grind.Types
 import Init.Grind.Ordered.Module
 import Lean.Meta.Tactic.Grind.Simp
+import Lean.Meta.Tactic.Grind.OrderInsts
 import Lean.Meta.Tactic.Grind.SynthInstance
 import Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt
 import Lean.Meta.Tactic.Grind.Arith.CommRing.RingId
@@ -97,43 +98,6 @@ private def mkOne? (u : Level) (type : Expr) : GoalM (Option Expr) := do
   unless (← isDefEqD one one') do reportIssue! (← mkExpectedDefEqMsg one one')
   return some one
 
-private def mkLawfulOrderLTInst? (u : Level) (type : Expr) (ltInst? leInst? : Option Expr) : GoalM (Option Expr) := do
-  let some ltInst := ltInst? | return none
-  let some leInst := leInst? | return none
-  let lawfulOrderLTType := mkApp3 (mkConst ``Std.LawfulOrderLT [u]) type ltInst leInst
-  let some inst ← synthInstance? lawfulOrderLTType
-    | reportIssue! "type has `LE` and `LT`, but the `LT` instance is not lawful, failed to synthesize{indentExpr lawfulOrderLTType}\n\
-        the `linarith` module will not process strict inequalities in this type"
-      return none
-  return some inst
-
-private def mkIsPreorderInst? (u : Level) (type : Expr) (leInst? : Option Expr) : GoalM (Option Expr) := do
-  let some leInst := leInst? | return none
-  let isPreorderType := mkApp2 (mkConst ``Std.IsPreorder [u]) type leInst
-  let some inst ← synthInstance? isPreorderType
-    | reportIssue! "type has `LE`, but is not a preorder, failed to synthesize{indentExpr isPreorderType}\n\
-        the `linarith` module will not run on this type"
-      return none
-  return some inst
-
-private def mkIsPartialOrderInst? (u : Level) (type : Expr) (leInst? : Option Expr) : GoalM (Option Expr) := do
-  let some leInst := leInst? | return none
-  let isPartialOrderType := mkApp2 (mkConst ``Std.IsPartialOrder [u]) type leInst
-  let some inst ← synthInstance? isPartialOrderType
-    | -- There is no need to report an issue here, as behaviour doesn't change: we only synthesize the partial order instance
-      -- in order to check the linear order and preorder instances are compatible.
-      return none
-  return some inst
-
-private def mkIsLinearOrderInst? (u : Level) (type : Expr) (leInst?  : Option Expr) : GoalM (Option Expr) := do
-  let some leInst := leInst? | return none
-  let isLinearOrderType := mkApp2 (mkConst ``Std.IsLinearOrder [u]) type leInst
-  let some inst ← synthInstance? isLinearOrderType
-    | reportIssue! "type has `LE`, but is not a linear order, failed to synthesize{indentExpr isLinearOrderType}\n\
-        the `linarith` module will not process disequalities in this type (or equality goals)"
-      return none
-  return some inst
-
 private def mkOrderedRingInst? (u : Level) (type : Expr) (semiringInst? leInst? ltInst? preorderInst? : Option Expr) : GoalM (Option Expr) := do
   let some semiringInst := semiringInst? | return none
   let some leInst := leInst? | return none

src/Lean/Meta/Tactic/Grind/Order.lean

@@ -0,0 +1,21 @@
+/-
+Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+module
+prelude
+public import Lean.Meta.Tactic.Grind.Order.Types
+public import Lean.Meta.Tactic.Grind.Order.Internalize
+public import Lean.Meta.Tactic.Grind.Order.StructId
+public import Lean.Meta.Tactic.Grind.Order.OrderM
+public section
+namespace Lean.Meta.Grind.Order
+builtin_initialize registerTraceClass `grind.order
+builtin_initialize registerTraceClass `grind.order.internalize
+
+builtin_initialize
+  orderExt.setMethods
+    (internalize := Order.internalize)
+
+end Lean.Meta.Grind.Order

src/Lean/Meta/Tactic/Grind/Order/Internalize.lean

@@ -0,0 +1,36 @@
+/-
+Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+module
+prelude
+public import Lean.Meta.Tactic.Grind.Order.OrderM
+import Lean.Meta.Tactic.Grind.Order.StructId
+namespace Lean.Meta.Grind.Order
+
+def getType? (e : Expr) : Option Expr :=
+  match_expr e with
+  | LE.le α _ _ _ => some α
+  | LT.lt α _ _ _ => some α
+  | HAdd.hAdd α _ _ _ _ _ => some α
+  | HSub.hSub α _ _ _ _ _ => some α
+  | OfNat.ofNat α _ _ => some α
+  | _ => none
+
+def isForbiddenParent (parent? : Option Expr) : Bool :=
+  if let some parent := parent? then
+    getType? parent |>.isSome
+  else
+    false
+
+public def internalize (e : Expr) (parent? : Option Expr) : GoalM Unit := do
+  unless (← getConfig).order do return ()
+  let some α := getType? e | return ()
+  if isForbiddenParent parent? then return ()
+  let some structId ← getStructId? α | return ()
+  OrderM.run structId do
+  trace[grind.order.internalize] "{e}"
+  -- TODO
+
+end Lean.Meta.Grind.Order

src/Lean/Meta/Tactic/Grind/Order/OrderM.lean

@@ -0,0 +1,35 @@
+/-
+Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+module
+prelude
+public import Lean.Meta.Tactic.Grind.Order.Types
+public section
+namespace Lean.Meta.Grind.Order
+
+structure OrderM.Context where
+  structId : Nat
+
+abbrev OrderM := ReaderT OrderM.Context GoalM
+
+abbrev OrderM.run (structId : Nat) (x : OrderM α) : GoalM α :=
+  x { structId }
+
+abbrev getStructId : OrderM Nat :=
+  return (← read).structId
+
+def getStruct : OrderM Struct := do
+  let s ← get'
+  let structId ← getStructId
+  if h : structId < s.structs.size then
+    return s.structs[structId]
+  else
+    throwError "`grind` internal error, invalid order structure id"
+
+def modifyStruct (f : Struct → Struct) : OrderM Unit := do
+  let structId ← getStructId
+  modify' fun s => { s with structs := s.structs.modify structId f }
+
+end Lean.Meta.Grind.Order

src/Lean/Meta/Tactic/Grind/Order/StructId.lean

@@ -0,0 +1,56 @@
+/-
+Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+module
+prelude
+public import Lean.Meta.Tactic.Grind.Order.Types
+import Lean.Meta.Tactic.Grind.OrderInsts
+public section
+namespace Lean.Meta.Grind.Order
+
+private def preprocess (e : Expr) : GoalM Expr := do
+  shareCommon (← canon e)
+
+private def internalizeFn (fn : Expr) : GoalM Expr := do
+  preprocess fn
+
+private def getInst? (declName : Name) (u : Level) (type : Expr) : GoalM (Option Expr) := do
+  synthInstance? <| mkApp (mkConst declName [u]) type
+
+def getStructId? (type : Expr) : GoalM (Option Nat) := do
+  unless (← getConfig).order do return none
+  if let some id? := (← get').typeIdOf.find? { expr := type } then
+    return id?
+  else
+    let id? ← go?
+    modify' fun s => { s with typeIdOf := s.typeIdOf.insert { expr := type } id? }
+    return id?
+where
+  go? : GoalM (Option Nat) := do
+    let u ← getDecLevel type
+    let some leInst ← getInst? ``LE u type | return none
+    let some isPreorderInst ← mkIsPreorderInst? u type (some leInst) | return none
+    let isPartialInst? ← mkIsPartialOrderInst? u type (some leInst)
+    let isLinearPreInst? ← mkIsLinearPreorderInst? u type (some leInst)
+    let ltInst? ← getInst? ``LT u type
+    let leFn ← internalizeFn <| mkApp2 (mkConst ``LE.le [u]) type leInst
+    let (lawfulOrderLTInst?, ltFn?) ← if let some ltInst := ltInst? then
+      let inst? ← mkLawfulOrderLTInst? u type ltInst? (some leInst)
+      if inst?.isNone then
+        pure (none, none)
+      else
+        let ltFn ← internalizeFn <| mkApp2 (mkConst ``LT.lt [u]) type ltInst
+        pure (inst?, some ltFn)
+    else
+      pure (none, none)
+    let id := (← get').structs.size
+    let struct := {
+      id,  type, u, leInst, isPreorderInst, ltInst?, leFn, isPartialInst?
+      isLinearPreInst?, ltFn?, lawfulOrderLTInst?
+     }
+    modify' fun s => { s with structs := s.structs.push struct }
+    return some id
+
+end Lean.Meta.Grind.Order

src/Lean/Meta/Tactic/Grind/Order/Types.lean

@@ -0,0 +1,168 @@
+/-
+Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+module
+prelude
+public import Lean.Meta.Tactic.Grind.Types
+public import Init.Data.Rat.Basic
+public section
+namespace Lean.Meta.Grind.Order
+
+/-!
+Solver for preorders, partial orders, linear orders, and support for offsets.
+-/
+
+abbrev NodeId := Nat
+/--
+**Note**: We use `Int` to represent weights, but solver supports `Unit` (encoded as `0`),
+`Nat`, and `Int`. During proof construction we perform the necessary conversions.
+-/
+abbrev Weight := Int
+
+/--
+A constraint of the form `u + k₁ ≤ v + k₂` (`u + k₁ < v + k₂` if `strict := true`)
+Remark: If the order does not support offsets, then `k₁` and `k₂` are zero.
+`h? := some h` if the Lean expression is not definitionally equal to the constraint,
+but provably equal with proof `h`.
+-/
+structure Cnstr where
+  u      : NodeId
+  v      : NodeId
+  strict : Bool   := false
+  k₁     : Weight := 0
+  k₂     : Weight := 0
+  h?     : Option Expr := none
+  deriving Inhabited
+
+structure WeightS where
+  w : Rat
+  strict := false
+
+def WeightS.compare (a b : WeightS) : Ordering :=
+  if a.w < b.w then
+    .lt
+  else if b.w > a.w then
+    .gt
+  else if a.strict == b.strict then
+    .eq
+  else if !a.strict && b.strict then
+    .lt
+  else
+    .gt
+
+instance : Ord WeightS where
+  compare := WeightS.compare
+
+instance : LE WeightS where
+  le a b := compare a b ≠ .gt
+
+instance : LT WeightS where
+  lt a b := compare a b = .lt
+
+instance : DecidableLE WeightS :=
+  fun a b => inferInstanceAs (Decidable (compare a b ≠ .gt))
+
+instance : DecidableLT WeightS :=
+  fun a b => inferInstanceAs (Decidable (compare a b = .lt))
+
+/-- Auxiliary structure used for proof extraction.  -/
+structure ProofInfo where
+  w      : NodeId
+  strict : Bool := false
+  k₁     : Rat := 0
+  k₂     : Rat := 0
+  proof  : Expr
+  deriving Inhabited
+
+/--
+Auxiliary inductive type for representing constraints and equalities
+that should be propagated to core.
+Recall that we cannot compute proofs until the short-distance
+data-structures have been fully updated when a new edge is inserted.
+Thus, we store the information to be propagated into a list.
+See field `propagate` in `State`.
+-/
+inductive ToPropagate where
+  | eqTrue (e : Expr) (u v : NodeId) (k k' : Int)
+  | eqFalse (e : Expr) (u v : NodeId) (k k' : Int)
+  | eq (u v : NodeId)
+  deriving Inhabited
+
+/--
+State for each order structure processed by this module.
+Each type must at least implement the instance `Std.IsPreorder`.
+-/
+structure Struct where
+  id                 : Nat
+  type               : Expr
+  /-- Cached `getDecLevel type` -/
+  u                  : Level
+  isPreorderInst     : Expr
+  /-- `LE` instance  -/
+  leInst             : Expr
+  /-- `LT` instance if available -/
+  ltInst?            : Option Expr
+  /-- `IsPartialOrder` instance if available -/
+  isPartialInst?     : Option Expr
+  /-- `IsLinearPreorder` instance if available -/
+  isLinearPreInst?   : Option Expr
+  /-- `LawfulOrderLT` instance if available -/
+  lawfulOrderLTInst? : Option Expr
+  leFn               : Expr
+  ltFn?              : Option Expr
+  -- TODO: offset instances
+  /-- Mapping from `NodeId` to the `Expr` represented by the node. -/
+  nodes              : PArray Expr := {}
+  /-- Mapping from `Expr` to a node representing it. -/
+  nodeMap            : PHashMap ExprPtr NodeId := {}
+  /-- Mapping from `Expr` representing inequalities to constraints. -/
+  cnstrs             : PHashMap ExprPtr Cnstr := {}
+  /--
+  Mapping from pairs `(u, v)` to a list of constraints on `u` and `v`.
+  We use this mapping to implement exhaustive constraint propagation.
+  -/
+  cnstrsOf           : PHashMap (NodeId × NodeId) (List (NodeId × Expr)) := {}
+  /--
+  For each node with id `u`, `sources[u]` contains
+  pairs `(v, k)` s.t. there is a path from `v` to `u` with weight `k`.
+  -/
+  sources            : PArray (AssocList NodeId WeightS) := {}
+  /--
+  For each node with id `u`, `targets[u]` contains
+  pairs `(v, k)` s.t. there is a path from `u` to `v` with weight `k`.
+  -/
+  targets            : PArray (AssocList NodeId WeightS) := {}
+  /--
+  Proof reconstruction information. For each node with id `u`, `proofs[u]` contains
+  pairs `(v, { w, proof })` s.t. there is a path from `u` to `v`, and
+  `w` is the penultimate node in the path, and `proof` is the justification for
+  the last edge.
+  -/
+  proofs             : PArray (AssocList NodeId ProofInfo) := {}
+  /-- Truth values and equalities to propagate to core. -/
+  propagate : List ToPropagate := []
+  deriving Inhabited
+
+/-- State for all order types detected by `grind`. -/
+structure State where
+  /-- Order structures detected. -/
+  structs : Array Struct := {}
+  /--
+  Mapping from types to its "structure id". We cache failures using `none`.
+  `typeIdOf[type]` is `some id`, then `id < structs.size`. -/
+  typeIdOf : PHashMap ExprPtr (Option Nat) := {}
+  /- Mapping from expressions/terms to their structure ids. -/
+  exprToStructId : PHashMap ExprPtr Nat := {}
+  deriving Inhabited
+
+builtin_initialize orderExt : SolverExtension State ← registerSolverExtension (return {})
+
+def get' : GoalM State := do
+  orderExt.getState
+
+@[inline] def modify' (f : State → State) : GoalM Unit := do
+  orderExt.modifyState f
+
+end Lean.Meta.Grind.Order

src/Lean/Meta/Tactic/Grind/OrderInsts.lean

@@ -0,0 +1,56 @@
+/-
+Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+module
+prelude
+public import Lean.Meta.Tactic.Grind.SynthInstance
+public section
+namespace Lean.Meta.Grind
+/-!
+Helper function for synthesizing order related instances.
+-/
+
+def mkLawfulOrderLTInst? (u : Level) (type : Expr) (ltInst? leInst? : Option Expr) : GoalM (Option Expr) := do
+  let some ltInst := ltInst? | return none
+  let some leInst := leInst? | return none
+  let lawfulOrderLTType := mkApp3 (mkConst ``Std.LawfulOrderLT [u]) type ltInst leInst
+  let some inst ← synthInstance? lawfulOrderLTType
+    | reportIssue! "type has `LE` and `LT`, but the `LT` instance is not lawful, failed to synthesize{indentExpr lawfulOrderLTType}"
+      return none
+  return some inst
+
+def mkIsPreorderInst? (u : Level) (type : Expr) (leInst? : Option Expr) : GoalM (Option Expr) := do
+  let some leInst := leInst? | return none
+  let isPreorderType := mkApp2 (mkConst ``Std.IsPreorder [u]) type leInst
+  let some inst ← synthInstance? isPreorderType
+    | reportIssue! "type has `LE`, but is not a preorder, failed to synthesize{indentExpr isPreorderType}"
+      return none
+  return some inst
+
+def mkIsPartialOrderInst? (u : Level) (type : Expr) (leInst? : Option Expr) : GoalM (Option Expr) := do
+  let some leInst := leInst? | return none
+  let isPartialOrderType := mkApp2 (mkConst ``Std.IsPartialOrder [u]) type leInst
+  let some inst ← synthInstance? isPartialOrderType
+    | reportIssue! "type has `LE`, but is not a partial order, failed to synthesize{indentExpr isPartialOrderType}"
+      return none
+  return some inst
+
+def mkIsLinearOrderInst? (u : Level) (type : Expr) (leInst?  : Option Expr) : GoalM (Option Expr) := do
+  let some leInst := leInst? | return none
+  let isLinearOrderType := mkApp2 (mkConst ``Std.IsLinearOrder [u]) type leInst
+  let some inst ← synthInstance? isLinearOrderType
+    | reportIssue! "type has `LE`, but is not a linear order, failed to synthesize{indentExpr isLinearOrderType}"
+      return none
+  return some inst
+
+def mkIsLinearPreorderInst? (u : Level) (type : Expr) (leInst?  : Option Expr) : GoalM (Option Expr) := do
+  let some leInst := leInst? | return none
+  let isLinearOrderType := mkApp2 (mkConst ``Std.IsLinearPreorder [u]) type leInst
+  let some inst ← synthInstance? isLinearOrderType
+    | reportIssue! "type has `LE`, but is not a linear preorder, failed to synthesize{indentExpr isLinearOrderType}"
+      return none
+  return some inst
+
+end Lean.Meta.Grind

tests/lean/run/grind_linarith_1.lean

@@ -66,12 +66,18 @@ example [CommRing α] [LE α] [LT α] [LawfulOrderLT α] [IsPreorder α] [Ordere
 
 -- Test misconfigured instances
 /--
-trace: [grind.issues] type has `LE` and `LT`, but the `LT` instance is not lawful, failed to synthesize
+trace: [grind.issues] type has `LE`, but is not a partial order, failed to synthesize
+      IsPartialOrder α
+[grind.issues] type has `LE`, but is not a linear preorder, failed to synthesize
+      IsLinearPreorder α
+[grind.issues] type has `LE` and `LT`, but the `LT` instance is not lawful, failed to synthesize
       LawfulOrderLT α
-    the `linarith` module will not process strict inequalities in this type
+[grind.issues] type has `LE` and `LT`, but the `LT` instance is not lawful, failed to synthesize
+      LawfulOrderLT α
+[grind.issues] type has `LE`, but is not a partial order, failed to synthesize
+      IsPartialOrder α
 [grind.issues] type has `LE`, but is not a linear order, failed to synthesize
       IsLinearOrder α
-    the `linarith` module will not process disequalities in this type (or equality goals)
 [grind.issues] type has a `Preorder` and is a `Semiring`, but is not an ordered ring, failed to synthesize
       OrderedRing α
 -/

tests/lean/run/infoFromFailure.lean

@@ -16,7 +16,11 @@ info: B.foo "hello" : String × String
 ---
 trace: [Meta.synthInstance] ❌️ Add String
   [Meta.synthInstance] new goal Add String
-    [Meta.synthInstance.instances] #[@Lean.Grind.AddCommMonoid.toAdd, @Lean.Grind.Semiring.toAdd]
+    [Meta.synthInstance.instances] #[@Lean.Grind.AddCommMonoid.toAdd, @Lean.Grind.Semiring.toAdd, @Lean.Grind.Order.Weight.toAdd]
+  [Meta.synthInstance] ✅️ apply @Lean.Grind.Order.Weight.toAdd to Add String
+    [Meta.synthInstance.tryResolve] ✅️ Add String ≟ Add String
+    [Meta.synthInstance] no instances for Lean.Grind.Order.Weight String
+      [Meta.synthInstance.instances] #[]
   [Meta.synthInstance] ✅️ apply @Lean.Grind.Semiring.toAdd to Add String
     [Meta.synthInstance.tryResolve] ✅️ Add String ≟ Add String
     [Meta.synthInstance] new goal Lean.Grind.Semiring String
@@ -73,7 +77,11 @@ trace: [Meta.synthInstance] ❌️ Add String
 /--
 trace: [Meta.synthInstance] ❌️ Add Bool
   [Meta.synthInstance] new goal Add Bool
-    [Meta.synthInstance.instances] #[@Lean.Grind.AddCommMonoid.toAdd, @Lean.Grind.Semiring.toAdd]
+    [Meta.synthInstance.instances] #[@Lean.Grind.AddCommMonoid.toAdd, @Lean.Grind.Semiring.toAdd, @Lean.Grind.Order.Weight.toAdd]
+  [Meta.synthInstance] ✅️ apply @Lean.Grind.Order.Weight.toAdd to Add Bool
+    [Meta.synthInstance.tryResolve] ✅️ Add Bool ≟ Add Bool
+    [Meta.synthInstance] no instances for Lean.Grind.Order.Weight Bool
+      [Meta.synthInstance.instances] #[]
   [Meta.synthInstance] ✅️ apply @Lean.Grind.Semiring.toAdd to Add Bool
     [Meta.synthInstance.tryResolve] ✅️ Add Bool ≟ Add Bool
     [Meta.synthInstance] new goal Lean.Grind.Semiring Bool

tests/lean/run/info_trees.lean

@@ -60,7 +60,7 @@ info: • [Command] @ ⟨77, 0⟩-⟨77, 40⟩ @ Lean.Elab.Command.elabDeclarati
                   ⊢ 0 ≤ n
                   after no goals
                   • [Term] Nat.zero_le n : 0 ≤ n @ ⟨1, 1⟩†-⟨1, 1⟩† @ Lean.Elab.Term.elabApp
-                    • [Completion-Id] Nat.zero_le : some LE.le.{0} Nat instLENat (OfNat.ofNat.{0} Nat 0 (instOfNatNat 0)) _uniq.37 @ ⟨1, 0⟩†-⟨1, 0⟩†
+                    • [Completion-Id] Nat.zero_le : some LE.le.{0} Nat instLENat (OfNat.ofNat.{0} Nat 0 (instOfNatNat 0)) _uniq.40 @ ⟨1, 0⟩†-⟨1, 0⟩†
                     • [Term] Nat.zero_le : ∀ (n : Nat), 0 ≤ n @ ⟨1, 0⟩†-⟨1, 0⟩†
                     • [Term] n : Nat @ ⟨1, 5⟩†-⟨1, 5⟩† @ Lean.Elab.Term.elabIdent
                       • [Completion-Id] n : some Nat @ ⟨1, 5⟩†-⟨1, 5⟩†