merge

src/Init/Grind/Ordered/Field.lean

@@ -13,18 +13,19 @@ namespace Lean.Grind
 
 namespace Field.IsOrdered
 
-variable {R : Type u} [Field R] [LinearOrder R] [Ring.IsOrdered R]
+variable {R : Type u} [Field R] [LinearOrder R] [OrderedRing R]
 
-open Ring.IsOrdered
+open OrderedAdd
+open OrderedRing
 
 theorem pos_of_inv_pos {a : R} (h : 0 < a⁻¹) : 0 < a := by
   rcases LinearOrder.trichotomy 0 a with (h' | rfl | h')
   · exact h'
   · simpa [Field.inv_zero] using h
   · exfalso
-    have := Ring.IsOrdered.mul_neg_of_pos_of_neg h h'
+    have := OrderedRing.mul_neg_of_pos_of_neg h h'
     rw [inv_mul_cancel (Preorder.ne_of_lt h')] at this
-    exact Ring.IsOrdered.not_one_lt_zero this
+    exact OrderedRing.not_one_lt_zero this
 
 theorem inv_pos_iff {a : R} : 0 < a⁻¹ ↔ 0 < a := by
   constructor
@@ -36,7 +37,7 @@ theorem inv_pos_iff {a : R} : 0 < a⁻¹ ↔ 0 < a := by
 theorem inv_neg_iff {a : R} : a⁻¹ < 0 ↔ a < 0 := by
   have := inv_pos_iff (a := -a)
   rw [Field.inv_neg] at this
-  simpa [IntModule.IsOrdered.neg_pos_iff]
+  simpa [neg_pos_iff]
 
 theorem inv_nonneg_iff {a : R} : 0 ≤ a⁻¹ ↔ 0 ≤ a := by
   simp [PartialOrder.le_iff_lt_or_eq, inv_pos_iff, Field.zero_eq_inv_iff]
@@ -44,15 +45,15 @@ theorem inv_nonneg_iff {a : R} : 0 ≤ a⁻¹ ↔ 0 ≤ a := by
 theorem inv_nonpos_iff {a : R} : a⁻¹ ≤ 0 ↔ a ≤ 0 := by
   have := inv_nonneg_iff (a := -a)
   rw [Field.inv_neg] at this
-  simpa [IntModule.IsOrdered.neg_nonneg_iff] using this
+  simpa [neg_nonneg_iff] using this
 
 private theorem mul_le_of_le_mul_inv {a b c : R} (h : 0 < c) (h' : a ≤ b * c⁻¹) : a * c ≤ b := by
   simpa [Semiring.mul_assoc, Field.inv_mul_cancel (Preorder.ne_of_gt h), Semiring.mul_one] using
-    Ring.IsOrdered.mul_le_mul_of_nonneg_right h' (Preorder.le_of_lt h)
+    OrderedRing.mul_le_mul_of_nonneg_right h' (Preorder.le_of_lt h)
 
 private theorem le_mul_inv_of_mul_le {a b c : R} (h : 0 < b) (h' : a * b ≤ c) : a ≤ c * b⁻¹ := by
   simpa [Semiring.mul_assoc, Field.mul_inv_cancel (Preorder.ne_of_gt h), Semiring.mul_one] using
-    Ring.IsOrdered.mul_le_mul_of_nonneg_right h' (Preorder.le_of_lt (inv_pos_iff.mpr h))
+    OrderedRing.mul_le_mul_of_nonneg_right h' (Preorder.le_of_lt (inv_pos_iff.mpr h))
 
 theorem le_mul_inv_iff_mul_le (a b : R) {c : R} (h : 0 < c) : a ≤ b * c⁻¹ ↔ a * c ≤ b :=
   ⟨mul_le_of_le_mul_inv h, le_mul_inv_of_mul_le h⟩
@@ -63,11 +64,11 @@ private theorem mul_inv_le_iff_le_mul (a c : R) {b : R} (h : 0 < b) : a * b⁻¹
 
 private theorem mul_lt_of_lt_mul_inv {a b c : R} (h : 0 < c) (h' : a < b * c⁻¹) : a * c < b := by
   simpa [Semiring.mul_assoc, Field.inv_mul_cancel (Preorder.ne_of_gt h), Semiring.mul_one] using
-    Ring.IsOrdered.mul_lt_mul_of_pos_right h' h
+    OrderedRing.mul_lt_mul_of_pos_right h' h
 
 private theorem lt_mul_inv_of_mul_lt {a b c : R} (h : 0 < b) (h' : a * b < c) : a < c * b⁻¹ := by
   simpa [Semiring.mul_assoc, Field.mul_inv_cancel (Preorder.ne_of_gt h), Semiring.mul_one] using
-    Ring.IsOrdered.mul_lt_mul_of_pos_right h' (inv_pos_iff.mpr h)
+    OrderedRing.mul_lt_mul_of_pos_right h' (inv_pos_iff.mpr h)
 
 theorem lt_mul_inv_iff_mul_lt (a b : R) {c : R} (h : 0 < c) : a < b * c⁻¹ ↔ a * c < b :=
   ⟨mul_lt_of_lt_mul_inv h, lt_mul_inv_of_mul_lt h⟩
@@ -77,19 +78,19 @@ theorem mul_inv_lt_iff_lt_mul (a c : R) {b : R} (h : 0 < b) : a * b⁻¹ < c ↔
 
 private theorem le_mul_of_le_mul_inv {a b c : R} (h : c < 0) (h' : a ≤ b * c⁻¹) : b ≤ a * c := by
   simpa [Semiring.mul_assoc, Field.inv_mul_cancel (Preorder.ne_of_lt h), Semiring.mul_one] using
-    Ring.IsOrdered.mul_le_mul_of_nonpos_right h' (Preorder.le_of_lt h)
+    OrderedRing.mul_le_mul_of_nonpos_right h' (Preorder.le_of_lt h)
 
 private theorem mul_le_of_mul_inv_le {a b c : R} (h : b < 0) (h' : a * b⁻¹ ≤ c) : c * b ≤ a := by
   simpa [Semiring.mul_assoc, Field.inv_mul_cancel (Preorder.ne_of_lt h), Semiring.mul_one] using
-    Ring.IsOrdered.mul_le_mul_of_nonpos_right h' (Preorder.le_of_lt h)
+    OrderedRing.mul_le_mul_of_nonpos_right h' (Preorder.le_of_lt h)
 
 private theorem mul_inv_le_of_mul_le {a b c : R} (h : b < 0) (h' : a * b ≤ c) : c * b⁻¹ ≤ a := by
   simpa [Semiring.mul_assoc, Field.mul_inv_cancel (Preorder.ne_of_lt h), Semiring.mul_one] using
-    Ring.IsOrdered.mul_le_mul_of_nonpos_right h' (Preorder.le_of_lt (inv_neg_iff.mpr h))
+    OrderedRing.mul_le_mul_of_nonpos_right h' (Preorder.le_of_lt (inv_neg_iff.mpr h))
 
 private theorem le_mul_inv_of_le_mul {a b c : R} (h : c < 0) (h' : a ≤ b * c) : b ≤ a * c⁻¹ := by
   simpa [Semiring.mul_assoc, Field.mul_inv_cancel (Preorder.ne_of_lt h), Semiring.mul_one] using
-    Ring.IsOrdered.mul_le_mul_of_nonpos_right h' (Preorder.le_of_lt (inv_neg_iff.mpr h))
+    OrderedRing.mul_le_mul_of_nonpos_right h' (Preorder.le_of_lt (inv_neg_iff.mpr h))
 
 theorem le_mul_inv_iff_le_mul_of_neg (a b : R) {c : R} (h : c < 0) : a ≤ b * c⁻¹ ↔ b ≤ a * c :=
   ⟨le_mul_of_le_mul_inv h, le_mul_inv_of_le_mul h⟩
@@ -99,19 +100,19 @@ theorem mul_inv_le_iff_mul_le_of_neg (a c : R) {b : R} (h : b < 0) : a * b⁻¹
 
 private theorem lt_mul_of_lt_mul_inv {a b c : R} (h : c < 0) (h' : a < b * c⁻¹) : b < a * c := by
   simpa [Semiring.mul_assoc, Field.inv_mul_cancel (Preorder.ne_of_lt h), Semiring.mul_one] using
-    Ring.IsOrdered.mul_lt_mul_of_neg_right h' h
+    OrderedRing.mul_lt_mul_of_neg_right h' h
 
 private theorem mul_lt_of_mul_inv_lt {a b c : R} (h : b < 0) (h' : a * b⁻¹ < c) : c * b < a := by
   simpa [Semiring.mul_assoc, Field.inv_mul_cancel (Preorder.ne_of_lt h), Semiring.mul_one] using
-    Ring.IsOrdered.mul_lt_mul_of_neg_right h' h
+    OrderedRing.mul_lt_mul_of_neg_right h' h
 
 private theorem mul_inv_lt_of_mul_lt {a b c : R} (h : b < 0) (h' : a * b < c) : c * b⁻¹ < a := by
   simpa [Semiring.mul_assoc, Field.mul_inv_cancel (Preorder.ne_of_lt h), Semiring.mul_one] using
-    Ring.IsOrdered.mul_lt_mul_of_neg_right h' (inv_neg_iff.mpr h)
+    OrderedRing.mul_lt_mul_of_neg_right h' (inv_neg_iff.mpr h)
 
 private theorem lt_mul_inv_of_lt_mul {a b c : R} (h : c < 0) (h' : a < b * c) : b < a * c⁻¹ := by
   simpa [Semiring.mul_assoc, Field.mul_inv_cancel (Preorder.ne_of_lt h), Semiring.mul_one] using
-    Ring.IsOrdered.mul_lt_mul_of_neg_right h' (inv_neg_iff.mpr h)
+    OrderedRing.mul_lt_mul_of_neg_right h' (inv_neg_iff.mpr h)
 
 theorem lt_mul_inv_iff_lt_mul_of_neg (a b : R) {c : R} (h : c < 0) : a < b * c⁻¹ ↔ b < a * c :=
   ⟨lt_mul_of_lt_mul_inv h, lt_mul_inv_of_lt_mul h⟩

src/Init/Grind/Ordered/Int.lean

@@ -21,13 +21,10 @@ instance : Preorder Int where
   le_trans := Int.le_trans
   lt_iff_le_not_le := by omega
 
-instance : IntModule.IsOrdered Int where
-  neg_le_iff := by omega
-  add_le_left := by omega
-  hmul_pos_iff k a ha := ⟨fun h => Int.pos_of_mul_pos_left h ha, fun hk => Int.mul_pos hk ha⟩
-  hmul_nonneg hk ha := Int.mul_nonneg hk ha
+instance : OrderedAdd Int where
+  add_le_left_iff := by omega
 
-instance : Ring.IsOrdered Int where
+instance : OrderedRing Int where
   zero_lt_one := by omega
   mul_lt_mul_of_pos_left := Int.mul_lt_mul_of_pos_left
   mul_lt_mul_of_pos_right := Int.mul_lt_mul_of_pos_right

src/Init/Grind/Ordered/Linarith.lean

@@ -246,23 +246,23 @@ def Poly.leadCoeff (p : Poly) : Int :=
   | .add a _ _ => a
   | _ => 1
 
-open IntModule.IsOrdered
+open OrderedAdd
 
 /-!
 Helper theorems for conflict resolution during model construction.
 -/
 
-private theorem le_add_le {α} [IntModule α] [Preorder α] [IntModule.IsOrdered α] {a b : α}
+private theorem le_add_le {α} [IntModule α] [Preorder α] [OrderedAdd α] {a b : α}
     (h₁ : a ≤ 0) (h₂ : b ≤ 0) : a + b ≤ 0 := by
   replace h₁ := add_le_left h₁ b; simp at h₁
   exact Preorder.le_trans h₁ h₂
 
-private theorem le_add_lt {α} [IntModule α] [Preorder α] [IntModule.IsOrdered α] {a b : α}
+private theorem le_add_lt {α} [IntModule α] [Preorder α] [OrderedAdd α] {a b : α}
     (h₁ : a ≤ 0) (h₂ : b < 0) : a + b < 0 := by
   replace h₁ := add_le_left h₁ b; simp at h₁
   exact Preorder.lt_of_le_of_lt h₁ h₂
 
-private theorem lt_add_lt {α} [IntModule α] [Preorder α] [IntModule.IsOrdered α] {a b : α}
+private theorem lt_add_lt {α} [IntModule α] [Preorder α] [OrderedAdd α] {a b : α}
     (h₁ : a < 0) (h₂ : b < 0) : a + b < 0 := by
   replace h₁ := add_lt_left h₁ b; simp at h₁
   exact Preorder.lt_trans h₁ h₂
@@ -275,11 +275,11 @@ def le_le_combine_cert (p₁ p₂ p₃ : Poly) : Bool :=
   let a₂ := p₂.leadCoeff.natAbs
   p₃ == (p₁.mul a₂ |>.combine (p₂.mul a₁))
 
-theorem le_le_combine {α} [IntModule α] [Preorder α] [IntModule.IsOrdered α] (ctx : Context α) (p₁ p₂ p₃ : Poly)
+theorem le_le_combine {α} [IntModule α] [Preorder α] [OrderedAdd α] (ctx : Context α) (p₁ p₂ p₃ : Poly)
     : le_le_combine_cert p₁ p₂ p₃ → p₁.denote' ctx ≤ 0 → p₂.denote' ctx ≤ 0 → p₃.denote' ctx ≤ 0 := by
   simp [le_le_combine_cert]; intro _ h₁ h₂; subst p₃; simp
-  replace h₁ := hmul_nonpos (coe_natAbs_nonneg p₂.leadCoeff) h₁
-  replace h₂ := hmul_nonpos (coe_natAbs_nonneg p₁.leadCoeff) h₂
+  replace h₁ := hmul_int_nonpos (coe_natAbs_nonneg p₂.leadCoeff) h₁
+  replace h₂ := hmul_int_nonpos (coe_natAbs_nonneg p₁.leadCoeff) h₂
   exact le_add_le h₁ h₂
 
 def le_lt_combine_cert (p₁ p₂ p₃ : Poly) : Bool :=
@@ -287,11 +287,11 @@ def le_lt_combine_cert (p₁ p₂ p₃ : Poly) : Bool :=
   let a₂ := p₂.leadCoeff.natAbs
   a₁ > (0 : Int) && p₃ == (p₁.mul a₂ |>.combine (p₂.mul a₁))
 
-theorem le_lt_combine {α} [IntModule α] [Preorder α] [IntModule.IsOrdered α] (ctx : Context α) (p₁ p₂ p₃ : Poly)
+theorem le_lt_combine {α} [IntModule α] [Preorder α] [OrderedAdd α] (ctx : Context α) (p₁ p₂ p₃ : Poly)
     : le_lt_combine_cert p₁ p₂ p₃ → p₁.denote' ctx ≤ 0 → p₂.denote' ctx < 0 → p₃.denote' ctx < 0 := by
   simp [-Int.natAbs_pos, -Int.ofNat_pos, le_lt_combine_cert]; intro hp _ h₁ h₂; subst p₃; simp
-  replace h₁ := hmul_nonpos (coe_natAbs_nonneg p₂.leadCoeff) h₁
-  replace h₂ := hmul_neg_iff (↑p₁.leadCoeff.natAbs) h₂ |>.mpr hp
+  replace h₁ := hmul_int_nonpos (coe_natAbs_nonneg p₂.leadCoeff) h₁
+  replace h₂ := hmul_int_neg_iff (↑p₁.leadCoeff.natAbs) h₂ |>.mpr hp
   exact le_add_lt h₁ h₂
 
 def lt_lt_combine_cert (p₁ p₂ p₃ : Poly) : Bool :=
@@ -299,18 +299,18 @@ def lt_lt_combine_cert (p₁ p₂ p₃ : Poly) : Bool :=
   let a₂ := p₂.leadCoeff.natAbs
   a₂ > (0 : Int) && a₁ > (0 : Int) && p₃ == (p₁.mul a₂ |>.combine (p₂.mul a₁))
 
-theorem lt_lt_combine {α} [IntModule α] [Preorder α] [IntModule.IsOrdered α] (ctx : Context α) (p₁ p₂ p₃ : Poly)
+theorem lt_lt_combine {α} [IntModule α] [Preorder α] [OrderedAdd α] (ctx : Context α) (p₁ p₂ p₃ : Poly)
     : lt_lt_combine_cert p₁ p₂ p₃ → p₁.denote' ctx < 0 → p₂.denote' ctx < 0 → p₃.denote' ctx < 0 := by
   simp [-Int.natAbs_pos, -Int.ofNat_pos, lt_lt_combine_cert]; intro hp₁ hp₂ _ h₁ h₂; subst p₃; simp
-  replace h₁ := hmul_neg_iff (↑p₂.leadCoeff.natAbs) h₁ |>.mpr hp₁
-  replace h₂ := hmul_neg_iff (↑p₁.leadCoeff.natAbs) h₂ |>.mpr hp₂
+  replace h₁ := hmul_int_neg_iff (↑p₂.leadCoeff.natAbs) h₁ |>.mpr hp₁
+  replace h₂ := hmul_int_neg_iff (↑p₁.leadCoeff.natAbs) h₂ |>.mpr hp₂
   exact lt_add_lt h₁ h₂
 
 def diseq_split_cert (p₁ p₂ : Poly) : Bool :=
   p₂ == p₁.mul (-1)
 
 -- We need `LinearOrder` to use `trichotomy`
-theorem diseq_split {α} [IntModule α] [LinearOrder α] [IntModule.IsOrdered α] (ctx : Context α) (p₁ p₂ : Poly)
+theorem diseq_split {α} [IntModule α] [LinearOrder α] [OrderedAdd α] (ctx : Context α) (p₁ p₂ : Poly)
     : diseq_split_cert p₁ p₂ → p₁.denote' ctx ≠ 0 → p₁.denote' ctx < 0 ∨ p₂.denote' ctx < 0 := by
   simp [diseq_split_cert]; intro _ h₁; subst p₂; simp
   cases LinearOrder.trichotomy (p₁.denote ctx) 0
@@ -320,7 +320,7 @@ theorem diseq_split {α} [IntModule α] [LinearOrder α] [IntModule.IsOrdered α
     simp [h₁] at h
     rw [← neg_pos_iff, neg_hmul, neg_neg, one_hmul]; assumption
 
-theorem diseq_split_resolve {α} [IntModule α] [LinearOrder α] [IntModule.IsOrdered α] (ctx : Context α) (p₁ p₂ : Poly)
+theorem diseq_split_resolve {α} [IntModule α] [LinearOrder α] [OrderedAdd α] (ctx : Context α) (p₁ p₂ : Poly)
     : diseq_split_cert p₁ p₂ → p₁.denote' ctx ≠ 0 → ¬p₁.denote' ctx < 0 → p₂.denote' ctx < 0 := by
   intro h₁ h₂ h₃
   exact (diseq_split ctx p₁ p₂ h₁ h₂).resolve_left h₃
@@ -336,7 +336,7 @@ theorem eq_norm {α} [IntModule α] (ctx : Context α) (lhs rhs : Expr) (p : Pol
     : norm_cert lhs rhs p → lhs.denote ctx = rhs.denote ctx → p.denote' ctx = 0 := by
   simp [norm_cert]; intro _ h₁; subst p; simp [Expr.denote, h₁, sub_self]
 
-theorem le_of_eq {α} [IntModule α] [Preorder α] [IntModule.IsOrdered α] (ctx : Context α) (lhs rhs : Expr) (p : Poly)
+theorem le_of_eq {α} [IntModule α] [Preorder α] [OrderedAdd α] (ctx : Context α) (lhs rhs : Expr) (p : Poly)
     : norm_cert lhs rhs p → lhs.denote ctx = rhs.denote ctx → p.denote' ctx ≤ 0 := by
   simp [norm_cert]; intro _ h₁; subst p; simp [Expr.denote, h₁, sub_self]
   apply Preorder.le_refl
@@ -349,21 +349,21 @@ theorem diseq_norm {α} [IntModule α] (ctx : Context α) (lhs rhs : Expr) (p :
   rw [add_left_comm, ← sub_eq_add_neg, sub_self, add_zero] at h
   contradiction
 
-theorem le_norm {α} [IntModule α] [Preorder α] [IntModule.IsOrdered α] (ctx : Context α) (lhs rhs : Expr) (p : Poly)
+theorem le_norm {α} [IntModule α] [Preorder α] [OrderedAdd α] (ctx : Context α) (lhs rhs : Expr) (p : Poly)
     : norm_cert lhs rhs p → lhs.denote ctx ≤ rhs.denote ctx → p.denote' ctx ≤ 0 := by
   simp [norm_cert]; intro _ h₁; subst p; simp [Expr.denote]
   replace h₁ := add_le_left h₁ (-rhs.denote ctx)
   simp [← sub_eq_add_neg, sub_self] at h₁
   assumption
 
-theorem lt_norm {α} [IntModule α] [Preorder α] [IntModule.IsOrdered α] (ctx : Context α) (lhs rhs : Expr) (p : Poly)
+theorem lt_norm {α} [IntModule α] [Preorder α] [OrderedAdd α] (ctx : Context α) (lhs rhs : Expr) (p : Poly)
     : norm_cert lhs rhs p → lhs.denote ctx < rhs.denote ctx → p.denote' ctx < 0 := by
   simp [norm_cert]; intro _ h₁; subst p; simp [Expr.denote]
   replace h₁ := add_lt_left h₁ (-rhs.denote ctx)
   simp [← sub_eq_add_neg, sub_self] at h₁
   assumption
 
-theorem not_le_norm {α} [IntModule α] [LinearOrder α] [IntModule.IsOrdered α] (ctx : Context α) (lhs rhs : Expr) (p : Poly)
+theorem not_le_norm {α} [IntModule α] [LinearOrder α] [OrderedAdd α] (ctx : Context α) (lhs rhs : Expr) (p : Poly)
     : norm_cert rhs lhs p → ¬ lhs.denote ctx ≤ rhs.denote ctx → p.denote' ctx < 0 := by
   simp [norm_cert]; intro _ h₁; subst p; simp [Expr.denote]
   replace h₁ := LinearOrder.lt_of_not_le h₁
@@ -371,7 +371,7 @@ theorem not_le_norm {α} [IntModule α] [LinearOrder α] [IntModule.IsOrdered α
   simp [← sub_eq_add_neg, sub_self] at h₁
   assumption
 
-theorem not_lt_norm {α} [IntModule α] [LinearOrder α] [IntModule.IsOrdered α] (ctx : Context α) (lhs rhs : Expr) (p : Poly)
+theorem not_lt_norm {α} [IntModule α] [LinearOrder α] [OrderedAdd α] (ctx : Context α) (lhs rhs : Expr) (p : Poly)
     : norm_cert rhs lhs p → ¬ lhs.denote ctx < rhs.denote ctx → p.denote' ctx ≤ 0 := by
   simp [norm_cert]; intro _ h₁; subst p; simp [Expr.denote]
   replace h₁ := LinearOrder.le_of_not_lt h₁
@@ -381,14 +381,14 @@ theorem not_lt_norm {α} [IntModule α] [LinearOrder α] [IntModule.IsOrdered α
 
 -- If the module does not have a linear order, we can still put the expressions in polynomial forms
 
-theorem not_le_norm' {α} [IntModule α] [Preorder α] [IntModule.IsOrdered α] (ctx : Context α) (lhs rhs : Expr) (p : Poly)
+theorem not_le_norm' {α} [IntModule α] [Preorder α] [OrderedAdd α] (ctx : Context α) (lhs rhs : Expr) (p : Poly)
     : norm_cert lhs rhs p → ¬ lhs.denote ctx ≤ rhs.denote ctx → ¬ p.denote' ctx ≤ 0 := by
   simp [norm_cert]; intro _ h₁; subst p; simp [Expr.denote]; intro h
   replace h := add_le_right (rhs.denote ctx) h
   rw [sub_eq_add_neg, add_left_comm, ← sub_eq_add_neg, sub_self] at h; simp at h
   contradiction
 
-theorem not_lt_norm' {α} [IntModule α] [Preorder α] [IntModule.IsOrdered α] (ctx : Context α) (lhs rhs : Expr) (p : Poly)
+theorem not_lt_norm' {α} [IntModule α] [Preorder α] [OrderedAdd α] (ctx : Context α) (lhs rhs : Expr) (p : Poly)
     : norm_cert lhs rhs p → ¬ lhs.denote ctx < rhs.denote ctx → ¬ p.denote' ctx < 0 := by
   simp [norm_cert]; intro _ h₁; subst p; simp [Expr.denote]; intro h
   replace h := add_lt_right (rhs.denote ctx) h
@@ -401,7 +401,7 @@ Equality detection
 def eq_of_le_ge_cert (p₁ p₂ : Poly) : Bool :=
   p₂ == p₁.mul (-1)
 
-theorem eq_of_le_ge {α} [IntModule α] [PartialOrder α] [IntModule.IsOrdered α] (ctx : Context α) (p₁ : Poly) (p₂ : Poly)
+theorem eq_of_le_ge {α} [IntModule α] [PartialOrder α] [OrderedAdd α] (ctx : Context α) (p₁ : Poly) (p₂ : Poly)
     : eq_of_le_ge_cert p₁ p₂ → p₁.denote' ctx ≤ 0 → p₂.denote' ctx ≤ 0 → p₁.denote' ctx = 0 := by
   simp [eq_of_le_ge_cert]
   intro; subst p₂; simp
@@ -425,18 +425,18 @@ theorem lt_unsat {α} [IntModule α] [Preorder α] (ctx : Context α) : (Poly.ni
 def zero_lt_one_cert (p : Poly) : Bool :=
   p == .add (-1) 0 .nil
 
-theorem zero_lt_one {α} [Ring α] [Preorder α] [Ring.IsOrdered α] (ctx : Context α) (p : Poly)
+theorem zero_lt_one {α} [Ring α] [Preorder α] [OrderedRing α] (ctx : Context α) (p : Poly)
     : zero_lt_one_cert p → (0 : Var).denote ctx = One.one → p.denote' ctx < 0 := by
   simp [zero_lt_one_cert]; intro _ h; subst p; simp [Poly.denote, h, One.one, neg_hmul]
-  rw [neg_lt_iff, neg_zero]; apply Ring.IsOrdered.zero_lt_one
+  rw [neg_lt_iff, neg_zero]; apply OrderedRing.zero_lt_one
 
 def zero_ne_one_cert (p : Poly) : Bool :=
   p == .add 1 0 .nil
 
-theorem zero_ne_one_of_ord_ring {α} [Ring α] [Preorder α] [Ring.IsOrdered α] (ctx : Context α) (p : Poly)
+theorem zero_ne_one_of_ord_ring {α} [Ring α] [Preorder α] [OrderedRing α] (ctx : Context α) (p : Poly)
     : zero_ne_one_cert p → (0 : Var).denote ctx = One.one → p.denote' ctx ≠ 0 := by
   simp [zero_ne_one_cert]; intro _ h; subst p; simp [Poly.denote, h, One.one]
-  intro h; have := Ring.IsOrdered.zero_lt_one (R := α); simp [h, Preorder.lt_irrefl] at this
+  intro h; have := OrderedRing.zero_lt_one (R := α); simp [h, Preorder.lt_irrefl] at this
 
 theorem zero_ne_one_of_field {α} [Field α] (ctx : Context α) (p : Poly)
     : zero_ne_one_cert p → (0 : Var).denote ctx = One.one → p.denote' ctx ≠ 0 := by
@@ -482,22 +482,22 @@ theorem eq_coeff {α} [IntModule α] [NoNatZeroDivisors α] (ctx : Context α) (
 def coeff_cert (p₁ p₂ : Poly) (k : Nat) :=
   k > 0 && p₁ == p₂.mul k
 
-theorem le_coeff {α} [IntModule α] [LinearOrder α] [IntModule.IsOrdered α] (ctx : Context α) (p₁ p₂ : Poly) (k : Nat)
+theorem le_coeff {α} [IntModule α] [LinearOrder α] [OrderedAdd α] (ctx : Context α) (p₁ p₂ : Poly) (k : Nat)
     : coeff_cert p₁ p₂ k → p₁.denote' ctx ≤ 0 → p₂.denote' ctx ≤ 0 := by
   simp [coeff_cert]; intro h _; subst p₁; simp
   have : ↑k > (0 : Int) := Int.natCast_pos.mpr h
   intro h₁; apply Classical.byContradiction
   intro h₂; replace h₂ := LinearOrder.lt_of_not_le h₂
-  replace h₂ := IsOrdered.hmul_pos_iff (↑k) h₂ |>.mpr this
+  replace h₂ := hmul_int_pos_iff (↑k) h₂ |>.mpr this
   exact Preorder.lt_irrefl 0 (Preorder.lt_of_lt_of_le h₂ h₁)
 
-theorem lt_coeff {α} [IntModule α] [LinearOrder α] [IntModule.IsOrdered α] (ctx : Context α) (p₁ p₂ : Poly) (k : Nat)
+theorem lt_coeff {α} [IntModule α] [LinearOrder α] [OrderedAdd α] (ctx : Context α) (p₁ p₂ : Poly) (k : Nat)
     : coeff_cert p₁ p₂ k → p₁.denote' ctx < 0 → p₂.denote' ctx < 0 := by
   simp [coeff_cert]; intro h _; subst p₁; simp
   have : ↑k > (0 : Int) := Int.natCast_pos.mpr h
   intro h₁; apply Classical.byContradiction
   intro h₂; replace h₂ := LinearOrder.le_of_not_lt h₂
-  replace h₂ := IsOrdered.hmul_nonneg (Int.le_of_lt this) h₂
+  replace h₂ := hmul_int_nonneg (Int.le_of_lt this) h₂
   exact Preorder.lt_irrefl 0 (Preorder.lt_of_le_of_lt h₂ h₁)
 
 theorem diseq_neg {α} [IntModule α] (ctx : Context α) (p p' : Poly) : p' == p.mul (-1) → p.denote' ctx ≠ 0 → p'.denote' ctx ≠ 0 := by
@@ -542,20 +542,20 @@ def eq_le_subst_cert (x : Var) (p₁ p₂ p₃ : Poly) :=
   let b := p₂.coeff x
   a ≥ 0 && p₃ == (p₂.mul a |>.combine (p₁.mul (-b)))
 
-theorem eq_le_subst {α} [IntModule α] [Preorder α] [IntModule.IsOrdered α] (ctx : Context α) (x : Var) (p₁ p₂ p₃ : Poly)
+theorem eq_le_subst {α} [IntModule α] [Preorder α] [OrderedAdd α] (ctx : Context α) (x : Var) (p₁ p₂ p₃ : Poly)
     : eq_le_subst_cert x p₁ p₂ p₃ → p₁.denote' ctx = 0 → p₂.denote' ctx ≤ 0 → p₃.denote' ctx ≤ 0 := by
   simp [eq_le_subst_cert]; intro h _ h₁ h₂; subst p₃; simp [h₁]
-  exact hmul_nonpos h h₂
+  exact hmul_int_nonpos h h₂
 
 def eq_lt_subst_cert (x : Var) (p₁ p₂ p₃ : Poly) :=
   let a := p₁.coeff x
   let b := p₂.coeff x
   a > 0 && p₃ == (p₂.mul a |>.combine (p₁.mul (-b)))
 
-theorem eq_lt_subst {α} [IntModule α] [Preorder α] [IntModule.IsOrdered α] (ctx : Context α) (x : Var) (p₁ p₂ p₃ : Poly)
+theorem eq_lt_subst {α} [IntModule α] [Preorder α] [OrderedAdd α] (ctx : Context α) (x : Var) (p₁ p₂ p₃ : Poly)
     : eq_lt_subst_cert x p₁ p₂ p₃ → p₁.denote' ctx = 0 → p₂.denote' ctx < 0 → p₃.denote' ctx < 0 := by
   simp [eq_lt_subst_cert]; intro h _ h₁ h₂; subst p₃; simp [h₁]
-  exact IsOrdered.hmul_neg_iff (p₁.coeff x) h₂ |>.mpr h
+  exact hmul_int_neg_iff (p₁.coeff x) h₂ |>.mpr h
 
 def eq_eq_subst_cert (x : Var) (p₁ p₂ p₃ : Poly) :=
   let a := p₁.coeff x

src/Init/Grind/Ordered/Module.lean

@@ -13,35 +13,19 @@ import Init.Grind.Ordered.Order
 namespace Lean.Grind
 
 /--
-A module over the natural numbers which is also equipped with a preorder is considered an
-ordered module if addition is compatible with the preorder.
+Addition is compatible with a preorder if `a ≤ b ↔ a + c ≤ b + c`.
 -/
-class NatModule.IsOrdered (M : Type u) [Preorder M] [NatModule M] where
+class OrderedAdd (M : Type u) [HAdd M M M] [Preorder M] where
   /-- `a + c ≤ b + c` iff `a ≤ b`. -/
   add_le_left_iff : ∀ {a b : M} (c : M), a ≤ b ↔ a + c ≤ b + c
 
--- This class is actually redundant; it is available automatically when we have an
--- `IntModule` satisfying `NatModule.IsOrdered`.
--- Replace with a custom constructor?
-/--
-A module over the integers which is also equipped with a preorder is considered an
-ordered module if addition and negation are compatible with the preorder.
--/
-class IntModule.IsOrdered (M : Type u) [Preorder M] [IntModule M] where
-  /-- `-a ≤ b` iff `-b ≤ a`. -/
-  neg_le_iff : ∀ a b : M, -a ≤ b ↔ -b ≤ a
-  /-- `a + c ≤ b + c` iff `a ≤ b`. -/
-  add_le_left : ∀ {a b : M}, a ≤ b → (c : M) → a + c ≤ b + c
-  /-- -/
-  hmul_pos_iff : ∀ (k : Int) {a : M}, 0 < a → (0 < k * a ↔ 0 < k)
-  /-- -/
-  hmul_nonneg : ∀ {k : Int} {a : M}, 0 ≤ k → 0 ≤ a → 0 ≤ k * a
+namespace OrderedAdd
 
-namespace NatModule.IsOrdered
+open NatModule
 
 section
 
-variable {M : Type u} [Preorder M] [NatModule M] [NatModule.IsOrdered M]
+variable {M : Type u} [Preorder M] [NatModule M] [OrderedAdd M]
 
 theorem add_le_right_iff {a b : M} (c : M) : a ≤ b ↔ c + a ≤ c + b := by
   rw [add_comm c a, add_comm c b, add_le_left_iff]
@@ -121,51 +105,44 @@ end
 
 section
 
-variable {M : Type u} [Preorder M] [IntModule M] [NatModule.IsOrdered M]
+variable {M : Type u} [Preorder M] [IntModule M] [OrderedAdd M]
 
 theorem neg_le_iff {a b : M} : -a ≤ b ↔ -b ≤ a := by
-  rw [NatModule.IsOrdered.add_le_left_iff a, IntModule.neg_add_cancel]
-  conv => rhs; rw [NatModule.IsOrdered.add_le_left_iff b, IntModule.neg_add_cancel]
+  rw [OrderedAdd.add_le_left_iff a, IntModule.neg_add_cancel]
+  conv => rhs; rw [OrderedAdd.add_le_left_iff b, IntModule.neg_add_cancel]
   rw [add_comm]
 
 end
-
-end NatModule.IsOrdered
-
-namespace IntModule.IsOrdered
-
 section
 
-variable {M : Type u} [Preorder M] [IntModule M] [NatModule.IsOrdered M]
+variable {M : Type u} [Preorder M] [IntModule M] [OrderedAdd M]
 
-open NatModule.IsOrdered in
-instance : IntModule.IsOrdered M where
-  neg_le_iff a b := NatModule.IsOrdered.neg_le_iff
-  add_le_left := NatModule.IsOrdered.add_le_left
-  hmul_pos_iff k x :=
-    match k with
-    | (k + 1 : Nat) => by
-      intro h
-      simpa [hmul_zero, ← hmul_nat] using hmul_lt_hmul_iff (k := k + 1) h
-    | (0 : Nat) => by simp [zero_hmul]; intro h; exact Preorder.lt_irrefl 0
-    | -(k + 1 : Nat) => by
-      intro h
-      have : ¬ (k : Int) + 1 < 0 := by omega
-      simp [this]; clear this
-      rw [neg_hmul]
-      rw [Preorder.lt_iff_le_not_le]
-      simp
-      intro h'
-      rw [NatModule.IsOrdered.neg_le_iff, neg_zero]
-      simpa [hmul_zero, ← hmul_nat] using hmul_le_hmul (k := k + 1) (Preorder.le_of_lt h)
-  hmul_nonneg {k a} h :=
-    match k, h with
-    | (k : Nat), _ => by
-      simpa [hmul_nat] using NatModule.IsOrdered.hmul_nonneg
+theorem hmul_int_pos_iff (k : Int) {x : M} (h : 0 < x) : 0 < k * x ↔ 0 < k :=
+  match k with
+  | (k + 1 : Nat) => by
+    simpa [IntModule.hmul_zero, ← IntModule.hmul_nat] using hmul_lt_hmul_iff (k := k + 1) h
+  | (0 : Nat) => by simp [IntModule.zero_hmul]; exact Preorder.lt_irrefl 0
+  | -(k + 1 : Nat) => by
+    have : ¬ (k : Int) + 1 < 0 := by omega
+    simp [this]; clear this
+    rw [IntModule.neg_hmul]
+    rw [Preorder.lt_iff_le_not_le]
+    simp
+    intro h'
+    rw [OrderedAdd.neg_le_iff, IntModule.neg_zero]
+    simpa [IntModule.hmul_zero, ← IntModule.hmul_nat] using
+      hmul_le_hmul (k := k + 1) (Preorder.le_of_lt h)
+
+theorem hmul_int_nonneg {k : Int} {x : M} (h : 0 ≤ k) (hx : 0 ≤ x) : 0 ≤ k * x :=
+  match k, h with
+  | (k : Nat), _ => by
+    simpa [IntModule.hmul_nat] using OrderedAdd.hmul_nonneg hx
 
 end
 
-variable {M : Type u} [Preorder M] [IntModule M] [IntModule.IsOrdered M]
+variable {M : Type u} [Preorder M] [IntModule M] [OrderedAdd M]
+
+open IntModule
 
 theorem le_neg_iff {a b : M} : a ≤ -b ↔ b ≤ -a := by
   conv => lhs; rw [← neg_neg a]
@@ -185,89 +162,33 @@ theorem neg_nonneg_iff {a : M} : 0 ≤ -a ↔ a ≤ 0 := by
 theorem neg_pos_iff {a : M} : 0 < -a ↔ a < 0 := by
   rw [lt_neg_iff, neg_zero]
 
-theorem add_lt_left {a b : M} (h : a < b) (c : M) : a + c < b + c := by
-  simp only [Preorder.lt_iff_le_not_le] at h ⊢
-  constructor
-  · exact add_le_left h.1 _
-  · intro w
-    apply h.2
-    replace w := add_le_left w (-c)
-    rw [add_assoc, add_assoc, add_neg_cancel, add_zero, add_zero] at w
-    exact w
-
-theorem add_le_right (a : M) {b c : M} (h : b ≤ c) : a + b ≤ a + c := by
-  rw [add_comm a b, add_comm a c]
-  exact add_le_left h a
-
-theorem add_lt_right (a : M) {b c : M} (h : b < c) : a + b < a + c := by
-  rw [add_comm a b, add_comm a c]
-  exact add_lt_left h a
-
-theorem add_le_left_iff {a b : M} (c : M) : a ≤ b ↔ a + c ≤ b + c := by
-  constructor
-  · intro w
-    exact add_le_left w c
-  · intro w
-    have := add_le_left w (-c)
-    rwa [add_assoc, add_neg_cancel, add_zero, add_assoc, add_neg_cancel, add_zero] at this
-
-theorem add_le_right_iff {a b : M} (c : M) : a ≤ b ↔ c + a ≤ c + b := by
-  constructor
-  · intro w
-    exact add_le_right c w
-  · intro w
-    have := add_le_right (-c) w
-    rwa [← add_assoc, neg_add_cancel, zero_add, ← add_assoc, neg_add_cancel, zero_add] at this
-
-theorem add_lt_left_iff {a b : M} (c : M) : a < b ↔ a + c < b + c := by
-  constructor
-  · intro w
-    exact add_lt_left w c
-  · intro w
-    have := add_lt_left w (-c)
-    rwa [add_assoc, add_neg_cancel, add_zero, add_assoc, add_neg_cancel, add_zero] at this
-
-theorem add_lt_right_iff {a b : M} (c : M) : a < b ↔ c + a < c + b := by
-  constructor
-  · intro w
-    exact add_lt_right c w
-  · intro w
-    have := add_lt_right (-c) w
-    rwa [← add_assoc, neg_add_cancel, zero_add, ← add_assoc, neg_add_cancel, zero_add] at this
-
 theorem sub_nonneg_iff {a b : M} : 0 ≤ a - b ↔ b ≤ a := by
-  rw [add_le_left_iff b, zero_add, sub_add_cancel]
+  rw [add_le_left_iff b, IntModule.zero_add, sub_add_cancel]
 
 theorem sub_pos_iff {a b : M} : 0 < a - b ↔ b < a := by
-  rw [add_lt_left_iff b, zero_add, sub_add_cancel]
+  rw [add_lt_left_iff b, IntModule.zero_add, sub_add_cancel]
 
-theorem hmul_neg_iff (k : Int) {a : M} (h : a < 0) : k * a < 0 ↔ 0 < k := by
-  simpa [IntModule.hmul_neg, neg_pos_iff] using hmul_pos_iff k (neg_pos_iff.mpr h)
+theorem hmul_int_neg_iff (k : Int) {a : M} (h : a < 0) : k * a < 0 ↔ 0 < k := by
+  simpa [IntModule.hmul_neg, neg_pos_iff] using hmul_int_pos_iff k (neg_pos_iff.mpr h)
 
-theorem hmul_nonpos {k : Int} {a : M} (hk : 0 ≤ k) (ha : a ≤ 0) : k * a ≤ 0 := by
-  simpa [IntModule.hmul_neg, neg_nonneg_iff] using hmul_nonneg hk (neg_nonneg_iff.mpr ha)
+theorem hmul_int_nonpos {k : Int} {a : M} (hk : 0 ≤ k) (ha : a ≤ 0) : k * a ≤ 0 := by
+  simpa [IntModule.hmul_neg, neg_nonneg_iff] using hmul_int_nonneg hk (neg_nonneg_iff.mpr ha)
 
-theorem hmul_le_hmul {a b : M} {k : Int} (hk : 0 ≤ k) (h : a ≤ b) : k * a ≤ k * b := by
-  simpa [hmul_sub, sub_nonneg_iff] using hmul_nonneg hk (sub_nonneg_iff.mpr h)
+theorem hmul_int_le_hmul_int {a b : M} {k : Int} (hk : 0 ≤ k) (h : a ≤ b) : k * a ≤ k * b := by
+  simpa [hmul_sub, sub_nonneg_iff] using hmul_int_nonneg hk (sub_nonneg_iff.mpr h)
 
-theorem hmul_lt_hmul_iff (k : Int) {a b : M} (h : a < b) : k * a < k * b ↔ 0 < k := by
-  simpa [hmul_sub, sub_pos_iff] using hmul_pos_iff k (sub_pos_iff.mpr h)
+theorem hmul_int_lt_hmul_int_iff (k : Int) {a b : M} (h : a < b) : k * a < k * b ↔ 0 < k := by
+  simpa [hmul_sub, sub_pos_iff] using hmul_int_pos_iff k (sub_pos_iff.mpr h)
 
-theorem hmul_le_hmul_of_le_of_le_of_nonneg_of_nonneg
+theorem hmul_int_le_hmul_int_of_le_of_le_of_nonneg_of_nonneg
     {k₁ k₂ : Int} {x y : M} (hk : k₁ ≤ k₂) (h : x ≤ y) (w : 0 ≤ k₁) (w' : 0 ≤ x) :
     k₁ * x ≤ k₂ * y := by
   apply Preorder.le_trans
-  · have : 0 ≤ k₁ * (y - x) := hmul_nonneg w (sub_nonneg_iff.mpr h)
+  · have : 0 ≤ k₁ * (y - x) := hmul_int_nonneg w (sub_nonneg_iff.mpr h)
     rwa [IntModule.hmul_sub, sub_nonneg_iff] at this
-  · have : 0 ≤ (k₂ - k₁) * y := hmul_nonneg (Int.sub_nonneg.mpr hk) (Preorder.le_trans w' h)
+  · have : 0 ≤ (k₂ - k₁) * y := hmul_int_nonneg (Int.sub_nonneg.mpr hk) (Preorder.le_trans w' h)
     rwa [IntModule.sub_hmul, sub_nonneg_iff] at this
 
-theorem add_le_add {a b c d : M} (hab : a ≤ b) (hcd : c ≤ d) : a + c ≤ b + d :=
-  Preorder.le_trans (add_le_right a hcd) (add_le_left hab d)
-
-instance : NatModule.IsOrdered M where
-  add_le_left_iff := add_le_left_iff
-
-end IntModule.IsOrdered
+end OrderedAdd
 
 end Lean.Grind

src/Init/Grind/Ordered/Ring.lean

@@ -15,7 +15,7 @@ namespace Lean.Grind
 A ring which is also equipped with a preorder is considered a strict ordered ring if addition, negation,
 and multiplication are compatible with the preorder, and `0 < 1`.
 -/
-class Ring.IsOrdered (R : Type u) [Ring R] [Preorder R] extends NatModule.IsOrdered R where
+class OrderedRing (R : Type u) [Ring R] [Preorder R] extends OrderedAdd R where
   /-- In a strict ordered semiring, we have `0 < 1`. -/
   zero_lt_one : (0 : R) < 1
   /-- In a strict ordered semiring, we can multiply an inequality `a < b` on the left
@@ -25,17 +25,17 @@ class Ring.IsOrdered (R : Type u) [Ring R] [Preorder R] extends NatModule.IsOrde
   by a positive element `0 < c` to obtain `a * c < b * c`. -/
   mul_lt_mul_of_pos_right : ∀ {a b c : R}, a < b → 0 < c → a * c < b * c
 
-namespace Ring.IsOrdered
+namespace OrderedRing
 
 variable {R : Type u} [Ring R]
 
 section Preorder
 
-variable [Preorder R] [Ring.IsOrdered R]
+variable [Preorder R] [OrderedRing R]
 
 theorem neg_one_lt_zero : (-1 : R) < 0 := by
   have h := zero_lt_one (R := R)
-  have := NatModule.IsOrdered.add_lt_left h (-1)
+  have := OrderedAdd.add_lt_left h (-1)
   rw [Semiring.zero_add, Ring.add_neg_cancel] at this
   assumption
 
@@ -43,14 +43,14 @@ theorem ofNat_nonneg (x : Nat) : (OfNat.ofNat x : R) ≥ 0 := by
   induction x
   next => simp [OfNat.ofNat, Zero.zero]; apply Preorder.le_refl
   next n ih =>
-    have := Ring.IsOrdered.zero_lt_one (R := R)
+    have := OrderedRing.zero_lt_one (R := R)
     rw [Semiring.ofNat_succ]
-    replace ih := NatModule.IsOrdered.add_le_left ih 1
+    replace ih := OrderedAdd.add_le_left ih 1
     rw [Semiring.zero_add] at ih
     have := Preorder.lt_of_lt_of_le this ih
     exact Preorder.le_of_lt this
 
-instance [Ring α] [Preorder α] [Ring.IsOrdered α] : IsCharP α 0 := IsCharP.mk' _ _ <| by
+instance [Ring α] [Preorder α] [OrderedRing α] : IsCharP α 0 := IsCharP.mk' _ _ <| by
   intro x
   simp only [Nat.mod_zero]; constructor
   next =>
@@ -63,9 +63,9 @@ instance [Ring α] [Preorder α] [Ring.IsOrdered α] : IsCharP α 0 := IsCharP.m
       rw [Ring.sub_eq_add_neg, Semiring.add_assoc, Ring.add_neg_cancel,
           Ring.sub_eq_add_neg, Semiring.zero_add, Semiring.add_zero] at h
       have h₁ : (OfNat.ofNat x : α) < 0 := by
-        have := Ring.IsOrdered.neg_one_lt_zero (R := α)
+        have := OrderedRing.neg_one_lt_zero (R := α)
         rw [h]; assumption
-      have h₂ := Ring.IsOrdered.ofNat_nonneg (R := α) x
+      have h₂ := OrderedRing.ofNat_nonneg (R := α) x
       have : (0 : α) < 0 := Preorder.lt_of_le_of_lt h₂ h₁
       simp
       exact (Preorder.lt_irrefl 0) this
@@ -75,7 +75,7 @@ end Preorder
 
 section PartialOrder
 
-variable [PartialOrder R] [Ring.IsOrdered R]
+variable [PartialOrder R] [OrderedRing R]
 
 theorem zero_le_one : (0 : R) ≤ 1 := Preorder.le_of_lt zero_lt_one
 
@@ -104,57 +104,59 @@ theorem mul_le_mul_of_nonneg_right {a b c : R} (h : a ≤ b) (h' : 0 ≤ c) : a
     | inr h => subst h; exact Preorder.le_refl (a * c)
   | inr h' => subst h'; simp [Semiring.mul_zero, Preorder.le_refl]
 
+open OrderedAdd
+
 theorem mul_le_mul_of_nonpos_left {a b c : R} (h : a ≤ b) (h' : c ≤ 0) : c * b ≤ c * a := by
-  have := mul_le_mul_of_nonneg_left h (IntModule.IsOrdered.neg_nonneg_iff.mpr h')
-  rwa [Ring.neg_mul, Ring.neg_mul, IntModule.IsOrdered.neg_le_iff, IntModule.neg_neg] at this
+  have := mul_le_mul_of_nonneg_left h (neg_nonneg_iff.mpr h')
+  rwa [Ring.neg_mul, Ring.neg_mul, neg_le_iff, IntModule.neg_neg] at this
 
 theorem mul_le_mul_of_nonpos_right {a b c : R} (h : a ≤ b) (h' : c ≤ 0) : b * c ≤ a * c := by
-  have := mul_le_mul_of_nonneg_right h (IntModule.IsOrdered.neg_nonneg_iff.mpr h')
-  rwa [Ring.mul_neg, Ring.mul_neg, IntModule.IsOrdered.neg_le_iff, IntModule.neg_neg] at this
+  have := mul_le_mul_of_nonneg_right h (neg_nonneg_iff.mpr h')
+  rwa [Ring.mul_neg, Ring.mul_neg, neg_le_iff, IntModule.neg_neg] at this
 
 theorem mul_lt_mul_of_neg_left {a b c : R} (h : a < b) (h' : c < 0) : c * b < c * a := by
-  have := mul_lt_mul_of_pos_left h (IntModule.IsOrdered.neg_pos_iff.mpr h')
-  rwa [Ring.neg_mul, Ring.neg_mul, IntModule.IsOrdered.neg_lt_iff, IntModule.neg_neg] at this
+  have := mul_lt_mul_of_pos_left h (neg_pos_iff.mpr h')
+  rwa [Ring.neg_mul, Ring.neg_mul, neg_lt_iff, IntModule.neg_neg] at this
 
 theorem mul_lt_mul_of_neg_right {a b c : R} (h : a < b) (h' : c < 0) : b * c < a * c := by
-  have := mul_lt_mul_of_pos_right h (IntModule.IsOrdered.neg_pos_iff.mpr h')
-  rwa [Ring.mul_neg, Ring.mul_neg, IntModule.IsOrdered.neg_lt_iff, IntModule.neg_neg] at this
+  have := mul_lt_mul_of_pos_right h (neg_pos_iff.mpr h')
+  rwa [Ring.mul_neg, Ring.mul_neg, neg_lt_iff, IntModule.neg_neg] at this
 
 theorem mul_nonneg {a b : R} (h₁ : 0 ≤ a) (h₂ : 0 ≤ b) : 0 ≤ a * b := by
   simpa [Semiring.zero_mul] using mul_le_mul_of_nonneg_right h₁ h₂
 
 theorem mul_nonneg_of_nonpos_of_nonpos {a b : R} (h₁ : a ≤ 0) (h₂ : b ≤ 0) : 0 ≤ a * b := by
-  have := mul_nonneg (IntModule.IsOrdered.neg_nonneg_iff.mpr h₁) (IntModule.IsOrdered.neg_nonneg_iff.mpr h₂)
+  have := mul_nonneg (neg_nonneg_iff.mpr h₁) (neg_nonneg_iff.mpr h₂)
   simpa [Ring.neg_mul, Ring.mul_neg, Ring.neg_neg] using this
 
 theorem mul_nonpos_of_nonneg_of_nonpos {a b : R} (h₁ : 0 ≤ a) (h₂ : b ≤ 0) : a * b ≤ 0 := by
-  rw [← IntModule.IsOrdered.neg_nonneg_iff, ← Ring.mul_neg]
-  apply mul_nonneg h₁ (IntModule.IsOrdered.neg_nonneg_iff.mpr h₂)
+  rw [← neg_nonneg_iff, ← Ring.mul_neg]
+  apply mul_nonneg h₁ (neg_nonneg_iff.mpr h₂)
 
 theorem mul_nonpos_of_nonpos_of_nonneg {a b : R} (h₁ : a ≤ 0) (h₂ : 0 ≤ b) : a * b ≤ 0 := by
-  rw [← IntModule.IsOrdered.neg_nonneg_iff, ← Ring.neg_mul]
-  apply mul_nonneg (IntModule.IsOrdered.neg_nonneg_iff.mpr h₁) h₂
+  rw [← neg_nonneg_iff, ← Ring.neg_mul]
+  apply mul_nonneg (neg_nonneg_iff.mpr h₁) h₂
 
 theorem mul_pos {a b : R} (h₁ : 0 < a) (h₂ : 0 < b) : 0 < a * b := by
   simpa [Semiring.zero_mul] using mul_lt_mul_of_pos_right h₁ h₂
 
 theorem mul_pos_of_neg_of_neg {a b : R} (h₁ : a < 0) (h₂ : b < 0) : 0 < a * b := by
-  have := mul_pos (IntModule.IsOrdered.neg_pos_iff.mpr h₁) (IntModule.IsOrdered.neg_pos_iff.mpr h₂)
+  have := mul_pos (neg_pos_iff.mpr h₁) (neg_pos_iff.mpr h₂)
   simpa [Ring.neg_mul, Ring.mul_neg, Ring.neg_neg] using this
 
 theorem mul_neg_of_pos_of_neg {a b : R} (h₁ : 0 < a) (h₂ : b < 0) : a * b < 0 := by
-  rw [← IntModule.IsOrdered.neg_pos_iff, ← Ring.mul_neg]
-  apply mul_pos h₁ (IntModule.IsOrdered.neg_pos_iff.mpr h₂)
+  rw [← neg_pos_iff, ← Ring.mul_neg]
+  apply mul_pos h₁ (neg_pos_iff.mpr h₂)
 
 theorem mul_neg_of_neg_of_pos {a b : R} (h₁ : a < 0) (h₂ : 0 < b) : a * b < 0 := by
-  rw [← IntModule.IsOrdered.neg_pos_iff, ← Ring.neg_mul]
-  apply mul_pos (IntModule.IsOrdered.neg_pos_iff.mpr h₁) h₂
+  rw [← neg_pos_iff, ← Ring.neg_mul]
+  apply mul_pos (neg_pos_iff.mpr h₁) h₂
 
 end PartialOrder
 
 section LinearOrder
 
-variable [LinearOrder R] [Ring.IsOrdered R]
+variable [LinearOrder R] [OrderedRing R]
 
 theorem mul_nonneg_iff {a b : R} : 0 ≤ a * b ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0 := by
   rcases LinearOrder.trichotomy 0 a with (ha | rfl | ha)
@@ -203,6 +205,6 @@ theorem sq_pos {a : R} (h : a ≠ 0) : 0 < a^2 := by
 
 end LinearOrder
 
-end Ring.IsOrdered
+end OrderedRing
 
 end Lean.Grind

src/Init/Grind/Ring/Poly.lean

@@ -1178,23 +1178,23 @@ theorem diseq_norm {α} [CommRing α] (ctx : Context α) (lhs rhs : Expr) (p : P
   simp [core_cert, Poly.denoteAsIntModule_eq_denote]; intro _ h; subst p; simp [Expr.denote_toPoly, Expr.denote]
   intro h; rw [sub_eq_zero_iff] at h; contradiction
 
-open IntModule.IsOrdered
+open OrderedAdd
 
-theorem le_norm {α} [CommRing α] [Preorder α] [Ring.IsOrdered α] (ctx : Context α) (lhs rhs : Expr) (p : Poly)
+theorem le_norm {α} [CommRing α] [Preorder α] [OrderedRing α] (ctx : Context α) (lhs rhs : Expr) (p : Poly)
     : core_cert lhs rhs p → lhs.denote ctx ≤ rhs.denote ctx → p.denoteAsIntModule ctx ≤ 0 := by
   simp [core_cert, Poly.denoteAsIntModule_eq_denote]; intro _ h; subst p; simp [Expr.denote_toPoly, Expr.denote]
   replace h := add_le_left h ((-1) * rhs.denote ctx)
   rw [neg_mul, ← sub_eq_add_neg, one_mul, ← sub_eq_add_neg, sub_self] at h
   assumption
 
-theorem lt_norm {α} [CommRing α] [Preorder α] [Ring.IsOrdered α] (ctx : Context α) (lhs rhs : Expr) (p : Poly)
+theorem lt_norm {α} [CommRing α] [Preorder α] [OrderedRing α] (ctx : Context α) (lhs rhs : Expr) (p : Poly)
     : core_cert lhs rhs p → lhs.denote ctx < rhs.denote ctx → p.denoteAsIntModule ctx < 0 := by
   simp [core_cert, Poly.denoteAsIntModule_eq_denote]; intro _ h; subst p; simp [Expr.denote_toPoly, Expr.denote]
   replace h := add_lt_left h ((-1) * rhs.denote ctx)
   rw [neg_mul, ← sub_eq_add_neg, one_mul, ← sub_eq_add_neg, sub_self] at h
   assumption
 
-theorem not_le_norm {α} [CommRing α] [LinearOrder α] [Ring.IsOrdered α] (ctx : Context α) (lhs rhs : Expr) (p : Poly)
+theorem not_le_norm {α} [CommRing α] [LinearOrder α] [OrderedRing α] (ctx : Context α) (lhs rhs : Expr) (p : Poly)
     : core_cert rhs lhs p → ¬ lhs.denote ctx ≤ rhs.denote ctx → p.denoteAsIntModule ctx < 0 := by
   simp [core_cert, Poly.denoteAsIntModule_eq_denote]; intro _ h₁; subst p; simp [Expr.denote_toPoly, Expr.denote]
   replace h₁ := LinearOrder.lt_of_not_le h₁
@@ -1202,7 +1202,7 @@ theorem not_le_norm {α} [CommRing α] [LinearOrder α] [Ring.IsOrdered α] (ctx
   simp [← sub_eq_add_neg, sub_self] at h₁
   assumption
 
-theorem not_lt_norm {α} [CommRing α] [LinearOrder α] [Ring.IsOrdered α] (ctx : Context α) (lhs rhs : Expr) (p : Poly)
+theorem not_lt_norm {α} [CommRing α] [LinearOrder α] [OrderedRing α] (ctx : Context α) (lhs rhs : Expr) (p : Poly)
     : core_cert rhs lhs p → ¬ lhs.denote ctx < rhs.denote ctx → p.denoteAsIntModule ctx ≤ 0 := by
   simp [core_cert, Poly.denoteAsIntModule_eq_denote]; intro _ h₁; subst p; simp [Expr.denote_toPoly, Expr.denote]
   replace h₁ := LinearOrder.le_of_not_lt h₁
@@ -1210,14 +1210,14 @@ theorem not_lt_norm {α} [CommRing α] [LinearOrder α] [Ring.IsOrdered α] (ctx
   simp [← sub_eq_add_neg, sub_self] at h₁
   assumption
 
-theorem not_le_norm' {α} [CommRing α] [Preorder α] [Ring.IsOrdered α] (ctx : Context α) (lhs rhs : Expr) (p : Poly)
+theorem not_le_norm' {α} [CommRing α] [Preorder α] [OrderedRing α] (ctx : Context α) (lhs rhs : Expr) (p : Poly)
     : core_cert lhs rhs p → ¬ lhs.denote ctx ≤ rhs.denote ctx → ¬ p.denoteAsIntModule ctx ≤ 0 := by
   simp [core_cert, Poly.denoteAsIntModule_eq_denote]; intro _ h₁; subst p; simp [Expr.denote_toPoly, Expr.denote]; intro h
   replace h := add_le_right (rhs.denote ctx) h
   rw [sub_eq_add_neg, add_left_comm, ← sub_eq_add_neg, sub_self] at h; simp [add_zero] at h
   contradiction
 
-theorem not_lt_norm' {α} [CommRing α] [Preorder α] [Ring.IsOrdered α] (ctx : Context α) (lhs rhs : Expr) (p : Poly)
+theorem not_lt_norm' {α} [CommRing α] [Preorder α] [OrderedRing α] (ctx : Context α) (lhs rhs : Expr) (p : Poly)
     : core_cert lhs rhs p → ¬ lhs.denote ctx < rhs.denote ctx → ¬ p.denoteAsIntModule ctx < 0 := by
   simp [core_cert, Poly.denoteAsIntModule_eq_denote]; intro _ h₁; subst p; simp [Expr.denote_toPoly, Expr.denote]; intro h
   replace h := add_lt_right (rhs.denote ctx) h

src/Init/GrindInstances/Nat.lean

@@ -14,30 +14,4 @@ namespace Lean.Grind
 instance : AddRightCancel Nat where
   add_right_cancel _ _ _ := Nat.add_right_cancel
 
-instance : CommSemiring Nat where
-  add := Nat.add
-  mul := Nat.mul
-  hPow := Nat.pow
-  add_assoc := Nat.add_assoc
-  add_comm := Nat.add_comm
-  add_zero := Nat.add_zero
-  mul_assoc := Nat.mul_assoc
-  mul_comm := Nat.mul_comm
-  mul_one := Nat.mul_one
-  one_mul := Nat.one_mul
-  zero_mul := Nat.zero_mul
-  mul_zero := Nat.mul_zero
-  left_distrib := Nat.left_distrib
-  right_distrib := Nat.right_distrib
-  pow_zero := Nat.pow_zero
-  pow_succ := Nat.pow_succ
-
-instance : NoNatZeroDivisors Nat where
-  no_nat_zero_divisors := by
-    intro k a b h₁ h₂
-    exact Nat.mul_left_cancel (Nat.zero_lt_of_ne_zero h₁) h₂
-
-instance : IsCharP Nat 0 where
-  ofNat_ext_iff := by intro; simp [OfNat.ofNat]
-
 end Lean.Grind

src/Init/GrindInstances/Ring.lean

@@ -6,6 +6,7 @@ Authors: Kim Morrison
 module
 
 prelude
+import Init.GrindInstances.Ring.Nat
 import Init.GrindInstances.Ring.Int
 import Init.GrindInstances.Ring.UInt
 import Init.GrindInstances.Ring.SInt

src/Init/GrindInstances/Ring/Nat.lean

@@ -0,0 +1,36 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+module
+
+prelude
+import Init.Grind.Ring.Basic
+import Init.Data.Int.Lemmas
+
+namespace Lean.Grind
+
+instance : CommSemiring Nat where
+  add_assoc := Nat.add_assoc
+  add_comm := Nat.add_comm
+  add_zero := Nat.add_zero
+  mul_assoc := Nat.mul_assoc
+  mul_comm := Nat.mul_comm
+  mul_one := Nat.mul_one
+  one_mul := Nat.one_mul
+  left_distrib := Nat.mul_add
+  right_distrib := Nat.add_mul
+  zero_mul := Nat.zero_mul
+  mul_zero := Nat.mul_zero
+  pow_zero _ := by rfl
+  pow_succ _ _ := by rfl
+  ofNat_succ _ := by rfl
+
+instance : IsCharP Nat 0 where
+  ofNat_ext_iff {x y} := by simp [OfNat.ofNat]
+
+instance : NoNatZeroDivisors Nat where
+  no_nat_zero_divisors _ _ _ h₁ h₂ := (Nat.mul_right_inj h₁).mp h₂
+
+end Lean.Grind

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

@@ -143,21 +143,21 @@ private def mkIntModPreThmPrefix (declName : Name) : ProofM Expr := do
 
 /--
 Returns the prefix of a theorem with name `declName` where the first five arguments are
-`{α} [IntModule α] [Preorder α] [IntModule.IsOrdered α] (ctx : Context α)`
+`{α} [IntModule α] [Preorder α] [OrderedAdd α] (ctx : Context α)`
 This is the most common theorem prefix at `Linarith.lean`
 -/
 private def mkIntModPreOrdThmPrefix (declName : Name) : ProofM Expr := do
   let s ← getStruct
-  return mkApp5 (mkConst declName [s.u]) s.type s.intModuleInst (← getPreorderInst) (← getIsOrdInst) (← getContext)
+  return mkApp5 (mkConst declName [s.u]) s.type s.intModuleInst (← getPreorderInst) (← getOrderedAddInst) (← getContext)
 
 /--
 Returns the prefix of a theorem with name `declName` where the first five arguments are
-`{α} [IntModule α] [LinearOrder α] [IntModule.IsOrdered α] (ctx : Context α)`
+`{α} [IntModule α] [LinearOrder α] [OrderedAdd α] (ctx : Context α)`
 This is the most common theorem prefix at `Linarith.lean`
 -/
 private def mkIntModLinOrdThmPrefix (declName : Name) : ProofM Expr := do
   let s ← getStruct
-  return mkApp5 (mkConst declName [s.u]) s.type s.intModuleInst (← getLinearOrderInst) (← getIsOrdInst) (← getContext)
+  return mkApp5 (mkConst declName [s.u]) s.type s.intModuleInst (← getLinearOrderInst) (← getOrderedAddInst) (← getContext)
 
 /--
 Returns the prefix of a theorem with name `declName` where the first three arguments are
@@ -169,19 +169,19 @@ private def mkCommRingThmPrefix (declName : Name) : ProofM Expr := do
 
 /--
 Returns the prefix of a theorem with name `declName` where the first five arguments are
-`{α} [CommRing α] [Preorder α] [Ring.IsOrdered α] (rctx : Context α)`
+`{α} [CommRing α] [Preorder α] [OrderedRing α] (rctx : Context α)`
 -/
 private def mkCommRingPreOrdThmPrefix (declName : Name) : ProofM Expr := do
   let s ← getStruct
-  return mkApp5 (mkConst declName [s.u]) s.type (← getCommRingInst) (← getPreorderInst) (← getRingIsOrdInst) (← getRingContext)
+  return mkApp5 (mkConst declName [s.u]) s.type (← getCommRingInst) (← getPreorderInst) (← getOrderedRingInst) (← getRingContext)
 
 /--
 Returns the prefix of a theorem with name `declName` where the first five arguments are
-`{α} [CommRing α] [LinearOrder α] [Ring.IsOrdered α] (rctx : Context α)`
+`{α} [CommRing α] [LinearOrder α] [OrderedRing α] (rctx : Context α)`
 -/
 private def mkCommRingLinOrdThmPrefix (declName : Name) : ProofM Expr := do
   let s ← getStruct
-  return mkApp5 (mkConst declName [s.u]) s.type (← getCommRingInst) (← getLinearOrderInst) (← getRingIsOrdInst) (← getRingContext)
+  return mkApp5 (mkConst declName [s.u]) s.type (← getCommRingInst) (← getLinearOrderInst) (← getOrderedRingInst) (← getRingContext)
 
 mutual
 partial def IneqCnstr.toExprProof (c' : IneqCnstr) : ProofM Expr := caching c' do
@@ -213,7 +213,7 @@ partial def IneqCnstr.toExprProof (c' : IneqCnstr) : ProofM Expr := caching c' d
       (← c₁.toExprProof) (← c₂.toExprProof)
   | .oneGtZero =>
     let s ← getStruct
-    let h := mkApp5 (mkConst ``Grind.Linarith.zero_lt_one [s.u]) s.type (← getRingInst) (← getPreorderInst) (← getRingIsOrdInst) (← getContext)
+    let h := mkApp5 (mkConst ``Grind.Linarith.zero_lt_one [s.u]) s.type (← getRingInst) (← getPreorderInst) (← getOrderedRingInst) (← getContext)
     return mkApp3 h (← mkPolyDecl c'.p) reflBoolTrue (← mkEqRefl (← getOne))
   | .ofEq a b la lb =>
     let h ← mkIntModPreOrdThmPrefix ``Grind.Linarith.le_of_eq

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

@@ -224,7 +224,7 @@ def processNewEqImpl (a b : Expr) : GoalM Unit := do
   if isSameExpr a b then return () -- TODO: check why this is needed
   let some structId ← inSameStruct? a b | return ()
   LinearM.run structId do
-    if (← isOrdered) then
+    if (← isOrderedAdd) then
       trace_goal[grind.linarith.assert] "{← mkEq a b}"
       if (← isCommRing) then
         processNewCommRingEq' a b

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

@@ -132,12 +132,12 @@ where
     ensureToFieldDefEq hmulInst intModuleInst ``Grind.IntModule.hmulInt
     ensureToFieldDefEq hmulNatInst intModuleInst ``Grind.IntModule.hmulNat
     let preorderInst? ← getInst? ``Grind.Preorder
-    let isOrdInst? ← if let some preorderInst := preorderInst? then
-      let isOrderedType := mkApp3 (mkConst ``Grind.IntModule.IsOrdered [u]) type preorderInst intModuleInst
+    let orderedAddInst? ← if let some preorderInst := preorderInst? then
+      let isOrderedType := mkApp3 (mkConst ``Grind.OrderedAdd [u]) type addInst preorderInst
       pure <| LOption.toOption (← trySynthInstance isOrderedType)
     else
       pure none
-    let preorderInst? := if isOrdInst?.isNone then none else preorderInst?
+    let preorderInst? := if orderedAddInst?.isNone then none else preorderInst?
     let partialInst? ← checkToFieldDefEq? preorderInst? (← getInst? ``Grind.PartialOrder) ``Grind.PartialOrder.toPreorder
     let linearInst? ← checkToFieldDefEq? partialInst? (← getInst? ``Grind.LinearOrder) ``Grind.LinearOrder.toPartialOrder
     let (leFn?, ltFn?) ← if let some preorderInst := preorderInst? then
@@ -172,15 +172,15 @@ where
       return some one
     let one? ← getOne?
     let commRingInst? ← getInst? ``Grind.CommRing
-    let getRingIsOrdInst? : GoalM (Option Expr) := do
+    let getOrderedRingInst? : GoalM (Option Expr) := do
       let some ringInst := ringInst? | return none
       let some preorderInst := preorderInst? | return none
-      let isOrdType := mkApp3 (mkConst ``Grind.Ring.IsOrdered [u]) type ringInst preorderInst
+      let isOrdType := mkApp3 (mkConst ``Grind.OrderedRing [u]) type ringInst preorderInst
       let .some inst ← trySynthInstance isOrdType
-        | reportIssue! "type is an ordered `IntModule` and a `Ring`, but is not an ordered ring, failed to synthesize{indentExpr isOrdType}"
+        | reportIssue! "type has a `Preorder` and is a `Ring`, but is not an ordered ring, failed to synthesize{indentExpr isOrdType}"
           return none
       return some inst
-    let ringIsOrdInst? ← getRingIsOrdInst?
+    let orderedRingInst? ← getOrderedRingInst?
     let charInst? ← if let some semiringInst := semiringInst? then getIsCharInst? u type semiringInst else pure none
     let getNoNatZeroDivInst? : GoalM (Option Expr) := do
       let hmulNat := mkApp3 (mkConst ``HMul [0, u, u]) Nat.mkType type type
@@ -190,14 +190,14 @@ where
     let noNatDivInst? ← getNoNatZeroDivInst?
     let id := (← get').structs.size
     let struct : Struct := {
-      id, type, u, intModuleInst, preorderInst?, isOrdInst?, partialInst?, linearInst?, noNatDivInst?
+      id, type, u, intModuleInst, preorderInst?, orderedAddInst?, partialInst?, linearInst?, noNatDivInst?
       leFn?, ltFn?, addFn, subFn, negFn, hmulFn, hmulNatFn, hsmulFn?, hsmulNatFn?, zero, one?
-      ringInst?, commRingInst?, ringIsOrdInst?, charInst?, ringId?, fieldInst?, ofNatZero
+      ringInst?, commRingInst?, orderedRingInst?, charInst?, ringId?, fieldInst?, ofNatZero
     }
     modify' fun s => { s with structs := s.structs.push struct }
     if let some one := one? then
       if ringInst?.isSome then LinearM.run id do
-        if ringIsOrdInst?.isSome then
+        if orderedRingInst?.isSome then
           -- Create `1` variable, and assert strict lower bound `0 < 1` and `0 ≠ 1`
           let x ← mkVar one (mark := false)
           addZeroLtOne x

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

@@ -82,7 +82,7 @@ abbrev VarSet := RBTree Var compare
 /--
 State for each algebraic structure by this module.
 Each type must at least implement the instance `IntModule`.
-For being able to process inequalities, it must at least implement `Preorder`, and `IntModule.IsOrdered`
+For being able to process inequalities, it must at least implement `Preorder`, and `OrderedAdd`
 -/
 structure Struct where
   id               : Nat
@@ -95,8 +95,8 @@ structure Struct where
   intModuleInst    : Expr
   /-- `Preorder` instance if available -/
   preorderInst?    : Option Expr
-  /-- `IntModule.IsOrdered` instance with `Preorder` if available -/
-  isOrdInst?       : Option Expr
+  /-- `OrderedAdd` instance with `Preorder` if available -/
+  orderedAddInst?       : Option Expr
   /-- `PartialOrder` instance if available -/
   partialInst?     : Option Expr
   /-- `LinearOrder` instance if available -/
@@ -107,8 +107,8 @@ structure Struct where
   ringInst?        : Option Expr
   /-- `CommRing` instance -/
   commRingInst?    : Option Expr
-  /-- `Ring.IsOrdered` instance with `Preorder` -/
-  ringIsOrdInst?   : Option Expr
+  /-- `OrderedRing` instance with `Preorder` -/
+  orderedRingInst?   : Option Expr
   /-- `Field` instance -/
   fieldInst?       : Option Expr
   /-- `IsCharP` instance for `type` if available. -/

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

@@ -87,7 +87,7 @@ def isCommRing : LinearM Bool :=
   return (← getStruct).ringId?.isSome
 
 def isOrderedCommRing : LinearM Bool := do
-  return (← isCommRing) && (← getStruct).ringIsOrdInst?.isSome
+  return (← isCommRing) && (← getStruct).orderedRingInst?.isSome
 
 def isLinearOrder : LinearM Bool :=
   return (← getStruct).linearInst?.isSome
@@ -120,13 +120,13 @@ def getPreorderInst : LinearM Expr := do
     | throwError "`grind linarith` internal error, structure is not a preorder"
   return inst
 
-def getIsOrdInst : LinearM Expr := do
-  let some inst := (← getStruct).isOrdInst?
+def getOrderedAddInst : LinearM Expr := do
+  let some inst := (← getStruct).orderedAddInst?
     | throwError "`grind linarith` internal error, structure is not an ordered module"
   return inst
 
-def isOrdered : LinearM Bool :=
-  return (← getStruct).isOrdInst?.isSome
+def isOrderedAdd : LinearM Bool :=
+  return (← getStruct).orderedAddInst?.isSome
 
 def getLtFn [Monad m] [MonadError m] [MonadGetStruct m] : m Expr := do
   let some lt := (← getStruct).ltFn?
@@ -153,8 +153,8 @@ def getCommRingInst : LinearM Expr := do
     | throwError "`grind linarith` internal error, structure is not a commutative ring"
   return inst
 
-def getRingIsOrdInst : LinearM Expr := do
-  let some inst := (← getStruct).ringIsOrdInst?
+def getOrderedRingInst : LinearM Expr := do
+  let some inst := (← getStruct).orderedRingInst?
     | throwError "`grind linarith` internal error, structure is not an ordered ring"
   return inst
 

tests/lean/grind/algebra/ordered_modules.lean

@@ -1,16 +1,15 @@
 open Lean.Grind
 
-variable (R : Type u) [IntModule R] [NoNatZeroDivisors R] [Preorder R] [IntModule.IsOrdered R]
+-- Many of these should work with less than `LinearOrder`.
+variable (R : Type u) [IntModule R] [NoNatZeroDivisors R] [LinearOrder R] [OrderedAdd R]
 
 example (a b c : R) (h : a < b) : a + c < b + c := by grind
 example (a b c : R) (h : a < b) : c + a < c + b := by grind
 example (a b : R) (h : a < b) : -b < -a := by grind
-example (a b : R) (h : a < b) : -a < -b := by grind
 
 example (a b c : R) (h : a ≤ b) : a + c ≤ b + c := by grind
 example (a b c : R) (h : a ≤ b) : c + a ≤ c + b := by grind
 example (a b : R) (h : a ≤ b) : -b ≤ -a := by grind
-example (a b : R) (h : a ≤ b) : -a ≤ -b := by grind
 
 example (a : R) (h : 0 < a) : 0 ≤ a := by grind
 example (a : R) (h : 0 < a) : -2 * a < 0 := by grind

tests/lean/grind/experiments/nat_semiring.lean

@@ -20,25 +20,25 @@ example {a b c d : Int} (h : a = b + c * d) (hb : 0 ≤ b) (hc : 0 ≤ c) (w : 1
 
 open Lean Grind
 
-example {α : Type} [Lean.Grind.IntModule α] [Lean.Grind.Preorder α] [Lean.Grind.IntModule.IsOrdered α] {a b c : α} {d : Int}
+example {α : Type} [Lean.Grind.IntModule α] [Lean.Grind.Preorder α] [Lean.Grind.OrderedAdd α] {a b c : α} {d : Int}
     (wb : 0 ≤ b) (wc : 0 ≤ c)
     (h : a = b + d * c) (w : 1 ≤ d) : a ≥ c := by
   subst h
   conv => rhs; rw [← IntModule.zero_add c]
-  apply IntModule.IsOrdered.add_le_add
+  apply OrderedAdd.add_le_add
   · exact wb
-  · have := IntModule.IsOrdered.hmul_le_hmul_of_le_of_le_of_nonneg_of_nonneg w (Preorder.le_refl c) (by decide) wc
+  · have := OrderedAdd.hmul_int_le_hmul_int_of_le_of_le_of_nonneg_of_nonneg w (Preorder.le_refl c) (by decide) wc
     rwa [IntModule.one_hmul] at this
 
 -- We can prove this directly in an ordered NatModule, from the axioms. (But shouldn't, see below.)
-example {α : Type} [Lean.Grind.NatModule α] [Lean.Grind.Preorder α] [Lean.Grind.NatModule.IsOrdered α] {a b c : α} {d : Nat}
+example {α : Type} [Lean.Grind.NatModule α] [Lean.Grind.Preorder α] [Lean.Grind.OrderedAdd α] {a b c : α} {d : Nat}
     (wb : 0 ≤ b) (wc : 0 ≤ c)
     (h : a = b + d * c) (w : 1 ≤ d) : a ≥ c := by
   subst h
   conv => rhs; rw [← NatModule.zero_add c]
-  apply NatModule.IsOrdered.add_le_add
+  apply OrderedAdd.add_le_add
   · exact wb
-  · have := NatModule.IsOrdered.hmul_le_hmul_of_le_of_le_of_nonneg w (Preorder.le_refl c) wc
+  · have := OrderedAdd.hmul_le_hmul_of_le_of_le_of_nonneg w (Preorder.le_refl c) wc
     rwa [NatModule.one_hmul] at this
 
 -- The correct proof is to embed a NatModule in its IntModule envelope.

tests/lean/run/grind_ematch_gen_pattern.lean

@@ -53,8 +53,6 @@ trace: [grind.ematch.instance] pbind_some': ∀ (h : b = some a), (b.pbind fun a
       (b.pbind fun a h => some (a + f b ⋯)) = some (a + 4 * f b ⋯ + f b ⋯)
 [grind.ematch.instance] pbind_some': ∀ (h_3 : b = some (a + 5 * f b ⋯)),
       (b.pbind fun a h => some (a + f b ⋯)) = some (a + 5 * f b ⋯ + f b ⋯)
-[grind.ematch.instance] pbind_some': ∀ (h_3 : b = some (2 * a + f b ⋯)),
-      (b.pbind fun a h => some (a + f b ⋯)) = some (2 * a + f b ⋯ + f b ⋯)
 [grind.ematch.instance] pbind_some': ∀ (h_3 : b = some (a + 6 * f b ⋯)),
       (b.pbind fun a h => some (a + f b ⋯)) = some (a + 6 * f b ⋯ + f b ⋯)
 [grind.ematch.instance] pbind_some': ∀ (h_3 : b = some (a + 7 * f b ⋯)),

tests/lean/run/grind_field_div.lean

@@ -67,7 +67,7 @@ example [Field α] {sqrtTwo a b c : α} :
 -- characteristic zero.
 #guard_msgs (trace) in
 set_option trace.grind.split true in
-example [Field α] [LinearOrder α] [Ring.IsOrdered α] (x y z : α)
+example [Field α] [LinearOrder α] [OrderedRing α] (x y z : α)
     : x > 0 → y > 0 → z > 0 → x * y * z ≥ 1 →
       (x ^ 2 - y * z) / (x ^ 2 + y ^ 2 + z ^ 2) + (y ^ 2 - z * x) / (y ^ 2 + z ^ 2 + x ^ 2) +
         (z ^ 2 - x * y) / (z ^ 2 + x ^ 2 + y ^ 2) =

tests/lean/run/grind_linarith_1.lean

@@ -1,152 +1,152 @@
 open Lean.Grind
 set_option grind.debug true
 
-example [IntModule α] [Preorder α] [IntModule.IsOrdered α] (a b : α)
+example [IntModule α] [Preorder α] [OrderedAdd α] (a b : α)
     : (2:Int)*a + b < b + a + a → False := by
   grind
 
-example [IntModule α] [LinearOrder α] [IntModule.IsOrdered α] (a b : α)
+example [IntModule α] [LinearOrder α] [OrderedAdd α] (a b : α)
     : (2:Int)*a + b < b + a + a → False := by
   grind
 
-example [IntModule α] [Preorder α] [IntModule.IsOrdered α] (a b : α)
+example [IntModule α] [Preorder α] [OrderedAdd α] (a b : α)
     : (2:Int)*a + b < b + a + a → False := by
   fail_if_success grind -linarith
   grind
 
-example [IntModule α] [LinearOrder α] [IntModule.IsOrdered α] (a b : α)
+example [IntModule α] [LinearOrder α] [OrderedAdd α] (a b : α)
     : (2:Int)*a + b ≥ b + a + a := by
   grind
 
 #guard_msgs (drop error) in
-example [IntModule α] [Preorder α] [IntModule.IsOrdered α] (a b : α)
+example [IntModule α] [Preorder α] [OrderedAdd α] (a b : α)
     : (2:Int)*a + b ≥ b + a + a := by
   fail_if_success grind
 
-example [CommRing α] [Preorder α] [Ring.IsOrdered α] (a b : α)
+example [CommRing α] [Preorder α] [OrderedRing α] (a b : α)
     : 2*a + b < b + a + a → False := by
   grind
 
-example [CommRing α] [Preorder α] [Ring.IsOrdered α] (a b : α)
+example [CommRing α] [Preorder α] [OrderedRing α] (a b : α)
     : 2 + 2*a + b + 1 < b + a + a + 3 → False := by
   grind
 
-example [CommRing α] [LinearOrder α] [Ring.IsOrdered α] (a b : α)
+example [CommRing α] [LinearOrder α] [OrderedRing α] (a b : α)
     : 2 + 2*a + b + 1 <= b + a + a + 3 := by
   grind
 
-example [IntModule α] [Preorder α] [IntModule.IsOrdered α] (a b c : α)
+example [IntModule α] [Preorder α] [OrderedAdd α] (a b c : α)
     : a < b → b < c → c < a → False := by
   grind
 
-example [IntModule α] [LinearOrder α] [IntModule.IsOrdered α] (a b c : α)
+example [IntModule α] [LinearOrder α] [OrderedAdd α] (a b c : α)
     : a < b → b < c → a < c := by
   grind
 
-example [IntModule α] [LinearOrder α] [IntModule.IsOrdered α] (a b c : α)
+example [IntModule α] [LinearOrder α] [OrderedAdd α] (a b c : α)
     : a < b → b ≤ c → a < c := by
   grind
 
-example [IntModule α] [LinearOrder α] [IntModule.IsOrdered α] (a b c : α)
+example [IntModule α] [LinearOrder α] [OrderedAdd α] (a b c : α)
     : a ≤ b → b ≤ c → a ≤ c := by
   grind
 
-example [IntModule α] [LinearOrder α] [IntModule.IsOrdered α] (a b c d : α)
+example [IntModule α] [LinearOrder α] [OrderedAdd α] (a b c d : α)
     : a < b → b < c + d → a - d < c := by
   grind
 
-example [CommRing α] [LinearOrder α] [Ring.IsOrdered α] (a b c d : α)
+example [CommRing α] [LinearOrder α] [OrderedRing α] (a b c d : α)
     : a < b → b < c + d → a - d < c := by
   grind
 
-example [CommRing α] [Preorder α] [Ring.IsOrdered α] (a b c : α)
+example [CommRing α] [Preorder α] [OrderedRing α] (a b c : α)
     : a < b → 2*b < c → c < 2*a → False := by
   grind
 
 -- Test misconfigured instances
 /--
-trace: [grind.issues] type is an ordered `IntModule` and a `Ring`, but is not an ordered ring, failed to synthesize
-      Ring.IsOrdered α
+trace: [grind.issues] type has a `Preorder` and is a `Ring`, but is not an ordered ring, failed to synthesize
+      OrderedRing α
 -/
 #guard_msgs (drop error, trace) in
 set_option trace.grind.issues true in
-example [CommRing α] [Preorder α] [IntModule.IsOrdered α] (a b c : α)
+example [CommRing α] [Preorder α] [OrderedAdd α] (a b c : α)
     : a < b → b + b < c → c < a → False := by
   grind
 
-example [CommRing α] [Preorder α] [Ring.IsOrdered α] (a b : α)
+example [CommRing α] [Preorder α] [OrderedRing α] (a b : α)
     : a < 2 → b < a → b > 5 → False := by
   grind
 
-example [CommRing α] [Preorder α] [Ring.IsOrdered α] (a b : α)
+example [CommRing α] [Preorder α] [OrderedRing α] (a b : α)
     : a < One.one + 4 → b < a → b ≥ 5 → False := by
   grind
 
-example [CommRing α] [Preorder α] [Ring.IsOrdered α] (a b : α)
+example [CommRing α] [Preorder α] [OrderedRing α] (a b : α)
     : a < One.one + 5 → b < a → b ≥ 5 → False := by
   fail_if_success grind
   sorry
 
-example [IntModule α] [Preorder α] [IntModule.IsOrdered α] (a b c d : α)
+example [IntModule α] [Preorder α] [OrderedAdd α] (a b c d : α)
     : a < c → b = a + d → b - d > c → False := by
   grind
 
-example [IntModule α] [Preorder α] [IntModule.IsOrdered α] (a b c d : α)
+example [IntModule α] [Preorder α] [OrderedAdd α] (a b c d : α)
     : a + d < c → b = a + (2:Int)*d → b - d > c → False := by
   grind
 
-example [CommRing α] [Preorder α] [Ring.IsOrdered α] (a b : α)
+example [CommRing α] [Preorder α] [OrderedRing α] (a b : α)
     : a < 2 → b = a → b > 5 → False := by
   grind
 
-example [CommRing α] [Preorder α] [Ring.IsOrdered α] (a b : α)
+example [CommRing α] [Preorder α] [OrderedRing α] (a b : α)
     : a < 2 → a = b + b → b > 5 → False := by
   grind
 
-example [CommRing α] [LinearOrder α] [Ring.IsOrdered α] (a b : α)
+example [CommRing α] [LinearOrder α] [OrderedRing α] (a b : α)
     : a < 2 → a = b + b → b < 1 := by
   grind
 
-example [CommRing α] [LinearOrder α] [Ring.IsOrdered α] (a b : α)
+example [CommRing α] [LinearOrder α] [OrderedRing α] (a b : α)
     : a ≤ 2 → a + b = 3*b → b ≤ 1 := by
   grind
 
-example [CommRing α] [LinearOrder α] [Ring.IsOrdered α] (a b c d e : α) :
+example [CommRing α] [LinearOrder α] [OrderedRing α] (a b c d e : α) :
     2*a + b ≥ 1 → b ≥ 0 → c ≥ 0 → d ≥ 0 → e ≥ 0
     → a ≥ 3*c → c ≥ 6*e → d - e*5 ≥ 0
     → a + b + 3*c + d + 2*e ≥ 0 := by
   grind
 
-example [CommRing α] [Preorder α] [Ring.IsOrdered α] (a b c d e : α) :
+example [CommRing α] [Preorder α] [OrderedRing α] (a b c d e : α) :
     2*a + b ≥ 1 → b ≥ 0 → c ≥ 0 → d ≥ 0 → e ≥ 0
     → a ≥ 3*c → c ≥ 6*e → d - e*5 ≥ 0
     → a + b + 3*c + d + 2*e < 0 → False := by
   grind
 
-example [CommRing α] [Preorder α] [Ring.IsOrdered α] (a b : α)
+example [CommRing α] [Preorder α] [OrderedRing α] (a b : α)
     : a = 0 → b = 1 → a + b > 2 → False := by
   grind
 
-example [CommRing α] [LinearOrder α] [Ring.IsOrdered α] (a b c : α)
+example [CommRing α] [LinearOrder α] [OrderedRing α] (a b c : α)
     : a = 0 → a + b > 2 → b = c → 1 = c → False := by
   grind
 
-example [CommRing α] [LinearOrder α] [Ring.IsOrdered α] (a b : α)
+example [CommRing α] [LinearOrder α] [OrderedRing α] (a b : α)
     : a = 0 → b = 1 → a + b ≤ 2 := by
   grind
 
-example [CommRing α] [LinearOrder α] [Ring.IsOrdered α] (a b : α)
+example [CommRing α] [LinearOrder α] [OrderedRing α] (a b : α)
     : a*b + b*a > 1 → a*b > 0 := by
   grind
 
-example [CommRing α] [LinearOrder α] [Ring.IsOrdered α] (a b c : α)
+example [CommRing α] [LinearOrder α] [OrderedRing α] (a b c : α)
     : a*b + c > 1 → c = b*a → a*b > 0 := by
   grind
 
 -- It must not internalize subterms `b + c + d` and `b + b + d`
 #guard_msgs (trace) in
 set_option trace.grind.linarith.internalize true
-example [CommRing α] [LinearOrder α] [Ring.IsOrdered α] (a b c d : α)
+example [CommRing α] [LinearOrder α] [OrderedRing α] (a b c d : α)
     : a < b + c + d → c = b → a < b + b + d := by
   grind
 

tests/lean/run/grind_linarith_2.lean

@@ -1,7 +1,7 @@
 open Lean Grind
 set_option grind.debug true
 
-example [IntModule α] [Preorder α] [IntModule.IsOrdered α] (a b : α)
+example [IntModule α] [Preorder α] [OrderedAdd α] (a b : α)
     : a + b = b + a  := by
   grind
 
@@ -21,7 +21,7 @@ trace: [grind.debug.proof] Classical.byContradiction fun h =>
 #guard_msgs in
 open Linarith in
 set_option trace.grind.debug.proof true in
-example [CommRing α] [Preorder α] [Ring.IsOrdered α] (a b : α)
+example [CommRing α] [Preorder α] [OrderedRing α] (a b : α)
     : a + b = b + a  := by
   grind -ring
 
@@ -36,33 +36,33 @@ trace: [grind.debug.linarith.search.assign] One.one := 1
 -/
 #guard_msgs (drop error, trace) in
 set_option trace.grind.debug.linarith.search.assign true in
-example [CommRing α] [LinearOrder α] [Ring.IsOrdered α] (a b c d : α)
+example [CommRing α] [LinearOrder α] [OrderedRing α] (a b c d : α)
     : b ≥ 0 → c > b → d > b → a ≠ b + c → a > b + c → a < b + d →  False := by
   grind
 
-example [CommRing α] [LinearOrder α] [Ring.IsOrdered α] (a b c d : α)
+example [CommRing α] [LinearOrder α] [OrderedRing α] (a b c d : α)
     : a ≤ b → a ≥ c + d → d = 0 → b = c → a = b := by
   grind
 
-example [IntModule α] [LinearOrder α] [IntModule.IsOrdered α] (a b c d : α)
+example [IntModule α] [LinearOrder α] [OrderedAdd α] (a b c d : α)
     : a ≤ b → a ≥ c + d → d ≤ 0 → d ≥ 0 → b = c → a = b := by
   grind
 
 open Linarith RArray
 set_option trace.grind.debug.proof true in
-example [IntModule α] [LinearOrder α] [IntModule.IsOrdered α] (a b c d : α)
+example [IntModule α] [LinearOrder α] [OrderedAdd α] (a b c d : α)
     : a ≤ b → a - c ≥ 0 + d → d ≤ 0 → d ≥ 0 → b = c → a ≠ b → False := by
   grind
 
-example [CommRing α] [LinearOrder α] [Ring.IsOrdered α] (a b c : α)
+example [CommRing α] [LinearOrder α] [OrderedRing α] (a b c : α)
     : a + 2*b = 0 → c + b = -b → a = c := by
   grind
 
-example [CommRing α] [LinearOrder α] [Ring.IsOrdered α] (a b c : α)
+example [CommRing α] [LinearOrder α] [OrderedRing α] (a b c : α)
     : a + 2*b = 0 → a = c → c + b = -b := by
   grind
 
-example [CommRing α] [LinearOrder α] [Ring.IsOrdered α] (a b c : α)
+example [CommRing α] [LinearOrder α] [OrderedRing α] (a b c : α)
     : c = a → a + b ≤ 3 → 3 ≤ b + c → a + b = 3 := by
   grind
 
@@ -74,7 +74,7 @@ trace: [grind.linarith.model] a := 7/2
 -/
 #guard_msgs (drop error, trace) in
 set_option trace.grind.linarith.model true in
-example [CommRing α] [LinearOrder α] [Ring.IsOrdered α] (a b c d : α)
+example [CommRing α] [LinearOrder α] [OrderedRing α] (a b c d : α)
     : b ≥ 0 → c > b → d > b → a ≠ b + c → a > b + c → a < b + d →  False := by
   grind
 
@@ -86,24 +86,24 @@ trace: [grind.linarith.model] a := 0
 -/
 #guard_msgs (drop error, trace) in
 set_option trace.grind.linarith.model true in
-example [IntModule α] [LinearOrder α] [IntModule.IsOrdered α] (a b c d : α)
+example [IntModule α] [LinearOrder α] [OrderedAdd α] (a b c d : α)
     : a ≤ b → a - c ≥ 0 + d → d ≤ 0 → b = c → a ≠ b → False := by
   grind
 
 /-- trace: [grind.split] x = 0, generation: 0 -/
 #guard_msgs (trace) in
 set_option trace.grind.split true in
-example [IntModule α] [LinearOrder α] [IntModule.IsOrdered α] (f : α → α) (x : α)
+example [IntModule α] [LinearOrder α] [OrderedAdd α] (f : α → α) (x : α)
     : Zero.zero ≤ x → x ≤ 0 → f x = a → f 0 = a := by
   grind
 
 -- should not split on `x = 0` since `α` is not a linear order
 #guard_msgs (drop error, trace) in
 set_option trace.grind.split true in
-example [IntModule α] [Preorder α] [IntModule.IsOrdered α] (f : α → α) (x : α)
+example [IntModule α] [Preorder α] [OrderedAdd α] (f : α → α) (x : α)
     : Zero.zero ≤ x → x ≤ 0 → f x = a → f 0 = a := by
   grind
 
-example [CommRing α] [LinearOrder α] [Ring.IsOrdered α] (f : α → α → α) (x y z : α)
+example [CommRing α] [LinearOrder α] [OrderedRing α] (f : α → α → α) (x y z : α)
     : z ≤ x → x ≤ 1 → z = 1 → f x y = 2 → f 1 y = 2 := by
   grind

tests/lean/run/grind_ord_module.lean

@@ -1,6 +1,6 @@
 open Lean.Grind
 
-variable (R : Type u) [IntModule R] [LinearOrder R] [IntModule.IsOrdered R]
+variable (R : Type u) [IntModule R] [LinearOrder R] [OrderedAdd R]
 
 example (a b c : R) (h : a < b) : a + c < b + c := by grind
 example (a b c : R) (h : a < b) : c + a < c + b := by grind

tests/lean/run/grind_preord_module.lean

@@ -1,7 +1,7 @@
 open Lean.Grind
 
 -- `grind linarith` currently does not support negation of linear constraints.
-variable (R : Type u) [IntModule R] [Preorder R] [IntModule.IsOrdered R]
+variable (R : Type u) [IntModule R] [Preorder R] [OrderedAdd R]
 
 example (a b : R) (_ : a < b) (_ : b < a) : False := by grind
 example (a b : R) (_ : a < b ∧ b < a) : False := by grind

tests/lean/run/grind_ring_1.lean

@@ -91,6 +91,6 @@ trace: [grind.ring.assert.basis] a ^ 2 * b + -1 = 0
 -/
 #guard_msgs (drop error, trace) in
 set_option trace.grind.ring.assert.basis true in
-example [CommRing α] [Preorder α] [Ring.IsOrdered α] (a b c : α)
+example [CommRing α] [Preorder α] [OrderedRing α] (a b c : α)
     : a^2*b = 1 → a*b^2 = b → False := by
    grind