ordered rings

src/Init/Grind.lean

@@ -16,4 +16,5 @@ import Init.Grind.Offset
 import Init.Grind.PP
 import Init.Grind.CommRing
 import Init.Grind.Module
+import Init.Grind.Ordered
 import Init.Grind.Ext

src/Init/Grind/CommRing/Basic.lean

@@ -104,6 +104,12 @@ theorem ofNat_mul (a b : Nat) : OfNat.ofNat (α := α) (a * b) = OfNat.ofNat a *
 theorem natCast_mul (a b : Nat) : ((a * b : Nat) : α) = ((a : α) * (b : α)) := by
   rw [← ofNat_eq_natCast, ofNat_mul, ofNat_eq_natCast, ofNat_eq_natCast]
 
+theorem pow_one (a : α) : a ^ 1 = a := by
+  rw [pow_succ, pow_zero, one_mul]
+
+theorem pow_two (a : α) : a ^ 2 = a * a := by
+  rw [pow_succ, pow_one]
+
 theorem pow_add (a : α) (k₁ k₂ : Nat) : a ^ (k₁ + k₂) = a^k₁ * a^k₂ := by
   induction k₂
   next => simp [pow_zero, mul_one]
@@ -274,7 +280,6 @@ instance : IntModule α where
   hmul_zero := by simp [mul_zero]
   hmul_add := by simp [left_distrib]
   mul_hmul := by simp [intCast_mul, mul_assoc]
-  neg_hmul := by simp [intCast_neg, neg_mul]
   neg_add_cancel := by simp [neg_add_cancel]
   sub_eq_add_neg := by simp [sub_eq_add_neg]
 

src/Init/Grind/Module.lean

@@ -7,4 +7,3 @@ module
 
 prelude
 import Init.Grind.Module.Basic
-import Init.Grind.Module.Int

src/Init/Grind/Module/Basic.lean

@@ -32,16 +32,17 @@ class IntModule (M : Type u) extends Zero M, Add M, Neg M, Sub M, HMul Int M M w
   zero_hmul : ∀ a : M, (0 : Int) * a = 0
   one_hmul : ∀ a : M, (1 : Int) * a = a
   add_hmul : ∀ n m : Int, ∀ a : M, (n + m) * a = n * a + m * a
-  neg_hmul : ∀ n : Int, ∀ a : M, (-n) * a = - (n * a)
   hmul_zero : ∀ n : Int, n * (0 : M) = 0
   hmul_add : ∀ n : Int, ∀ a b : M, n * (a + b) = n * a + n * b
   mul_hmul : ∀ n m : Int, ∀ a : M, (n * m) * a = n * (m * a)
   neg_add_cancel : ∀ a : M, -a + a = 0
   sub_eq_add_neg : ∀ a b : M, a - b = a + -b
 
+namespace IntModule
+
 attribute [instance 100] IntModule.toZero IntModule.toAdd IntModule.toNeg IntModule.toSub IntModule.toHMul
 
-instance IntModule.toNatModule (M : Type u) [i : IntModule M] : NatModule M :=
+instance toNatModule (M : Type u) [i : IntModule M] : NatModule M :=
   { i with
     hMul a x := (a : Int) * x
     hmul_zero := by simp [IntModule.hmul_zero]
@@ -49,22 +50,58 @@ instance IntModule.toNatModule (M : Type u) [i : IntModule M] : NatModule M :=
     hmul_add := by simp [IntModule.hmul_add]
     mul_hmul := by simp [IntModule.mul_hmul] }
 
-/-- A preorder is a reflexive, transitive relation `≤` with `a < b` defined in the obvious way. -/
-class Preorder (α : Type u) extends LE α, LT α where
-  le_refl : ∀ a : α, a ≤ a
-  le_trans : ∀ a b c : α, a ≤ b → b ≤ c → a ≤ c
-  lt := fun a b => a ≤ b ∧ ¬b ≤ a
-  lt_iff_le_not_le : ∀ a b : α, a < b ↔ a ≤ b ∧ ¬b ≤ a := by intros; rfl
+variable {M : Type u} [IntModule M]
 
-class IntModule.IsOrdered (M : Type u) [Preorder M] [IntModule M] where
-  neg_le_iff : ∀ a b : M, -a ≤ b ↔ -b ≤ a
-  neg_lt_iff : ∀ a b : M, -a < b ↔ -b < a
-  add_lt_left : ∀ a b c : M, a < b → a + c < b + c
-  add_lt_right : ∀ a b c : M, a < b → c + a < c + b
-  hmul_pos : ∀ (k : Int) (a : M), 0 < a → (0 < k ↔ 0 < k * a)
-  hmul_neg : ∀ (k : Int) (a : M), a < 0 → (0 < k ↔ k * a < 0)
-  hmul_nonneg : ∀ (k : Int) (a : M), 0 ≤ a → 0 ≤ k → 0 ≤ k * a
-  hmul_nonpos : ∀ (k : Int) (a : M), a ≤ 0 → 0 ≤ k → k * a ≤ 0
+theorem add_neg_cancel (a : M) : a + -a = 0 := by
+  rw [add_comm, neg_add_cancel]
+
+theorem add_left_inj {a b : M} (c : M) : a + c = b + c ↔ a = b :=
+  ⟨fun h => by simpa [add_assoc, add_neg_cancel, add_zero] using (congrArg (· + -c) h),
+   fun g => congrArg (· + c) g⟩
+
+theorem add_right_inj (a b c : M) : a + b = a + c ↔ b = c := by
+  rw [add_comm a b, add_comm a c, add_left_inj]
+
+theorem neg_zero : (-0 : M) = 0 := by
+  rw [← add_left_inj 0, neg_add_cancel, add_zero]
+
+theorem neg_neg (a : M) : -(-a) = a := by
+  rw [← add_left_inj (-a), neg_add_cancel, add_neg_cancel]
+
+theorem neg_eq_zero (a : M) : -a = 0 ↔ a = 0 :=
+  ⟨fun h => by
+    replace h := congrArg (-·) h
+    simpa [neg_neg, neg_zero] using h,
+   fun h => by rw [h, neg_zero]⟩
+
+theorem neg_add (a b : M) : -(a + b) = -a + -b := by
+  rw [← add_left_inj (a + b), neg_add_cancel, add_assoc (-a), add_comm a b, ← add_assoc (-b),
+    neg_add_cancel, zero_add, neg_add_cancel]
+
+theorem neg_sub (a b : M) : -(a - b) = b - a := by
+  rw [sub_eq_add_neg, neg_add, neg_neg, sub_eq_add_neg, add_comm]
+
+theorem sub_self (a : M) : a - a = 0 := by
+  rw [sub_eq_add_neg, add_neg_cancel]
+
+theorem sub_eq_iff {a b c : M} : a - b = c ↔ a = c + b := by
+  rw [sub_eq_add_neg]
+  constructor
+  next => intro; subst c; rw [add_assoc, neg_add_cancel, add_zero]
+  next => intro; subst a; rw [add_assoc, add_comm b, neg_add_cancel, add_zero]
+
+theorem sub_eq_zero_iff {a b : M} : a - b = 0 ↔ a = b := by
+  simp [sub_eq_iff, zero_add]
+
+theorem neg_hmul (n : Int) (a : M) : (-n) * a = - (n * a) := by
+  apply (add_left_inj (n * a)).mp
+  rw [← add_hmul, Int.add_left_neg, zero_hmul, neg_add_cancel]
+
+theorem hmul_neg (n : Int) (a : M) : n * (-a) = - (n * a) := by
+  apply (add_left_inj (n * a)).mp
+  rw [← hmul_add, neg_add_cancel, neg_add_cancel, hmul_zero]
+
+end IntModule
 
 /--
 Special case of Mathlib's `NoZeroSMulDivisors Nat α`.

src/Init/Grind/Ordered.lean

@@ -0,0 +1,12 @@
+/-
+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.Ordered.PartialOrder
+import Init.Grind.Ordered.Module
+import Init.Grind.Ordered.Ring
+import Init.Grind.Ordered.Int

src/Init/Grind/Ordered/Int.lean

@@ -6,7 +6,7 @@ Authors: Kim Morrison
 module
 
 prelude
-import Init.Grind.Module.Basic
+import Init.Grind.Ordered.Ring
 import Init.Grind.CommRing.Int
 import Init.Omega
 
@@ -18,17 +18,18 @@ namespace Lean.Grind
 
 instance : Preorder Int where
   le_refl := Int.le_refl
-  le_trans _ _ _ := Int.le_trans
+  le_trans := Int.le_trans
   lt_iff_le_not_le := by omega
 
 instance : IntModule.IsOrdered Int where
   neg_le_iff := by omega
-  neg_lt_iff := by omega
-  add_lt_left := by omega
-  add_lt_right := by omega
+  add_le_left := by omega
   hmul_pos k a ha := ⟨fun hk => Int.mul_pos hk ha, fun h => Int.pos_of_mul_pos_left h ha⟩
-  hmul_neg k a ha := ⟨fun hk => Int.mul_neg_of_pos_of_neg hk ha, fun h => Int.pos_of_mul_neg_left h ha⟩
-  hmul_nonpos k a ha hk := Int.mul_nonpos_of_nonneg_of_nonpos hk ha
-  hmul_nonneg k a ha hk := Int.mul_nonneg hk ha
+  hmul_nonneg hk ha := Int.mul_nonneg hk ha
+
+instance : Ring.IsOrdered 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
 
 end Lean.Grind

src/Init/Grind/Ordered/Module.lean

@@ -0,0 +1,69 @@
+/-
+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.Data.Int.Order
+import Init.Grind.Module.Basic
+import Init.Grind.Ordered.PartialOrder
+
+namespace Lean.Grind
+
+class IntModule.IsOrdered (M : Type u) [Preorder M] [IntModule M] where
+  neg_le_iff : ∀ a b : M, -a ≤ b ↔ -b ≤ a
+  add_le_left : ∀ {a b : M}, a ≤ b → (c : M) → a + c ≤ b + c
+  hmul_pos : ∀ (k : Int) {a : M}, 0 < a → (0 < k ↔ 0 < k * a)
+  hmul_nonneg : ∀ {k : Int} {a : M}, 0 ≤ k → 0 ≤ a → 0 ≤ k * a
+
+namespace IntModule.IsOrdered
+
+variable {M : Type u} [Preorder M] [IntModule M] [IntModule.IsOrdered M]
+
+theorem le_neg_iff {a b : M} : a ≤ -b ↔ b ≤ -a := by
+  conv => lhs; rw [← neg_neg a]
+  rw [neg_le_iff, neg_neg]
+
+theorem neg_lt_iff {a b : M} : -a < b ↔ -b < a := by
+  simp [Preorder.lt_iff_le_not_le]
+  rw [neg_le_iff, le_neg_iff]
+
+theorem lt_neg_iff {a b : M} : a < -b ↔ b < -a := by
+  conv => lhs; rw [← neg_neg a]
+  rw [neg_lt_iff, neg_neg]
+
+theorem neg_nonneg_iff {a : M} : 0 ≤ -a ↔ a ≤ 0 := by
+  rw [le_neg_iff, neg_zero]
+
+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 [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 hmul_neg (k : Int) {a : M} (h : a < 0) : 0 < k ↔ k * a < 0 := by
+  simpa [IntModule.hmul_neg, neg_pos_iff] using hmul_pos 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)
+
+end IntModule.IsOrdered
+
+end Lean.Grind

src/Init/Grind/Ordered/PartialOrder.lean

@@ -0,0 +1,61 @@
+/-
+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.Data.Int.Order
+
+namespace Lean.Grind
+
+/-- A preorder is a reflexive, transitive relation `≤` with `a < b` defined in the obvious way. -/
+class Preorder (α : Type u) extends LE α, LT α where
+  le_refl : ∀ a : α, a ≤ a
+  le_trans : ∀ {a b c : α}, a ≤ b → b ≤ c → a ≤ c
+  lt := fun a b => a ≤ b ∧ ¬b ≤ a
+  lt_iff_le_not_le : ∀ {a b : α}, a < b ↔ a ≤ b ∧ ¬b ≤ a := by intros; rfl
+
+namespace Preorder
+
+variable {α : Type u} [Preorder α]
+
+theorem le_of_lt {a b : α} (h : a < b) : a ≤ b := (lt_iff_le_not_le.mp h).1
+
+theorem lt_of_lt_of_le {a b c : α} (h₁ : a < b) (h₂ : b ≤ c) : a < c := by
+  simp [lt_iff_le_not_le] at h₁ ⊢
+  exact ⟨le_trans h₁.1 h₂, fun h => h₁.2 (le_trans h₂ h)⟩
+
+theorem lt_of_le_of_lt {a b c : α} (h₁ : a ≤ b) (h₂ : b < c) : a < c := by
+  simp [lt_iff_le_not_le] at h₂ ⊢
+  exact ⟨le_trans h₁ h₂.1, fun h => h₂.2 (le_trans h h₁)⟩
+
+theorem lt_trans {a b c : α} (h₁ : a < b) (h₂ : b < c) : a < c :=
+  lt_of_lt_of_le h₁ (le_of_lt h₂)
+
+theorem lt_irrefl {a : α} (h : a < a) : False := by
+  simp [lt_iff_le_not_le] at h
+
+end Preorder
+
+class PartialOrder (α : Type u) extends Preorder α where
+  le_antisymm : ∀ {a b : α}, a ≤ b → b ≤ a → a = b
+
+namespace PartialOrder
+
+variable {α : Type u} [PartialOrder α]
+
+theorem le_iff_lt_or_eq {a b : α} : a ≤ b ↔ a < b ∨ a = b := by
+  constructor
+  · intro h
+    rw [Preorder.lt_iff_le_not_le, Classical.or_iff_not_imp_right]
+    exact fun w => ⟨h, fun w' => w (le_antisymm h w')⟩
+  · intro h
+    cases h with
+    | inl h => exact Preorder.le_of_lt h
+    | inr h => subst h; exact Preorder.le_refl a
+
+end PartialOrder
+
+end Lean.Grind

src/Init/Grind/Ordered/Ring.lean

@@ -0,0 +1,66 @@
+/-
+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.CommRing.Basic
+import Init.Grind.Ordered.Module
+
+namespace Lean.Grind
+
+class Ring.IsOrdered (R : Type u) [Ring R] [Preorder R] extends IntModule.IsOrdered R where
+  /-- In a strict ordered semiring, we have `0 < 1`. -/
+  zero_lt_one : 0 < 1
+  /-- In a strict ordered semiring, we can multiply an inequality `a < b` on the left
+  by a positive element `0 < c` to obtain `c * a < c * b`. -/
+  mul_lt_mul_of_pos_left : ∀ {a b c : R}, a < b → 0 < c → c * a < c * b
+  /-- In a strict ordered semiring, we can multiply an inequality `a < b` on the right
+  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
+
+variable {R : Type u} [Ring R] [PartialOrder R] [Ring.IsOrdered R]
+
+theorem mul_le_mul_of_nonneg_left {a b c : R} (h : a ≤ b) (h' : 0 ≤ c) : c * a ≤ c * b := by
+  rw [PartialOrder.le_iff_lt_or_eq] at h'
+  cases h' with
+  | inl h' =>
+    have p := mul_lt_mul_of_pos_left (a := a) (b := b) (c := c)
+    rw [PartialOrder.le_iff_lt_or_eq] at h
+    cases h with
+    | inl h => exact Preorder.le_of_lt (p h h')
+    | inr h => subst h; exact Preorder.le_refl (c * a)
+  | inr h' => subst h'; simp [Semiring.zero_mul, Preorder.le_refl]
+
+theorem mul_le_mul_of_nonneg_right {a b c : R} (h : a ≤ b) (h' : 0 ≤ c) : a * c ≤ b * c := by
+  rw [PartialOrder.le_iff_lt_or_eq] at h'
+  cases h' with
+  | inl h' =>
+    have p := mul_lt_mul_of_pos_right (a := a) (b := b) (c := c)
+    rw [PartialOrder.le_iff_lt_or_eq] at h
+    cases h with
+    | inl h => exact Preorder.le_of_lt (p h h')
+    | inr h => subst h; exact Preorder.le_refl (a * c)
+  | inr h' => subst h'; simp [Semiring.mul_zero, Preorder.le_refl]
+
+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_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 sq_nonneg {a : R} (h : 0 ≤ a) : 0 ≤ a^2 := by
+  rw [Semiring.pow_two]
+  apply mul_nonneg h h
+
+theorem sq_pos {a : R} (h : 0 < a) : 0 < a^2 := by
+  rw [Semiring.pow_two]
+  apply mul_pos h h
+
+end Ring.IsOrdered
+
+end Lean.Grind