feat: CommRing interface for grind linarith (#8670)

This PR adds helper theorems that will be used to interface the
`CommRing` module with the linarith procedure in `grind`.

Author: leodemoura

src/Init/Grind/CommRing/Poly.lean

@@ -11,6 +11,7 @@ import Init.Data.Hashable
 import all Init.Data.Ord
 import Init.Data.RArray
 import Init.Grind.CommRing.Basic
+import Init.Grind.Ordered.Ring
 
 namespace Lean.Grind
 namespace CommRing
@@ -35,13 +36,13 @@ abbrev Context (α : Type u) := RArray α
 def Var.denote {α} (ctx : Context α) (v : Var) : α :=
   ctx.get v
 
-def denoteInt {α} [CommRing α] (k : Int) : α :=
+def denoteInt {α} [Ring α] (k : Int) : α :=
   bif k < 0 then
     - OfNat.ofNat (α := α) k.natAbs
   else
     OfNat.ofNat (α := α) k.natAbs
 
-def Expr.denote {α} [CommRing α] (ctx : Context α) : Expr → α
+def Expr.denote {α} [Ring α] (ctx : Context α) : Expr → α
   | .add a b  => denote ctx a + denote ctx b
   | .sub a b  => denote ctx a - denote ctx b
   | .mul a b  => denote ctx a * denote ctx b
@@ -1139,5 +1140,72 @@ theorem imp_keqC {α c} [CommRing α] [IsCharP α c] (ctx : Context α) [NoNatZe
 
 end Stepwise
 
+/-! IntModule interface -/
+
+def Poly.denoteAsIntModule [CommRing α] (ctx : Context α) (p : Poly) : α :=
+  match p with
+  | .num k => Int.cast k * 1
+  | .add k m p => Int.cast k * m.denote ctx + denote ctx p
+
+theorem Poly.denoteAsIntModule_eq_denote {α} [CommRing α] (ctx : Context α) (p : Poly) : p.denoteAsIntModule ctx = p.denote ctx := by
+  induction p <;> simp [*, denoteAsIntModule, denote, mul_one]
+
+open Stepwise
+
+theorem eq_norm {α} [CommRing α] (ctx : Context α) (lhs rhs : Expr) (p : Poly)
+    : core_cert lhs rhs p → lhs.denote ctx = rhs.denote ctx → p.denoteAsIntModule ctx = 0 := by
+  rw [Poly.denoteAsIntModule_eq_denote]; apply core
+
+theorem diseq_norm {α} [CommRing α] (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; rw [sub_eq_zero_iff] at h; contradiction
+
+open IntModule.IsOrdered
+
+theorem le_norm {α} [CommRing α] [Preorder α] [Ring.IsOrdered α] (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)
+    : 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)
+    : core_cert rhs lhs p → ¬ lhs.denote ctx ≤ rhs.denote ctx → p.denote ctx < 0 := by
+  simp [core_cert]; intro _ h₁; subst p; simp [Expr.denote_toPoly, Expr.denote]
+  replace h₁ := LinearOrder.lt_of_not_le h₁
+  replace h₁ := add_lt_left h₁ (-lhs.denote 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)
+    : core_cert rhs lhs p → ¬ lhs.denote ctx < rhs.denote ctx → p.denote ctx ≤ 0 := by
+  simp [core_cert]; intro _ h₁; subst p; simp [Expr.denote_toPoly, Expr.denote]
+  replace h₁ := LinearOrder.le_of_not_lt h₁
+  replace h₁ := add_le_left h₁ (-lhs.denote 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)
+    : core_cert lhs rhs p → ¬ lhs.denote ctx ≤ rhs.denote ctx → ¬ p.denote ctx ≤ 0 := by
+  simp [core_cert]; 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)
+    : core_cert lhs rhs p → ¬ lhs.denote ctx < rhs.denote ctx → ¬ p.denote ctx < 0 := by
+  simp [core_cert]; intro _ h₁; subst p; simp [Expr.denote_toPoly, Expr.denote]; intro h
+  replace h := add_lt_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
+
 end CommRing
 end Lean.Grind

src/Init/Grind/Ordered/Linarith.lean

@@ -386,35 +386,38 @@ theorem lt_norm {α} [IntModule α] [Preorder α] [IntModule.IsOrdered α] (ctx
   simp [← sub_eq_add_neg, sub_self] at h₁
   assumption
 
-private theorem le_of_not_lt {α} [LinearOrder α] {a b : α} (h : ¬ a < b) : b ≤ a := by
-  cases LinearOrder.trichotomy a b
-  next => contradiction
-  next h => apply PartialOrder.le_iff_lt_or_eq.mpr; cases h <;> simp [*]
-
-private theorem lt_of_not_le {α} [LinearOrder α] {a b : α} (h : ¬ a ≤ b) : b < a := by
-  cases LinearOrder.trichotomy a b
-  next h₁ h₂ => have := Preorder.lt_iff_le_not_le.mp h₂; simp [h] at this
-  next h =>
-    cases h
-    next h => subst a; exact False.elim <| h (Preorder.le_refl b)
-    next => assumption
-
 theorem not_le_norm {α} [IntModule α] [LinearOrder α] [IntModule.IsOrdered α] (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, h₁, sub_self]
-  replace h₁ := lt_of_not_le h₁
+  replace h₁ := LinearOrder.lt_of_not_le h₁
   replace h₁ := add_lt_left h₁ (-lhs.denote ctx)
   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)
     : 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, h₁, sub_self]
-  replace h₁ := le_of_not_lt h₁
+  replace h₁ := LinearOrder.le_of_not_lt h₁
   replace h₁ := add_le_left h₁ (-lhs.denote ctx)
   simp [← sub_eq_add_neg, sub_self] at h₁
   assumption
 
+-- 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)
+    : 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]; 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)
+    : 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]; intro h
+  replace h := add_lt_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
+
 /-!
 Equality detection
 -/
@@ -459,7 +462,7 @@ theorem le_coeff {α} [IntModule α] [LinearOrder α] [IntModule.IsOrdered α] (
   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₂ := lt_of_not_le h₂
+  intro h₂; replace h₂ := LinearOrder.lt_of_not_le h₂
   replace h₂ := IsOrdered.hmul_pos (↑k) h₂ |>.mp this
   exact Preorder.lt_irrefl 0 (Preorder.lt_of_lt_of_le h₂ h₁)
 
@@ -468,7 +471,7 @@ theorem lt_coeff {α} [IntModule α] [LinearOrder α] [IntModule.IsOrdered α] (
   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₂ := le_of_not_lt h₂
+  intro h₂; replace h₂ := LinearOrder.le_of_not_lt h₂
   replace h₂ := IsOrdered.hmul_nonneg (Int.le_of_lt this) h₂
   exact Preorder.lt_irrefl 0 (Preorder.lt_of_le_of_lt h₂ h₁)
 

src/Init/Grind/Ordered/Order.lean

@@ -91,6 +91,19 @@ theorem trichotomy (a b : α) : a < b ∨ a = b ∨ b < a := by
     | inl h => right; right; exact h
     | inr h => right; left; exact h.symm
 
+theorem le_of_not_lt {α} [LinearOrder α] {a b : α} (h : ¬ a < b) : b ≤ a := by
+  cases LinearOrder.trichotomy a b
+  next => contradiction
+  next h => apply PartialOrder.le_iff_lt_or_eq.mpr; cases h <;> simp [*]
+
+theorem lt_of_not_le {α} [LinearOrder α] {a b : α} (h : ¬ a ≤ b) : b < a := by
+  cases LinearOrder.trichotomy a b
+  next h₁ h₂ => have := Preorder.lt_iff_le_not_le.mp h₂; simp [h] at this
+  next h =>
+    cases h
+    next h => subst a; exact False.elim <| h (Preorder.le_refl b)
+    next => assumption
+
 end LinearOrder
 
 end Lean.Grind