From 0eb9671787a01aaa77e8876b2fe5a214d8cbe68c Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Tue, 29 Apr 2025 18:03:57 -0700
Subject: [PATCH] fix: proof term for Nullstellensatz certificate (#8168)

This PR fixes a bug when constructing the proof term for a
Nullstellensatz certificate produced by the new commutative ring
procedure in `grind`. The kernel was rejecting the proof term.
---
 .../Tactic/Grind/Arith/CommRing/Proof.lean    |  6 +++---
 tests/lean/grind/grobner_type_mismatch.lean   | 20 +------------------
 tests/lean/run/grind_ring_2.lean              |  3 +++
 tests/lean/run/grind_ring_4.lean              | 18 +++++++++++++++++
 4 files changed, 25 insertions(+), 22 deletions(-)
 create mode 100644 tests/lean/run/grind_ring_4.lean

diff --git a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Proof.lean b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Proof.lean
index 372d885867..5fe2660bae 100644
--- a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Proof.lean
+++ b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Proof.lean
@@ -231,11 +231,11 @@ def EqCnstr.setUnsat (c : EqCnstr) : RingM Unit := do
 def DiseqCnstr.setUnsat (c : DiseqCnstr) : RingM Unit := do
   trace_goal[grind.ring.assert.unsat] "{← c.denoteExpr}"
   let ncx ← c.mkNullCertExt
-  trace_goal[grind.ring.assert.unsat] "{ncx.d}*({← c.d.p.denoteExpr}), {← (← ncx.toPoly).denoteExpr}"
+  trace_goal[grind.ring.assert.unsat] "multiplier: {c.d.getMultiplier}, {ncx.d}*({← c.d.p.denoteExpr}), {← (← ncx.toPoly).denoteExpr}"
   let nc := toExpr (ncx.toNullCert)
   let ring ← getRing
   let ctx ← toContextExpr
-  let k := c.d.getMultiplier
+  let k := c.d.getMultiplier * ncx.d
   let h := match (← nonzeroCharInst?), (← getNoZeroDivInstIfNeeded? k) with
     | some (charInst, char), some nzDivInst =>
       mkApp8 (mkConst ``Grind.CommRing.NullCert.ne_nzdiv_unsatC [ring.u]) ring.type (toExpr char) ring.commRingInst charInst nzDivInst ctx nc (toExpr k)
@@ -253,7 +253,7 @@ def propagateEq (a b : Expr) (ra rb : RingExpr) (d : PolyDerivation) : RingM Uni
   let nc := toExpr (ncx.toNullCert)
   let ring ← getRing
   let ctx ← toContextExpr
-  let k := d.getMultiplier
+  let k := d.getMultiplier * ncx.d
   let h := match (← nonzeroCharInst?), (← getNoZeroDivInstIfNeeded? k) with
     | some (charInst, char), some nzDivInst =>
       mkApp8 (mkConst ``Grind.CommRing.NullCert.eq_nzdivC [ring.u]) ring.type (toExpr char) ring.commRingInst charInst nzDivInst ctx nc (toExpr k)
diff --git a/tests/lean/grind/grobner_type_mismatch.lean b/tests/lean/grind/grobner_type_mismatch.lean
index bbf8d6679c..b68042627b 100644
--- a/tests/lean/grind/grobner_type_mismatch.lean
+++ b/tests/lean/grind/grobner_type_mismatch.lean
@@ -1,24 +1,6 @@
 open Lean.Grind
 
--- These are variants of the calculation in `grind_ring_3.lean`, but using `NoZeroNatDivisors`,
--- and which currently fail because of a kernel type mismatch.
-
--- Then final example in this file is failing with kernel deep recursion.
-
-set_option grind.warning false
-
-example {α} [CommRing α] [IsCharP α 0] [NoZeroNatDivisors α]
-    (d t : α)
-  (Δ40 : d + t + d * t = 0)
-  (Δ41 : 2 * d + 2 * d * t - 4 * d * t^2 + 2 * d * t^4 + 2 * d^2 * t^4 = 0) :
-  t + 2 * t^2 - t^3 - 2 * t^4 + t^5 = 0 := by grind +ring -- (kernel) application type mismatch
-
-example {α} [CommRing α] [IsCharP α 0] [NoZeroNatDivisors α]
-    (d t d_inv : α)
-  (Δ40 : d * (d + t + d * t) = 0)
-  (Δ41 : d^2 * (d + d * t - 2 * d * t^2 + d * t^4 + d^2 * t^4) = 0)
-  (_ : d * d_inv = 1) :
-  t + 2 * t^2 - t^3 - 2 * t^4 + t^5 = 0 := by grind +ring -- (kernel) application type mismatch
+-- Then example in this file is failing with kernel deep recursion.
 
 -- This one shouldn't succeed (it's true, but not over an arbitrary ring), but hopefully should fail cleanly.
 example {α} [CommRing α] [IsCharP α 0] (d t c : α) (d_inv PSO3_inv : α)
diff --git a/tests/lean/run/grind_ring_2.lean b/tests/lean/run/grind_ring_2.lean
index 1cdacd7602..be3a6168ca 100644
--- a/tests/lean/run/grind_ring_2.lean
+++ b/tests/lean/run/grind_ring_2.lean
@@ -126,3 +126,6 @@ example [CommRing α] (a b c : α) (f : α → Nat)
     a^3 + b^3 + c^3 = 7 →
     f (a^4 + b^4) + f (9 - c^4) ≠ 1 := by
   grind +ring
+
+example [CommRing α] [NoNatZeroDivisors α] (x y z : α) : 3*x = 1 → 3*z = 2 → 2*y = 2 → x + z + 3*y = 4 := by
+  grind +ring
diff --git a/tests/lean/run/grind_ring_4.lean b/tests/lean/run/grind_ring_4.lean
new file mode 100644
index 0000000000..704aaf35ff
--- /dev/null
+++ b/tests/lean/run/grind_ring_4.lean
@@ -0,0 +1,18 @@
+open Lean.Grind
+
+set_option grind.warning false
+
+example {α} [CommRing α] [IsCharP α 0] [NoNatZeroDivisors α]
+    (d t : α)
+  (Δ40 : d + t + d * t = 0)
+  (Δ41 : 2 * d + 2 * d * t - 4 * d * t^2 + 2 * d * t^4 + 2 * d^2 * t^4 = 0) :
+  t + 2 * t^2 - t^3 - 2 * t^4 + t^5 = 0 := by
+  grind +ring
+
+example {α} [CommRing α] [IsCharP α 0] [NoNatZeroDivisors α]
+    (d t d_inv : α)
+  (Δ40 : d * (d + t + d * t) = 0)
+  (Δ41 : d^2 * (d + d * t - 2 * d * t^2 + d * t^4 + d^2 * t^4) = 0)
+  (_ : d * d_inv = 1) :
+  t + 2 * t^2 - t^3 - 2 * t^4 + t^5 = 0 := by
+  grind +ring