chore: fix tests

Users have not found them very useful

src/Init/Data/Int/OfNat.lean

@@ -88,6 +88,20 @@ theorem finVal {n : Nat} {a : Fin n} {a' : Int}
     (h₁ : Lean.Grind.ToInt.toInt a = a') : NatCast.natCast (a.val) = a' := by
   rw [← h₁, Lean.Grind.ToInt.toInt, Lean.Grind.instToIntFinCoOfNatIntCast]
 
+theorem eq_eq {a b : Nat} {a' b' : Int}
+    (h₁ : NatCast.natCast a = a') (h₂ : NatCast.natCast b = b') : (a = b) = (a' = b') := by
+  simp [← h₁, ←h₂]; constructor
+  next => intro; subst a; rfl
+  next => simp [Int.natCast_inj]
+
+theorem lt_eq {a b : Nat} {a' b' : Int}
+    (h₁ : NatCast.natCast a = a') (h₂ : NatCast.natCast b = b') : (a < b) = (a' < b') := by
+  simp only [← h₁, ← h₂, Int.ofNat_lt]
+
+theorem le_eq {a b : Nat} {a' b' : Int}
+    (h₁ : NatCast.natCast a = a') (h₂ : NatCast.natCast b = b') : (a ≤ b) = (a' ≤ b') := by
+  simp only [← h₁, ← h₂, Int.ofNat_le]
+
 end Nat.ToInt
 
 namespace Int.Nonneg

src/Init/Grind.lean

@@ -24,4 +24,3 @@ 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

@@ -1,299 +0,0 @@
-/-
-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/Ring/CommSolver.lean

@@ -1739,4 +1739,75 @@ noncomputable def norm_int_cert (e : Expr) (p : Poly) : Bool :=
 theorem norm_int (ctx : Context Int) (e : Expr) (p : Poly) : norm_int_cert e p → e.denote ctx = p.denote' ctx := by
   simp [norm_int_cert, Poly.denote'_eq_denote]; intro; subst p; simp [Expr.denote_toPoly]
 
+/-!
+Helper theorems for normalizing ring constraints in the `grind order` module.
+-/
+
+noncomputable def norm_cnstr_cert (lhs rhs lhs' rhs' : Expr) : Bool :=
+  (rhs.sub lhs).toPoly_k.beq' (rhs'.sub lhs').toPoly_k
+
+theorem le_norm_expr {α} [CommRing α] [LE α] [LT α] [IsPreorder α] [OrderedRing α] (ctx : Context α) (lhs rhs : Expr) (lhs' rhs' : Expr)
+    : norm_cnstr_cert lhs rhs lhs' rhs' → (lhs.denote ctx ≤ rhs.denote ctx) = (lhs'.denote ctx ≤ rhs'.denote ctx) := by
+  simp [norm_cnstr_cert]; intro h
+  replace h := congrArg (Poly.denote ctx) h; simp [Expr.denote_toPoly] at h
+  replace h : rhs.denote ctx - lhs.denote ctx = rhs'.denote ctx - lhs'.denote ctx := h
+  rw [← OrderedAdd.sub_nonneg_iff, h, OrderedAdd.sub_nonneg_iff]
+
+theorem lt_norm_expr {α} [CommRing α] [LE α] [LT α] [LawfulOrderLT α] [IsPreorder α] [OrderedRing α] (ctx : Context α) (lhs rhs : Expr) (lhs' rhs' : Expr)
+    : norm_cnstr_cert lhs rhs lhs' rhs' → (lhs.denote ctx < rhs.denote ctx) = (lhs'.denote ctx < rhs'.denote ctx) := by
+  simp [norm_cnstr_cert]; intro h
+  replace h := congrArg (Poly.denote ctx) h; simp [Expr.denote_toPoly] at h
+  replace h : rhs.denote ctx - lhs.denote ctx = rhs'.denote ctx - lhs'.denote ctx := h
+  rw [← OrderedAdd.sub_pos_iff, h, OrderedAdd.sub_pos_iff]
+
+noncomputable def norm_eq_cert (lhs rhs lhs' rhs' : Expr) : Bool :=
+  (lhs.sub rhs).toPoly_k.beq' (lhs'.sub rhs').toPoly_k
+
+theorem eq_norm_expr {α} [CommRing α] (ctx : Context α) (lhs rhs : Expr) (lhs' rhs' : Expr)
+    : norm_eq_cert lhs rhs lhs' rhs' → (lhs.denote ctx = rhs.denote ctx) = (lhs'.denote ctx = rhs'.denote ctx) := by
+  simp [norm_eq_cert]; intro h
+  replace h := congrArg (Poly.denote ctx) h; simp [Expr.denote_toPoly] at h
+  replace h : lhs.denote ctx - rhs.denote ctx = lhs'.denote ctx - rhs'.denote ctx := h
+  rw [← AddCommGroup.sub_eq_zero_iff, h, AddCommGroup.sub_eq_zero_iff]
+
+noncomputable def norm_cnstr_nc_cert (lhs rhs lhs' rhs' : Expr) : Bool :=
+  (rhs.sub lhs).toPoly_nc.beq' (rhs'.sub lhs').toPoly_nc
+
+theorem le_norm_expr_nc {α} [Ring α] [LE α] [LT α] [IsPreorder α] [OrderedRing α] (ctx : Context α) (lhs rhs : Expr) (lhs' rhs' : Expr)
+    : norm_cnstr_nc_cert lhs rhs lhs' rhs' → (lhs.denote ctx ≤ rhs.denote ctx) = (lhs'.denote ctx ≤ rhs'.denote ctx) := by
+  simp [norm_cnstr_nc_cert]; intro h
+  replace h := congrArg (Poly.denote ctx) h; simp [Expr.denote_toPoly_nc] at h
+  replace h : rhs.denote ctx - lhs.denote ctx = rhs'.denote ctx - lhs'.denote ctx := h
+  rw [← OrderedAdd.sub_nonneg_iff, h, OrderedAdd.sub_nonneg_iff]
+
+theorem lt_norm_expr_nc {α} [Ring α] [LE α] [LT α] [LawfulOrderLT α] [IsPreorder α] [OrderedRing α] (ctx : Context α) (lhs rhs : Expr) (lhs' rhs' : Expr)
+    : norm_cnstr_nc_cert lhs rhs lhs' rhs' → (lhs.denote ctx < rhs.denote ctx) = (lhs'.denote ctx < rhs'.denote ctx) := by
+  simp [norm_cnstr_nc_cert]; intro h
+  replace h := congrArg (Poly.denote ctx) h; simp [Expr.denote_toPoly_nc] at h
+  replace h : rhs.denote ctx - lhs.denote ctx = rhs'.denote ctx - lhs'.denote ctx := h
+  rw [← OrderedAdd.sub_pos_iff, h, OrderedAdd.sub_pos_iff]
+
+noncomputable def norm_eq_nc_cert (lhs rhs lhs' rhs' : Expr) : Bool :=
+  (lhs.sub rhs).toPoly_nc.beq' (lhs'.sub rhs').toPoly_nc
+
+theorem eq_norm_expr_nc {α} [Ring α] (ctx : Context α) (lhs rhs : Expr) (lhs' rhs' : Expr)
+    : norm_eq_nc_cert lhs rhs lhs' rhs' → (lhs.denote ctx = rhs.denote ctx) = (lhs'.denote ctx = rhs'.denote ctx) := by
+  simp [norm_eq_nc_cert]; intro h
+  replace h := congrArg (Poly.denote ctx) h; simp [Expr.denote_toPoly_nc] at h
+  replace h : lhs.denote ctx - rhs.denote ctx = lhs'.denote ctx - rhs'.denote ctx := h
+  rw [← AddCommGroup.sub_eq_zero_iff, h, AddCommGroup.sub_eq_zero_iff]
+
+/-!
+Helper theorems for quick normalization
+-/
+
+theorem le_norm0 {α} [Ring α] [LE α] (lhs rhs : α) : (lhs ≤ rhs) = (lhs ≤ rhs + Int.cast (R := α) 0) := by
+  rw [Ring.intCast_zero, Semiring.add_zero]
+
+theorem lt_norm0 {α} [Ring α] [LT α] (lhs rhs : α) : (lhs < rhs) = (lhs < rhs + Int.cast (R := α) 0) := by
+  rw [Ring.intCast_zero, Semiring.add_zero]
+
+theorem eq_norm0 {α} [Ring α] (lhs rhs : α) : (lhs = rhs) = (lhs = rhs + Int.cast (R := α) 0) := by
+  rw [Ring.intCast_zero, Semiring.add_zero]
+
 end Lean.Grind.CommRing

src/Lean/Expr.lean

@@ -2376,6 +2376,13 @@ private def intLEPred : Expr :=
 def mkIntLE (a b : Expr) : Expr :=
   mkApp2 intLEPred a b
 
+private def intLTPred : Expr :=
+  mkApp2 (mkConst ``LT.lt [0]) Int.mkType Int.mkInstLT
+
+/-- Given `a b : Int`, returns `a < b` -/
+def mkIntLT (a b : Expr) : Expr :=
+  mkApp2 intLTPred a b
+
 private def intEqPred : Expr :=
   mkApp (mkConst ``Eq [1]) Int.mkType
 

src/Lean/Meta/Tactic/Grind/Arith/CommRing/DenoteExpr.lean

@@ -66,8 +66,8 @@ def _root_.Lean.Grind.CommRing.Expr.denoteExpr (e : RingExpr) : M Expr := do
 where
   go : RingExpr → M Expr
   | .num k => denoteNum k
-  | .natCast k => denoteNum k
-  | .intCast k => denoteNum k
+  | .natCast k => return mkApp (← getNatCastFn) (mkNatLit k)
+  | .intCast k => return mkApp (← getIntCastFn) (mkIntLit k)
   | .var x => return (← getRing).vars[x]!
   | .add a b => return mkApp2 (← getAddFn) (← go a) (← go b)
   | .sub a b => return mkApp2 (← getSubFn) (← go a) (← go b)

src/Lean/Meta/Tactic/Grind/Arith/CommRing/Poly.lean

@@ -237,4 +237,37 @@ def Poly.length : Poly → Nat
   | .num _ => 0
   | .add _ _ p => 1 + p.length
 
+def Power.toExpr (pw : Power) : Expr :=
+  if pw.k == 1 then
+    .var pw.x
+  else
+    .pow (.var pw.x) pw.k
+
+def Mon.toExpr (m : Mon) : Expr :=
+  match m with
+  | .unit => .num 1
+  | .mult pw m => go m pw.toExpr
+where
+  go (m : Mon) (acc : Expr) : Expr :=
+    match m with
+    | .unit => acc
+    | .mult pw m => go m (.mul acc pw.toExpr)
+
+def Poly.toExpr (p : Poly) : Expr :=
+  match p with
+  | .num k => .num k
+  | .add k m p => go p (goTerm k m)
+where
+  goTerm (k : Int) (m : Mon) : Expr :=
+    if k == 1 then
+      m.toExpr
+    else
+      .mul (.num k) m.toExpr
+
+  go (p : Poly) (acc : Expr) : Expr :=
+    match p with
+    | .num 0 => acc
+    | .num k => .add acc (.num k)
+    | .add k m p => go p (.add acc (goTerm k m))
+
 end Lean.Grind.CommRing

src/Lean/Meta/Tactic/Grind/Arith/CommRing/Proof.lean

@@ -378,4 +378,64 @@ def setNonCommSemiringDiseqUnsat (a b : Expr) (sa sb : SemiringExpr) : NonCommSe
   let h := mkApp3 h (toExpr sa) (toExpr sb) eagerReflBoolTrue
   closeGoal (mkApp hne h)
 
+private structure NormResult where
+  lhs  : RingExpr
+  rhs  : RingExpr
+  lhs' : RingExpr
+  rhs' : RingExpr
+  vars : Array Expr
+
+private def norm (vars : PArray Expr) (lhs rhs lhs' rhs' : RingExpr) : NormResult :=
+  let usedVars     := lhs.collectVars >> lhs.collectVars >> lhs'.collectVars >> rhs'.collectVars <| {}
+  let vars'        := usedVars.toArray
+  let varRename    := mkVarRename vars'
+  let vars         := vars'.map fun x => vars[x]!
+  let lhs          := lhs.renameVars varRename
+  let rhs          := rhs.renameVars varRename
+  let lhs'         := lhs'.renameVars varRename
+  let rhs'         := rhs'.renameVars varRename
+  { lhs, rhs, lhs', rhs', vars }
+
+def mkLeIffProof (leInst ltInst isPreorderInst orderedRingInst : Expr) (lhs rhs lhs' rhs' : RingExpr) : RingM Expr := do
+  let ring ← getCommRing
+  let { lhs, rhs, lhs', rhs', vars } := norm ring.vars lhs rhs lhs' rhs'
+  let ctx ← toContextExpr vars
+  let h := mkApp6 (mkConst ``Grind.CommRing.le_norm_expr [ring.u]) ring.type ring.commRingInst leInst ltInst isPreorderInst orderedRingInst
+  return mkApp6 h ctx (toExpr lhs) (toExpr rhs) (toExpr lhs') (toExpr rhs') eagerReflBoolTrue
+
+def mkLtIffProof (leInst ltInst lawfulOrdLtInst isPreorderInst orderedRingInst : Expr) (lhs rhs lhs' rhs' : RingExpr) : RingM Expr := do
+  let ring ← getCommRing
+  let { lhs, rhs, lhs', rhs', vars } := norm ring.vars lhs rhs lhs' rhs'
+  let ctx ← toContextExpr vars
+  let h := mkApp7 (mkConst ``Grind.CommRing.lt_norm_expr [ring.u]) ring.type ring.commRingInst leInst ltInst lawfulOrdLtInst isPreorderInst orderedRingInst
+  return mkApp6 h ctx (toExpr lhs) (toExpr rhs) (toExpr lhs') (toExpr rhs') eagerReflBoolTrue
+
+def mkEqIffProof (lhs rhs lhs' rhs' : RingExpr) : RingM Expr := do
+  let ring ← getCommRing
+  let { lhs, rhs, lhs', rhs', vars } := norm ring.vars lhs rhs lhs' rhs'
+  let ctx ← toContextExpr vars
+  let h := mkApp2 (mkConst ``Grind.CommRing.eq_norm_expr [ring.u]) ring.type ring.commRingInst
+  return mkApp6 h ctx (toExpr lhs) (toExpr rhs) (toExpr lhs') (toExpr rhs') eagerReflBoolTrue
+
+def mkNonCommLeIffProof (leInst ltInst isPreorderInst orderedRingInst : Expr) (lhs rhs lhs' rhs' : RingExpr) : NonCommRingM Expr := do
+  let ring ← getRing
+  let { lhs, rhs, lhs', rhs', vars } := norm ring.vars lhs rhs lhs' rhs'
+  let ctx ← toContextExpr vars
+  let h := mkApp6 (mkConst ``Grind.CommRing.le_norm_expr_nc [ring.u]) ring.type ring.ringInst leInst ltInst isPreorderInst orderedRingInst
+  return mkApp6 h ctx (toExpr lhs) (toExpr rhs) (toExpr lhs') (toExpr rhs') eagerReflBoolTrue
+
+def mkNonCommLtIffProof (leInst ltInst lawfulOrdLtInst isPreorderInst orderedRingInst : Expr) (lhs rhs lhs' rhs' : RingExpr) : NonCommRingM Expr := do
+  let ring ← getRing
+  let { lhs, rhs, lhs', rhs', vars } := norm ring.vars lhs rhs lhs' rhs'
+  let ctx ← toContextExpr vars
+  let h := mkApp7 (mkConst ``Grind.CommRing.lt_norm_expr_nc [ring.u]) ring.type ring.ringInst leInst ltInst lawfulOrdLtInst isPreorderInst orderedRingInst
+  return mkApp6 h ctx (toExpr lhs) (toExpr rhs) (toExpr lhs') (toExpr rhs') eagerReflBoolTrue
+
+def mkNonCommEqIffProof (lhs rhs lhs' rhs' : RingExpr) : NonCommRingM Expr := do
+  let ring ← getRing
+  let { lhs, rhs, lhs', rhs', vars } := norm ring.vars lhs rhs lhs' rhs'
+  let ctx ← toContextExpr vars
+  let h := mkApp2 (mkConst ``Grind.CommRing.eq_norm_expr_nc [ring.u]) ring.type ring.ringInst
+  return mkApp6 h ctx (toExpr lhs) (toExpr rhs) (toExpr lhs') (toExpr rhs') eagerReflBoolTrue
+
 end Lean.Meta.Grind.Arith.CommRing

src/Lean/Meta/Tactic/Grind/Arith/Util.lean

@@ -101,6 +101,8 @@ def isArithTerm (e : Expr) : Bool :=
   | HSMul.hSMul _ _ _ _ _ _ => true
   | Neg.neg _ _ _ => true
   | OfNat.ofNat _ _ _ => true
+  | NatCast.natCast _ _ _ => true
+  | IntCast.intCast _ _ _ => true
   | _ => false
 
 /-- Quote `e` using `「` and `」` if `e` is an arithmetic term that is being treated as a variable. -/

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

@@ -6,11 +6,34 @@ Authors: Leonardo de Moura
 module
 prelude
 public import Lean.Meta.Tactic.Grind.Order.OrderM
+import Init.Data.Int.OfNat
+import Lean.Meta.Tactic.Grind.Arith.CommRing.RingM
+import Lean.Meta.Tactic.Grind.Arith.CommRing.NonCommRingM
+import Lean.Meta.Tactic.Grind.Arith.CommRing.Poly
+import Lean.Meta.Tactic.Grind.Arith.CommRing.SafePoly
+import Lean.Meta.Tactic.Grind.Arith.CommRing.Reify
+import Lean.Meta.Tactic.Grind.Arith.CommRing.Functions
+import Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr
+import Lean.Meta.Tactic.Grind.Arith.CommRing.Proof
+import Lean.Meta.Tactic.Grind.Arith.Cutsat.Nat
 import Lean.Meta.Tactic.Grind.Order.StructId
 namespace Lean.Meta.Grind.Order
 
+open Arith CommRing
+
 def getType? (e : Expr) : Option Expr :=
   match_expr e with
+  | Eq α lhs rhs =>
+    /-
+    **Note**: We only try internalize equalities if `lhs` or `rhs` arithmetic terms that may
+    need to be internalized. If they are not, normalization is not needed. Moreover, this is
+    an optimization for avoiding trying to infer order instances for "hopeless" types such as
+    `Bool`.
+    -/
+    if isArithTerm lhs || isArithTerm rhs then
+      some α
+    else
+      none
   | LE.le α _ _ _ => some α
   | LT.lt α _ _ _ => some α
   | HAdd.hAdd α _ _ _ _ _ => some α
@@ -24,13 +47,155 @@ def isForbiddenParent (parent? : Option Expr) : Bool :=
   else
     false
 
+def split (p : Poly) : Poly × Poly × Int :=
+  match p with
+  | .num k => (.num 0, .num 0, -k)
+  | .add k m p =>
+    let (lhs, rhs, c) := split p
+    if k < 0 then
+      (lhs, .add (-k) m rhs, c)
+    else
+      (.add k m lhs, rhs, c)
+
+def propEq := mkApp (mkConst ``Eq [1]) (mkSort 0)
+
+/--
+Given a proof `h` that `e ↔ rel lhs rhs`, add expected proposition hint around `h`.
+The relation `rel` is inferred from `kind`.
+-/
+def mkExpectedHint (s : Struct) (e : Expr) (kind : CnstrKind) (lhs rhs : Expr) (h : Expr) : Expr :=
+  let rel := match kind with
+    | .le => s.leFn
+    | .lt => s.ltFn?.get!
+    | .eq => mkApp (mkConst ``Eq [mkLevelSucc s.u]) s.type
+  let e' := mkApp2 rel lhs rhs
+  let prop :=  mkApp2 propEq e e'
+  mkExpectedPropHint h prop
+
+def mkLeNorm0 (s : Struct) (ringInst : Expr) (lhs rhs : Expr) : Expr :=
+  mkApp5 (mkConst ``Grind.CommRing.le_norm0 [s.u]) s.type ringInst s.leInst lhs rhs
+
+def mkLtNorm0 (s : Struct) (ringInst : Expr) (lhs rhs : Expr) : Expr :=
+  mkApp5 (mkConst ``Grind.CommRing.lt_norm0 [s.u]) s.type ringInst s.ltInst?.get! lhs rhs
+
+def mkEqNorm0 (s : Struct) (ringInst : Expr) (lhs rhs : Expr) : Expr :=
+  mkApp4 (mkConst ``Grind.CommRing.eq_norm0 [s.u]) s.type ringInst lhs rhs
+
+def mkCnstrNorm0 (s : Struct) (ringInst : Expr) (kind : CnstrKind) (lhs rhs : Expr) : Expr :=
+  match kind with
+  | .le => mkLeNorm0 s ringInst lhs rhs
+  | .lt => mkLtNorm0 s ringInst lhs rhs
+  | .eq => mkEqNorm0 s ringInst lhs rhs
+
+def mkCommRingCnstr? (e : Expr) (s : Struct) (kind : CnstrKind) (lhs rhs : Expr) : RingM (Option (Cnstr Expr)) := do
+  if !isArithTerm lhs && !isArithTerm rhs then
+    return some { u := lhs, v := rhs, k := 0, kind, h? := some (mkCnstrNorm0 s (← getRing).ringInst kind lhs rhs)  }
+  let some lhs ← reify? lhs (skipVar := false) | return none
+  let some rhs ← reify? rhs (skipVar := false) | return none
+  let p ← lhs.sub rhs |>.toPolyM
+  let (lhs', rhs', k) := split p
+  let lhs' := lhs'.toExpr
+  let rhs' := rhs'.toExpr
+  let u ← shareCommon (← lhs'.denoteExpr)
+  let v ← shareCommon (← rhs'.denoteExpr)
+  let rhs' : RingExpr := .add rhs' (.intCast k)
+  let h ← match kind with
+    | .le => mkLeIffProof s.leInst s.ltInst?.get! s.isPreorderInst s.orderedRingInst?.get! lhs rhs lhs' rhs'
+    | .lt => mkLtIffProof s.leInst s.ltInst?.get! s.lawfulOrderLTInst?.get! s.isPreorderInst s.orderedRingInst?.get! lhs rhs lhs' rhs'
+    | .eq => mkEqIffProof lhs rhs lhs' rhs'
+  let h := mkExpectedHint s e kind u (← rhs'.denoteExpr) h
+  return some {
+    kind, u, v, k, h? := some h
+  }
+
+def mkNonCommRingCnstr? (e : Expr) (s : Struct) (kind : CnstrKind) (lhs rhs : Expr) : NonCommRingM (Option (Cnstr Expr)) := do
+  if !isArithTerm lhs && !isArithTerm rhs then
+    return some { u := lhs, v := rhs, k := 0, kind, h? := some (mkCnstrNorm0 s (← getRing).ringInst kind lhs rhs)  }
+  let some lhs ← ncreify? lhs (skipVar := false) | return none
+  let some rhs ← ncreify? rhs (skipVar := false) | return none
+  -- **TODO**: We need a `toPolyM_nc` similar `toPolyM`
+  let p := lhs.sub rhs |>.toPoly_nc
+  let (lhs', rhs', k) := split p
+  let lhs' := lhs'.toExpr
+  let rhs' := rhs'.toExpr
+  let u ← shareCommon (← lhs'.denoteExpr)
+  let v ← shareCommon (← rhs'.denoteExpr)
+  let rhs' : RingExpr := .add rhs' (.intCast k)
+  let h ← match kind with
+    | .le => mkNonCommLeIffProof s.leInst s.ltInst?.get! s.isPreorderInst s.orderedRingInst?.get! lhs rhs lhs' rhs'
+    | .lt => mkNonCommLtIffProof s.leInst s.ltInst?.get! s.lawfulOrderLTInst?.get! s.isPreorderInst s.orderedRingInst?.get! lhs rhs lhs' rhs'
+    | .eq => mkNonCommEqIffProof lhs rhs lhs' rhs'
+  let h := mkExpectedHint s e kind u (← rhs'.denoteExpr) h
+  return some {
+    kind, u, v, k, h? := some h
+  }
+
+def mkCnstr? (e : Expr) (kind : CnstrKind) (lhs rhs : Expr) : OrderM (Option (Cnstr Expr)) := do
+  let s ← getStruct
+  if let some ringId := s.ringId? then
+    if s.isCommRing then
+      RingM.run ringId <| mkCommRingCnstr? e s kind lhs rhs
+    else
+      NonCommRingM.run ringId <| mkNonCommRingCnstr? e s kind lhs rhs
+  else
+    return some { kind, u := lhs, v := rhs }
+
+def internalizeCnstr (e : Expr) (kind : CnstrKind) (lhs rhs : Expr) : OrderM Unit := do
+  let some cnstr ← mkCnstr? e kind lhs rhs | return ()
+  trace[grind.order.internalize] "{cnstr.u}, {cnstr.v}, {cnstr.k}"
+  if grind.debug.get (← getOptions) then
+    if let some h := cnstr.h? then check h
+  -- **TODO**: update data-structures
+
+def hasLt : OrderM Bool :=
+  return (← getStruct).ltFn?.isSome
+
+open Arith.Cutsat in
+def adaptNat (e : Expr) : GoalM Expr := do
+  let (eNew, h) ← match_expr e with
+    | LE.le _ _ lhs rhs =>
+      let (lhs', h₁) ← natToInt lhs
+      let (rhs', h₂) ← natToInt rhs
+      let eNew := mkIntLE lhs' rhs'
+      let h := mkApp6 (mkConst ``Nat.ToInt.le_eq) lhs rhs lhs' rhs' h₁ h₂
+      pure (eNew, h)
+    | LT.lt _ _ lhs rhs =>
+      let (lhs', h₁) ← natToInt lhs
+      let (rhs', h₂) ← natToInt rhs
+      let eNew := mkIntLT lhs' rhs'
+      let h := mkApp6 (mkConst ``Nat.ToInt.lt_eq) lhs rhs lhs' rhs' h₁ h₂
+      pure (eNew, h)
+    | Eq _ lhs rhs =>
+      let (lhs', h₁) ← natToInt lhs
+      let (rhs', h₂) ← natToInt rhs
+      let eNew := mkIntEq lhs' rhs'
+      let h := mkApp6 (mkConst ``Nat.ToInt.eq_eq) lhs rhs lhs' rhs' h₁ h₂
+      pure (eNew, h)
+    | _ => return e
+  modify' fun s => { s with cnstrsMap := s.cnstrsMap.insert { expr := e } (eNew, h) }
+  return eNew
+
+def adapt (α : Expr) (e : Expr) : GoalM (Expr × Expr) := do
+  -- **Note**: We currently only adapt `Nat` expressions
+  if α == Nat.mkType then
+    let eNew ← adaptNat e
+    return ((← getIntExpr), eNew)
+  else
+    return (α, e)
+
 public def internalize (e : Expr) (parent? : Option Expr) : GoalM Unit := do
   unless (← getConfig).order do return ()
   let some α := getType? e | return ()
+  let (α, e) ← adapt α e
   if isForbiddenParent parent? then return ()
   let some structId ← getStructId? α | return ()
   OrderM.run structId do
-  trace[grind.order.internalize] "{e}"
-  -- TODO
+  match_expr e with
+  | LE.le _ _ lhs rhs => internalizeCnstr e .le lhs rhs
+  | LT.lt _ _ lhs rhs => if (← hasLt) then internalizeCnstr e .lt lhs rhs
+  | Eq _ lhs rhs => internalizeCnstr e .eq lhs rhs
+  | _ =>
+    -- TODO
+    return ()
 
 end Lean.Meta.Grind.Order

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

@@ -7,6 +7,8 @@ module
 prelude
 public import Lean.Meta.Tactic.Grind.Order.Types
 import Lean.Meta.Tactic.Grind.OrderInsts
+import Lean.Meta.Tactic.Grind.Arith.CommRing.RingId
+import Lean.Meta.Tactic.Grind.Arith.CommRing.NonCommRingM
 public section
 namespace Lean.Meta.Grind.Order
 
@@ -19,6 +21,13 @@ private def internalizeFn (fn : Expr) : GoalM Expr := do
 private def getInst? (declName : Name) (u : Level) (type : Expr) : GoalM (Option Expr) := do
   synthInstance? <| mkApp (mkConst declName [u]) type
 
+open Arith CommRing
+
+private def mkOrderedRingInst? (u : Level) (α : Expr) (semiringInst : Expr)
+    (leInst ltInst isPreorderInst : Expr) : GoalM (Option Expr) := do
+  let e := mkApp5 (mkConst ``Grind.OrderedRing [u]) α semiringInst leInst ltInst isPreorderInst
+  synthInstance? e
+
 def getStructId? (type : Expr) : GoalM (Option Nat) := do
   unless (← getConfig).order do return none
   if let some id? := (← get').typeIdOf.find? { expr := type } then
@@ -29,9 +38,10 @@ def getStructId? (type : Expr) : GoalM (Option Nat) := do
     return id?
 where
   go? : GoalM (Option Nat) := do
-    let u ← getDecLevel type
+    let some u ← getDecLevel? type | return none
     let some leInst ← getInst? ``LE u type | return none
     let some isPreorderInst ← mkIsPreorderInst? u type (some leInst) | return none
+    -- **TODO** compute `isPartialInst?` and `isLinearPreInst?` on demand
     let isPartialInst? ← mkIsPartialOrderInst? u type (some leInst)
     let isLinearPreInst? ← mkIsLinearPreorderInst? u type (some leInst)
     let ltInst? ← getInst? ``LT u type
@@ -45,10 +55,24 @@ where
         pure (inst?, some ltFn)
     else
       pure (none, none)
+    let (ringId?, orderedRingInst?, isCommRing) ← if lawfulOrderLTInst?.isNone then
+      pure (none, none, false)
+    else if let some ringId ← getCommRingId? type then
+      let semiringInst ← RingM.run ringId do return (← getRing).semiringInst
+      let some ordRingInst ← mkOrderedRingInst? u type semiringInst leInst ltInst?.get! isPreorderInst
+        | pure (none, none, true)
+      pure (some ringId, some ordRingInst, true)
+    else if let some ringId ← getNonCommRingId? type then
+      let semiringInst ← NonCommRingM.run ringId do return (← getRing).semiringInst
+      let some ordRingInst ← mkOrderedRingInst? u type semiringInst leInst ltInst?.get! isPreorderInst
+        | pure (none, none, true)
+      pure (some ringId, some ordRingInst, false)
+    else
+      pure (none, none, false)
     let id := (← get').structs.size
     let struct := {
-      id,  type, u, leInst, isPreorderInst, ltInst?, leFn, isPartialInst?
-      isLinearPreInst?, ltFn?, lawfulOrderLTInst?
+      id,  type, u, leInst, isPreorderInst, ltInst?, leFn, isPartialInst?, orderedRingInst?
+      isLinearPreInst?, ltFn?, lawfulOrderLTInst?, ringId?, isCommRing
      }
     modify' fun s => { s with structs := s.structs.push struct }
     return some id

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

@@ -17,22 +17,25 @@ 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.
+and `Int`. During proof construction we perform the necessary conversions.
 -/
 abbrev Weight := Int
 
+inductive CnstrKind where
+  | le | lt | eq
+  deriving Inhabited
+
 /--
-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.
+A constraint of the form `u ≤ v + k` (`u < v + k` if `strict := true`)
+Remark: If the order does not support offsets, then `k` is 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
+structure Cnstr (α : Type) where
+  kind   : CnstrKind
+  u      : α
+  v      : α
+  k      : Weight := 0
   h?     : Option Expr := none
   deriving Inhabited
 
@@ -71,8 +74,7 @@ instance : DecidableLT WeightS :=
 structure ProofInfo where
   w      : NodeId
   strict : Bool := false
-  k₁     : Rat := 0
-  k₂     : Rat := 0
+  k      : Int := 0
   proof  : Expr
   deriving Inhabited
 
@@ -110,20 +112,25 @@ structure Struct where
   isLinearPreInst?   : Option Expr
   /-- `LawfulOrderLT` instance if available -/
   lawfulOrderLTInst? : Option Expr
+  /-- `id` of the `CommRing` (or `Ring`) structure in the `grind ring` module if available. -/
+  ringId?            : Option Nat
+  /-- `true` if `ringId?` is the Id of a commutative ring -/
+  isCommRing         : Bool
+  /-- `OrderedRing` instance if available -/
+  orderedRingInst?   : 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 := {}
+  cnstrs             : PHashMap ExprPtr (Cnstr NodeId) := {}
   /--
   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)) := {}
+  cnstrsOf           : PHashMap (NodeId × NodeId) (List (Cnstr 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`.
@@ -142,7 +149,7 @@ structure Struct where
   -/
   proofs             : PArray (AssocList NodeId ProofInfo) := {}
   /-- Truth values and equalities to propagate to core. -/
-  propagate : List ToPropagate := []
+  propagate          : List ToPropagate := []
   deriving Inhabited
 
 /-- State for all order types detected by `grind`. -/
@@ -153,8 +160,14 @@ structure State where
   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. -/
+  /-- Mapping from expressions/terms to their structure ids. -/
   exprToStructId : PHashMap ExprPtr Nat := {}
+  /--
+  Mapping from terms/constraints that have been mapped into `Ring`s before being internalized.
+  Example: given `x y : Nat`, `x ≤ y + 1` is mapped to `Int.ofNat x ≤ Int.ofNat y + 1`, and proof
+  of equivalence.
+  -/
+  cnstrsMap : PHashMap ExprPtr (Expr × Expr) := {}
   deriving Inhabited
 
 builtin_initialize orderExt : SolverExtension State ← registerSolverExtension (return {})

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

@@ -17,7 +17,7 @@ def mkLawfulOrderLTInst? (u : Level) (type : Expr) (ltInst? leInst? : Option Exp
   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}"
+    | reportDbgIssue! "type has `LE` and `LT`, but the `LT` instance is not lawful, failed to synthesize{indentExpr lawfulOrderLTType}"
       return none
   return some inst
 
@@ -25,7 +25,7 @@ def mkIsPreorderInst? (u : Level) (type : Expr) (leInst? : Option Expr) : GoalM
   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}"
+    | reportDbgIssue! "type has `LE`, but is not a preorder, failed to synthesize{indentExpr isPreorderType}"
       return none
   return some inst
 
@@ -33,7 +33,7 @@ def mkIsPartialOrderInst? (u : Level) (type : Expr) (leInst? : Option Expr) : Go
   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}"
+    | reportDbgIssue! "type has `LE`, but is not a partial order, failed to synthesize{indentExpr isPartialOrderType}"
       return none
   return some inst
 
@@ -41,7 +41,7 @@ def mkIsLinearOrderInst? (u : Level) (type : Expr) (leInst?  : Option Expr) : Go
   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}"
+    | reportDbgIssue! "type has `LE`, but is not a linear order, failed to synthesize{indentExpr isLinearOrderType}"
       return none
   return some inst
 
@@ -49,7 +49,7 @@ def mkIsLinearPreorderInst? (u : Level) (type : Expr) (leInst?  : Option Expr) :
   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}"
+    | reportDbgIssue! "type has `LE`, but is not a linear preorder, failed to synthesize{indentExpr isLinearOrderType}"
       return none
   return some inst
 

tests/lean/run/grind_const_pattern.lean

@@ -19,7 +19,7 @@ h : ¬a = 10
   [eqc] False propositions
     [prop] a = 10
   [cutsat] Assignment satisfying linear constraints
-    [assign] a := 1
+    [assign] a := 0
 -/
 #guard_msgs (error) in
 example : a = 5 + 5 := by
@@ -50,8 +50,8 @@ h : ¬f a = 11
   [eqc] False propositions
     [prop] f a = 11
   [cutsat] Assignment satisfying linear constraints
-    [assign] a := 2
-    [assign] f a := 1
+    [assign] a := 1
+    [assign] f a := 0
 -/
 #guard_msgs (error) in
 example : f a = 10 + 1 := by
@@ -76,9 +76,9 @@ h : ¬f x = 11
   [ematch] E-matching patterns
     [thm] fa: [f `[a]]
   [cutsat] Assignment satisfying linear constraints
-    [assign] x := 3
-    [assign] a := 2
-    [assign] f x := 1
+    [assign] x := 2
+    [assign] a := 1
+    [assign] f x := 0
 -/
 #guard_msgs (error) in
 example : f x = 10 + 1 := by

tests/lean/run/grind_cutsat_nat_le.lean

@@ -32,17 +32,17 @@ example (a b : Int) : a + b = Int.ofNat 2 → a - 2 = -b := by
   grind
 
 /--
-trace: [grind.cutsat.assert] -1*↑a ≤ 0
-[grind.cutsat.assert] -1*↑b ≤ 0
+trace: [grind.cutsat.assert] -1*「↑a」 ≤ 0
+[grind.cutsat.assert] -1*「↑b」 ≤ 0
+[grind.cutsat.assert] -1*「↑c」 ≤ 0
 [grind.cutsat.assert] -1*「↑a * ↑b」 ≤ 0
-[grind.cutsat.assert] -1*↑c ≤ 0
-[grind.cutsat.assert] -1*「↑a * ↑b + -1 * ↑c + 1」 + 「↑a * ↑b」 + -1*↑c + 1 = 0
-[grind.cutsat.assert] 「↑a * ↑b」 + -1*↑c + 1 ≤ 0
-[grind.cutsat.assert] -1*↑0 = 0
-[grind.cutsat.assert] ↑c = 0
+[grind.cutsat.assert] -1*「↑a * ↑b + -1 * ↑c + 1」 + 「↑a * ↑b」 + -1*「↑c」 + 1 = 0
+[grind.cutsat.assert] 「↑a * ↑b」 + -1*「↑c」 + 1 ≤ 0
+[grind.cutsat.assert] -1*「↑0」 = 0
+[grind.cutsat.assert] 「↑c」 = 0
 [grind.cutsat.assert] 0 ≤ 0
 [grind.cutsat.assert] 「↑a * ↑b」 + 1 ≤ 0
-[grind.cutsat.assert] -1*↑0 + ↑c = 0
+[grind.cutsat.assert] -1*「↑0」 + 「↑c」 = 0
 [grind.cutsat.assert] 1 ≤ 0
 -/
 #guard_msgs (trace) in

tests/lean/run/grind_cutsat_toint_1.lean

@@ -90,7 +90,7 @@ example (a b : Fin 3) : a > 0 → a ≠ b → a + b ≠ 0 → a + b ≠ 1 → Fa
   grind
 
 -- We use `↑a` when pretty printing `ToInt.toInt a`
-/-- trace: [grind.debug.ring.basis] ↑a + ↑b + -3 * ((↑a + ↑b) / 3) + -1 * ((↑a + ↑b) % 3) = 0 -/
+/-- trace: [grind.debug.ring.basis] (↑a + ↑b) % 3 + -1 * ↑a + -1 * ↑b + 3 * ((↑a + ↑b) / 3) = 0 -/
 #guard_msgs (drop error, trace) in
 set_option trace.grind.debug.ring.basis true in
 example (a b : Fin 3) : a > 0 → a ≠ b → a + b ≠ 0 → a + b ≠ 1 → False := by

tests/lean/run/infoFromFailure.lean

@@ -16,11 +16,7 @@ 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, @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.instances] #[@Lean.Grind.AddCommMonoid.toAdd, @Lean.Grind.Semiring.toAdd]
   [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
@@ -77,11 +73,7 @@ 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, @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.instances] #[@Lean.Grind.AddCommMonoid.toAdd, @Lean.Grind.Semiring.toAdd]
   [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.40 @ ⟨1, 0⟩†-⟨1, 0⟩†
+                    • [Completion-Id] Nat.zero_le : some LE.le.{0} Nat instLENat (OfNat.ofNat.{0} Nat 0 (instOfNatNat 0)) _uniq.37 @ ⟨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⟩†