feat: lemmas about ordered rings and fields for grind (#8443)

This PR adds the lemmas about ordered rings and ordered fields which
will be needed by the new algebraic normalization components of `grind`.

Author: kim-em

src/Init/Grind/CommRing/Field.lean

@@ -12,8 +12,8 @@ namespace Lean.Grind
 
 class Field (α : Type u) extends CommRing α, Inv α, Div α where
   div_eq_mul_inv : ∀ a b : α, a / b = a * b⁻¹
+  zero_ne_one : (0 : α) ≠ 1
   inv_zero : (0 : α)⁻¹ = 0
-  inv_one : (1 : α)⁻¹ = 1
   mul_inv_cancel : ∀ {a : α}, a ≠ 0 → a * a⁻¹ = 1
 
 attribute [instance 100] Field.toInv Field.toDiv
@@ -25,6 +25,52 @@ variable [Field α] {a : α}
 theorem inv_mul_cancel (h : a ≠ 0) : a⁻¹ * a = 1 := by
   rw [CommSemiring.mul_comm, mul_inv_cancel h]
 
+theorem eq_inv_of_mul_eq_one (h : a * b = 1) : a = b⁻¹ := by
+  by_cases h' : b = 0
+  · subst h'
+    rw [Semiring.mul_zero] at h
+    exfalso
+    exact zero_ne_one h
+  · replace h := congrArg (fun x => x * b⁻¹) h
+    simpa [Semiring.mul_assoc, mul_inv_cancel h', Semiring.mul_one, Semiring.one_mul] using h
+
+theorem inv_one : (1 : α)⁻¹ = 1 :=
+  (eq_inv_of_mul_eq_one (Semiring.mul_one 1)).symm
+
+theorem inv_inv (a : α) : a⁻¹⁻¹ = a := by
+  by_cases h : a = 0
+  · subst h
+    simp [Field.inv_zero]
+  · symm
+    apply eq_inv_of_mul_eq_one
+    exact mul_inv_cancel h
+
+theorem inv_neg (a : α) : (-a)⁻¹ = -a⁻¹ := by
+  by_cases h : a = 0
+  · subst h
+    simp [Field.inv_zero, Ring.neg_zero]
+  · symm
+    apply eq_inv_of_mul_eq_one
+    simp [Ring.neg_mul, Ring.mul_neg, Ring.neg_neg, Field.inv_mul_cancel h]
+
+theorem inv_eq_zero_iff {a : α} : a⁻¹ = 0 ↔ a = 0 := by
+  constructor
+  · intro w
+    by_cases h : a = 0
+    · subst h
+      rfl
+    · have := congrArg (fun x => x * a) w
+      dsimp at this
+      rw [Semiring.zero_mul, inv_mul_cancel h] at this
+      exfalso
+      exact zero_ne_one this.symm
+  · intro w
+    subst w
+    simp [Field.inv_zero]
+
+theorem zero_eq_inv_iff {a : α} : 0 = a⁻¹ ↔ 0 = a := by
+  rw [eq_comm, inv_eq_zero_iff, eq_comm]
+
 instance [IsCharP α 0] : NoNatZeroDivisors α where
   no_nat_zero_divisors := by
     intro a b h w

src/Init/Grind/Ordered.lean

@@ -6,7 +6,8 @@ Authors: Kim Morrison
 module
 
 prelude
-import Init.Grind.Ordered.PartialOrder
+import Init.Grind.Ordered.Order
 import Init.Grind.Ordered.Module
 import Init.Grind.Ordered.Ring
+import Init.Grind.Ordered.Field
 import Init.Grind.Ordered.Int

src/Init/Grind/Ordered/Field.lean

@@ -0,0 +1,188 @@
+/-
+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.Field
+import Init.Grind.Ordered.Ring
+
+namespace Lean.Grind
+
+namespace Field.IsOrdered
+
+variable {R : Type u} [Field R] [LinearOrder R] [Ring.IsOrdered R]
+
+open Ring.IsOrdered
+
+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'
+    rw [inv_mul_cancel (Preorder.ne_of_lt h')] at this
+    exact Ring.IsOrdered.not_one_lt_zero this
+
+theorem inv_pos_iff {a : R} : 0 < a⁻¹ ↔ 0 < a := by
+  constructor
+  · exact pos_of_inv_pos
+  · intro h
+    rw [← Field.inv_inv a] at h
+    exact pos_of_inv_pos h
+
+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]
+
+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]
+
+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
+
+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)
+
+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))
+
+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⟩
+
+private theorem mul_inv_le_iff_le_mul (a c : R) {b : R} (h : 0 < b) : a * b⁻¹ ≤ c ↔ a ≤ c * b := by
+  have := (le_mul_inv_iff_mul_le a c (inv_pos_iff.mpr h)).symm
+  simpa [Field.inv_inv] using this
+
+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
+
+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)
+
+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⟩
+
+theorem mul_inv_lt_iff_lt_mul (a c : R) {b : R} (h : 0 < b) : a * b⁻¹ < c ↔ a < c * b := by
+  simpa [Field.inv_inv] using (lt_mul_inv_iff_mul_lt a c (inv_pos_iff.mpr h)).symm
+
+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)
+
+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)
+
+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))
+
+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))
+
+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⟩
+
+theorem mul_inv_le_iff_mul_le_of_neg (a c : R) {b : R} (h : b < 0) : a * b⁻¹ ≤ c ↔ c * b ≤ a :=
+  ⟨mul_le_of_mul_inv_le h, mul_inv_le_of_mul_le h⟩
+
+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
+
+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
+
+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)
+
+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)
+
+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⟩
+
+theorem mul_inv_lt_iff_mul_lt_of_neg (a c : R) {b : R} (h : b < 0) : a * b⁻¹ < c ↔ c * b < a :=
+  ⟨mul_lt_of_mul_inv_lt h, mul_inv_lt_of_mul_lt h⟩
+
+theorem mul_lt_mul_iff_of_pos_right {a b c : R} (h : 0 < c) : a * c < b * c ↔ a < b := by
+  constructor
+  · intro h'
+    have := mul_lt_mul_of_pos_right h' (inv_pos_iff.mpr h)
+    rwa [Semiring.mul_assoc, Semiring.mul_assoc, mul_inv_cancel (Preorder.ne_of_gt h),
+      Semiring.mul_one, Semiring.mul_one] at this
+  · exact (mul_lt_mul_of_pos_right · h)
+
+theorem mul_lt_mul_iff_of_pos_left {a b c : R} (h : 0 < c) : c * a < c * b ↔ a < b := by
+  constructor
+  · intro h'
+    have := mul_lt_mul_of_pos_left h' (inv_pos_iff.mpr h)
+    rwa [← Semiring.mul_assoc, ← Semiring.mul_assoc, inv_mul_cancel (Preorder.ne_of_gt h),
+      Semiring.one_mul, Semiring.one_mul] at this
+  · exact (mul_lt_mul_of_pos_left · h)
+
+theorem mul_lt_mul_iff_of_neg_right {a b c : R} (h : c < 0) : a * c < b * c ↔ b < a := by
+  constructor
+  · intro h'
+    have := mul_lt_mul_of_neg_right h' (inv_neg_iff.mpr h)
+    rwa [Semiring.mul_assoc, Semiring.mul_assoc, mul_inv_cancel (Preorder.ne_of_lt h),
+      Semiring.mul_one, Semiring.mul_one] at this
+  · exact (mul_lt_mul_of_neg_right · h)
+
+theorem mul_lt_mul_iff_of_neg_left {a b c : R} (h : c < 0) : c * a < c * b ↔ b < a := by
+  constructor
+  · intro h'
+    have := mul_lt_mul_of_neg_left h' (inv_neg_iff.mpr h)
+    rwa [← Semiring.mul_assoc, ← Semiring.mul_assoc, inv_mul_cancel (Preorder.ne_of_lt h),
+      Semiring.one_mul, Semiring.one_mul] at this
+  · exact (mul_lt_mul_of_neg_left · h)
+
+theorem mul_le_mul_iff_of_pos_right {a b c : R} (h : 0 < c) : a * c ≤ b * c ↔ a ≤ b := by
+  constructor
+  · intro h'
+    have := mul_le_mul_of_nonneg_right h' (Preorder.le_of_lt (inv_pos_iff.mpr h))
+    rwa [Semiring.mul_assoc, Semiring.mul_assoc, mul_inv_cancel (Preorder.ne_of_gt h),
+      Semiring.mul_one, Semiring.mul_one] at this
+  · exact (mul_le_mul_of_nonneg_right · (Preorder.le_of_lt h))
+
+theorem mul_le_mul_iff_of_pos_left {a b c : R} (h : 0 < c) : c * a ≤ c * b ↔ a ≤ b := by
+  constructor
+  · intro h'
+    have := mul_le_mul_of_nonneg_left h' (Preorder.le_of_lt (inv_pos_iff.mpr h))
+    rwa [← Semiring.mul_assoc, ← Semiring.mul_assoc, inv_mul_cancel (Preorder.ne_of_gt h),
+      Semiring.one_mul, Semiring.one_mul] at this
+  · exact (mul_le_mul_of_nonneg_left · (Preorder.le_of_lt h))
+
+theorem mul_le_mul_iff_of_neg_right {a b c : R} (h : c < 0) : a * c ≤ b * c ↔ b ≤ a := by
+  constructor
+  · intro h'
+    have := mul_le_mul_of_nonpos_right h' (Preorder.le_of_lt (inv_neg_iff.mpr h))
+    rwa [Semiring.mul_assoc, Semiring.mul_assoc, mul_inv_cancel (Preorder.ne_of_lt h),
+      Semiring.mul_one, Semiring.mul_one] at this
+  · exact (mul_le_mul_of_nonpos_right · (Preorder.le_of_lt h))
+
+theorem mul_le_mul_iff_of_neg_left {a b c : R} (h : c < 0) : c * a ≤ c * b ↔ b ≤ a := by
+  constructor
+  · intro h'
+    have := mul_le_mul_of_nonpos_left h' (Preorder.le_of_lt (inv_neg_iff.mpr h))
+    rwa [← Semiring.mul_assoc, ← Semiring.mul_assoc, inv_mul_cancel (Preorder.ne_of_lt h),
+      Semiring.one_mul, Semiring.one_mul] at this
+  · exact (mul_le_mul_of_nonpos_left · (Preorder.le_of_lt h))
+
+end Field.IsOrdered
+
+end Lean.Grind

src/Init/Grind/Ordered/Module.lean

@@ -8,7 +8,7 @@ module
 prelude
 import Init.Data.Int.Order
 import Init.Grind.Module.Basic
-import Init.Grind.Ordered.PartialOrder
+import Init.Grind.Ordered.Order
 
 namespace Lean.Grind
 

src/Init/Grind/Ordered/PartialOrder.lean renamed to src/Init/Grind/Ordered/Order.lean

@@ -34,9 +34,22 @@ theorem lt_of_le_of_lt {a b c : α} (h₁ : a ≤ b) (h₂ : b < c) : a < c := b
 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
+theorem lt_irrefl (a : α) : ¬ (a < a) := by
+  intro h
   simp [lt_iff_le_not_le] at h
 
+theorem ne_of_lt {a b : α} (h : a < b) : a ≠ b :=
+  fun w => lt_irrefl a (w.symm ▸ h)
+
+theorem ne_of_gt {a b : α} (h : a > b) : a ≠ b :=
+  fun w => lt_irrefl b (w.symm ▸ h)
+
+theorem not_ge_of_lt {a b : α} (h : a < b) : ¬b ≤ a :=
+  fun w => lt_irrefl a (lt_of_lt_of_le h w)
+
+theorem not_gt_of_lt {a b : α} (h : a < b) : ¬a > b :=
+  fun w => lt_irrefl a (lt_trans h w)
+
 end Preorder
 
 class PartialOrder (α : Type u) extends Preorder α where
@@ -58,4 +71,26 @@ theorem le_iff_lt_or_eq {a b : α} : a ≤ b ↔ a < b ∨ a = b := by
 
 end PartialOrder
 
+class LinearOrder (α : Type u) extends PartialOrder α where
+  le_total : ∀ a b : α, a ≤ b ∨ b ≤ a
+
+namespace LinearOrder
+
+variable {α : Type u} [LinearOrder α]
+
+theorem trichotomy (a b : α) : a < b ∨ a = b ∨ b < a := by
+  cases LinearOrder.le_total a b with
+  | inl h =>
+    rw [PartialOrder.le_iff_lt_or_eq] at h
+    cases h with
+    | inl h => left; exact h
+    | inr h => right; left; exact h
+  | inr h =>
+    rw [PartialOrder.le_iff_lt_or_eq] at h
+    cases h with
+    | inl h => right; right; exact h
+    | inr h => right; left; exact h.symm
+
+end LinearOrder
+
 end Lean.Grind