ordered rings

Author: kim-em

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.lean

@@ -14,4 +14,3 @@ import Init.Grind.CommRing.Fin
 import Init.Grind.CommRing.BitVec
 import Init.Grind.CommRing.Poly
 import Init.Grind.CommRing.Field
-import Init.Grind.CommRing.Ordered

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]

src/Init/Grind/CommRing/Ordered.lean

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

src/Init/Grind/Module.lean

@@ -103,91 +103,6 @@ theorem hmul_neg (n : Int) (a : M) : n * (-a) = - (n * a) := by
 
 end IntModule
 
-/-- 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 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
-
 /--
 Special case of Mathlib's `NoZeroSMulDivisors Nat α`.
 -/

src/Init/Grind/Module/Basic.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.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
 
@@ -27,4 +27,9 @@ instance : IntModule.IsOrdered Int where
   hmul_pos k a ha := ⟨fun hk => Int.mul_pos hk ha, fun h => Int.pos_of_mul_pos_left h 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/Module/Int.lean src/Init/Grind/Ordered/Int.leansrc/Init/Grind/Module/Int.lean renamed to src/Init/Grind/Ordered/Int.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/Module.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