feat: the grothendieck envelope of an ordered semiring is an ordered ring (#8959)

This PR add instances showing that the Grothendieck (i.e. additive)
envelope of a semiring is an ordered ring if the original semiring is
ordered (and satisfies ExistsAddOfLE), and in this case the embedding is
monotone.

src/Init/Grind/Ordered/Module.lean

@@ -19,6 +19,9 @@ 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
 
+class ExistsAddOfLT (α : Type u) [LT α] [Zero α] [Add α] where
+  exists_add_of_le : ∀ {a b : α}, a < b → ∃ c, 0 < c ∧ b = a + c
+
 namespace OrderedAdd
 
 open NatModule

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 OrderedRing (R : Type u) [Ring R] [Preorder R] extends OrderedAdd R where
+class OrderedRing (R : Type u) [Semiring 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

src/Init/Grind/Ring/Envelope.lean

@@ -7,6 +7,7 @@ module
 
 prelude
 import Init.Grind.Ring.Basic
+import Init.Grind.Ordered.Ring
 import all Init.Data.AC
 
 namespace Lean.Grind.Ring
@@ -98,6 +99,9 @@ def Q.liftOn₂ (q₁ q₂ : Q α)
 
 attribute [local simp] Q.mk Q.liftOn₂
 
+def Q.ind {β : Q α → Prop} (mk : ∀ (a : α × α), β (Q.mk a)) (q : Q α) : β q :=
+  Quot.ind mk q
+
 @[local simp] def natCast (n : Nat) : Q α :=
   Q.mk (n, 0)
 
@@ -244,16 +248,26 @@ def ofSemiring : Ring (Q α) := {
 
 attribute [instance] ofSemiring
 
+@[local simp] private theorem mk_add_mk {a₁ a₂ b₁ b₂ : α} :
+    Q.mk (a₁, a₂) + Q.mk (b₁, b₂) = Q.mk (a₁ + b₁, a₂ + b₂) := by
+  rfl
+
+@[local simp] private theorem mk_mul_mk {a₁ a₂ b₁ b₂ : α} :
+    Q.mk (a₁, a₂) * Q.mk (b₁, b₂) = Q.mk (a₁*b₁ + a₂*b₂, a₁*b₂ + a₂*b₁) := by
+  rfl
+
 @[local simp] def toQ (a : α) : Q α :=
   Q.mk (a, 0)
 
+attribute [-simp] Q.mk
+
 /-! Embedding theorems -/
 
 theorem toQ_add (a b : α) : toQ (a + b) = toQ a + toQ b := by
-  simp; apply Quot.sound; simp
+  simp
 
 theorem toQ_mul (a b : α) : toQ (a * b) = toQ a * toQ b := by
-  simp; apply Quot.sound; simp
+  simp
 
 theorem toQ_natCast (n : Nat) : toQ (natCast (α := α) n) = natCast n := by
   simp; apply Quot.sound; simp; refine ⟨0, ?_⟩; rfl
@@ -336,6 +350,121 @@ instance {p} [Semiring α] [AddRightCancel α] [IsCharP α p] : IsCharP (OfSemir
       apply Quot.sound
       exists 0; simp [← Semiring.ofNat_eq_natCast, this]
 
+instance [Preorder α] [OrderedAdd α] : LE (OfSemiring.Q α) where
+  le a b := Q.liftOn₂ a b (fun (a, b) (c, d) => a + d ≤ b + c)
+    (by intro (a₁, b₁) (a₂, b₂) (a₃, b₃) (a₄, b₄)
+        simp; intro k₁ h₁ k₂ h₂
+        rw [OrderedAdd.add_le_left_iff (b₃ + k₁)]
+        have : a₁ + b₂ + (b₃ + k₁) = a₁ + b₃ + k₁ + b₂ := by ac_rfl
+        rw [this, h₁]; clear this
+        rw [OrderedAdd.add_le_left_iff (a₄ + k₂)]
+        have : b₁ + a₃ + k₁ + b₂ + (a₄ + k₂) = b₂ + a₄ + k₂ + b₁ + a₃ + k₁ := by ac_rfl
+        rw [this, ← h₂]; clear this
+        have : a₂ + b₄ + k₂ + b₁ + a₃ + k₁ = a₃ + b₄ + (a₂ + b₁ + k₁ + k₂) := by ac_rfl
+        rw [this]; clear this
+        have : b₁ + a₂ + (b₃ + k₁) + (a₄ + k₂) = b₃ + a₄ + (a₂ + b₁ + k₁ + k₂) := by ac_rfl
+        rw [this]; clear this
+        rw [← OrderedAdd.add_le_left_iff])
+
+@[local simp] theorem mk_le_mk [Preorder α] [OrderedAdd α] {a₁ a₂ b₁ b₂ : α}  :
+    Q.mk (a₁, a₂) ≤ Q.mk (b₁, b₂) ↔ a₁ + b₂ ≤ a₂ + b₁ := by
+  rfl
+
+instance [Preorder α] [OrderedAdd α] : Preorder (OfSemiring.Q α) where
+  le_refl a := by
+    induction a using Quot.ind
+    next a =>
+    rcases a with ⟨a₁, a₂⟩
+    change Q.mk _ ≤ Q.mk _
+    simp only [mk_le_mk]
+    simp [Semiring.add_comm]; exact Preorder.le_refl (a₁ + a₂)
+  le_trans {a b c} h₁ h₂ := by
+    induction a using Q.ind
+    induction b using Q.ind
+    induction c using Q.ind
+    next a b c =>
+    rcases a with ⟨a₁, a₂⟩; rcases b with ⟨b₁, b₂⟩; rcases c with ⟨c₁, c₂⟩
+    simp only [mk_le_mk] at h₁ h₂ ⊢
+    rw [OrderedAdd.add_le_left_iff (b₁ + b₂)]
+    have : a₁ + c₂ + (b₁ + b₂) = a₁ + b₂ + (b₁ + c₂) := by ac_rfl
+    rw [this]; clear this
+    have : a₂ + c₁ + (b₁ + b₂) = a₂ + b₁ + (b₂ + c₁) := by ac_rfl
+    rw [this]; clear this
+    exact OrderedAdd.add_le_add h₁ h₂
+
+@[local simp] private theorem mk_lt_mk [Preorder α] [OrderedAdd α] {a₁ a₂ b₁ b₂ : α}  :
+    Q.mk (a₁, a₂) < Q.mk (b₁, b₂) ↔ a₁ + b₂ < a₂ + b₁ := by
+  simp [Preorder.lt_iff_le_not_le, Semiring.add_comm]
+
+@[local simp] private theorem mk_pos [Preorder α] [OrderedAdd α] {a₁ a₂ : α} :
+    0 < Q.mk (a₁, a₂) ↔ a₂ < a₁ := by
+  simp [← toQ_ofNat, toQ, mk_lt_mk, Semiring.zero_add]
+
+@[local simp]
+theorem toQ_le [Preorder α] [OrderedAdd α] {a b : α} : toQ a ≤ toQ b ↔ a ≤ b := by
+  simp
+
+@[local simp]
+theorem toQ_lt [Preorder α] [OrderedAdd α] {a b : α} : toQ a < toQ b ↔ a < b := by
+  simp [Preorder.lt_iff_le_not_le]
+
+instance [Preorder α] [OrderedAdd α] : OrderedAdd (OfSemiring.Q α) where
+  add_le_left_iff := by
+    intro a b c
+    induction a using Quot.ind
+    induction b using Quot.ind
+    induction c using Quot.ind
+    next a b c =>
+    rcases a with ⟨a₁, a₂⟩; rcases b with ⟨b₁, b₂⟩; rcases c with ⟨c₁, c₂⟩
+    change a₁ + b₂ ≤ a₂ + b₁ ↔ (a₁ + c₁) + _ ≤ _
+    have : a₁ + c₁ + (b₂ + c₂) = a₁ + b₂ + (c₁ + c₂) := by ac_rfl
+    rw [this]; clear this
+    have : a₂ + c₂ + (b₁ + c₁) = a₂ + b₁ + (c₁ + c₂) := by ac_rfl
+    rw [this]; clear this
+    rw [← OrderedAdd.add_le_left_iff]
+
+-- This perhaps works in more generality than `ExistsAddOfLT`?
+instance [Preorder α] [OrderedRing α] [ExistsAddOfLT α] : OrderedRing (OfSemiring.Q α) where
+  zero_lt_one := by
+    rw [← toQ_ofNat, ← toQ_ofNat, toQ_lt]
+    exact OrderedRing.zero_lt_one
+  mul_lt_mul_of_pos_left := by
+    intro a b c h₁ h₂
+    induction a using Q.ind
+    induction b using Q.ind
+    induction c using Q.ind
+    next a b c =>
+    rcases a with ⟨a₁, a₂⟩; rcases b with ⟨b₁, b₂⟩; rcases c with ⟨c₁, c₂⟩
+    simp at h₁ h₂ ⊢
+    obtain ⟨d, d_pos, rfl⟩ := ExistsAddOfLT.exists_add_of_le h₂
+    simp [Semiring.right_distrib]
+    have : c₂ * a₁ + d * a₁ + c₂ * a₂ + (c₂ * b₂ + d * b₂ + c₂ * b₁) =
+      c₂ * a₁ + c₂ * a₂ + c₂ * b₁ + c₂ * b₂ + (d * a₁ + d * b₂) := by ac_rfl
+    rw [this]; clear this
+    have : c₂ * a₂ + d * a₂ + c₂ * a₁ + (c₂ * b₁ + d * b₁ + c₂ * b₂) =
+      c₂ * a₁ + c₂ * a₂ + c₂ * b₁ + c₂ * b₂ + (d * a₂ + d * b₁) := by ac_rfl
+    rw [this]; clear this
+    rw [← OrderedAdd.add_lt_right_iff]
+    simpa [Semiring.left_distrib] using OrderedRing.mul_lt_mul_of_pos_left h₁ d_pos
+  mul_lt_mul_of_pos_right := by
+    intro a b c h₁ h₂
+    induction a using Q.ind
+    induction b using Q.ind
+    induction c using Q.ind
+    next a b c =>
+    rcases a with ⟨a₁, a₂⟩; rcases b with ⟨b₁, b₂⟩; rcases c with ⟨c₁, c₂⟩
+    simp at h₁ h₂ ⊢
+    obtain ⟨d, d_pos, rfl⟩ := ExistsAddOfLT.exists_add_of_le h₂
+    simp [Semiring.left_distrib]
+    have : a₁ * c₂ + a₁ * d + a₂ * c₂ + (b₁ * c₂ + (b₂ * c₂ + b₂ * d)) =
+      a₁ * c₂ + a₂ * c₂ + b₁ * c₂ + b₂ * c₂ + (a₁ * d + b₂ * d) := by ac_rfl
+    rw [this]; clear this
+    have : a₁ * c₂ + (a₂ * c₂ + a₂ * d) + (b₁ * c₂ + b₁ * d + b₂ * c₂) =
+      a₁ * c₂ + a₂ * c₂ + b₁ * c₂ + b₂ * c₂ + (a₂ * d + b₁ * d) := by ac_rfl
+    rw [this]; clear this
+    rw [← OrderedAdd.add_lt_right_iff]
+    simpa [Semiring.right_distrib] using OrderedRing.mul_lt_mul_of_pos_right h₁ d_pos
+
 end OfSemiring
 end Lean.Grind.Ring
 

src/Init/GrindInstances/Nat.lean

@@ -6,7 +6,7 @@ Authors: Kim Morrison
 module
 prelude
 
-import Init.Grind.Module.Basic
+import Init.Grind.Ordered.Module
 import Init.Grind.Ring.Basic
 
 namespace Lean.Grind
@@ -14,4 +14,7 @@ namespace Lean.Grind
 instance : AddRightCancel Nat where
   add_right_cancel _ _ _ := Nat.add_right_cancel
 
+instance : ExistsAddOfLT Nat where
+  exists_add_of_le {a b} h := ⟨b - a, by omega⟩
+
 end Lean.Grind

src/Init/GrindInstances/Ring/Nat.lean

@@ -6,7 +6,7 @@ Authors: Kim Morrison
 module
 
 prelude
-import Init.Grind.Ring.Basic
+import Init.Grind.Ordered.Ring
 import Init.Data.Int.Lemmas
 
 namespace Lean.Grind
@@ -27,6 +27,17 @@ instance : CommSemiring Nat where
   pow_succ _ _ := by rfl
   ofNat_succ _ := by rfl
 
+instance : Preorder Nat where
+  le_refl := by omega
+  le_trans := by omega
+  lt_iff_le_not_le := by omega
+
+instance : OrderedRing Nat where
+  add_le_left_iff := by omega
+  zero_lt_one := by omega
+  mul_lt_mul_of_pos_left h₁ h₂ := Nat.mul_lt_mul_of_pos_left h₁ h₂
+  mul_lt_mul_of_pos_right h₁ h₂ := Nat.mul_lt_mul_of_pos_right h₁ h₂
+
 instance : IsCharP Nat 0 where
   ofNat_ext_iff {x y} := by simp [OfNat.ofNat]
 

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

@@ -173,11 +173,11 @@ where
     let one? ← getOne?
     let commRingInst? ← getInst? ``Grind.CommRing
     let getOrderedRingInst? : GoalM (Option Expr) := do
-      let some ringInst := ringInst? | return none
+      let some semiringInst := semiringInst? | return none
       let some preorderInst := preorderInst? | return none
-      let isOrdType := mkApp3 (mkConst ``Grind.OrderedRing [u]) type ringInst preorderInst
+      let isOrdType := mkApp3 (mkConst ``Grind.OrderedRing [u]) type semiringInst preorderInst
       let .some inst ← trySynthInstance isOrdType
-        | reportIssue! "type has a `Preorder` and is a `Ring`, but is not an ordered ring, failed to synthesize{indentExpr isOrdType}"
+        | reportIssue! "type has a `Preorder` and is a `Semiring`, but is not an ordered ring, failed to synthesize{indentExpr isOrdType}"
           return none
       return some inst
     let orderedRingInst? ← getOrderedRingInst?

tests/lean/run/grind_linarith_1.lean

@@ -65,7 +65,7 @@ example [CommRing α] [Preorder α] [OrderedRing α] (a b c : α)
 
 -- Test misconfigured instances
 /--
-trace: [grind.issues] type has a `Preorder` and is a `Ring`, but is not an ordered ring, failed to synthesize
+trace: [grind.issues] type has a `Preorder` and is a `Semiring`, but is not an ordered ring, failed to synthesize
       OrderedRing α
 -/
 #guard_msgs (drop error, trace) in

tests/lean/run/grind_nat_semiring.lean

@@ -1,3 +1,6 @@
 example (a b : Nat) : 3 * a * b = a * b * 3 := by grind
 
 example (k z : Nat) : k * (z * 2 * (z * 2 + 1)) = z * (k * (2 * (z * 2 + 1))) := by grind
+
+open Lean.Grind in
+example : OrderedRing (Ring.OfSemiring.Q Nat) := inferInstance