From 460b3c3e43fd8056d58eb6cf62d204fcde231d91 Mon Sep 17 00:00:00 2001
From: Kim Morrison <477956+kim-em@users.noreply.github.com>
Date: Mon, 5 Jan 2026 13:14:35 +1000
Subject: [PATCH] fix: grind propagates `0 * a = 0` for CommSemiring (#11881)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This PR fixes an issue where `grind` failed to prove `f ≠ 0` from `f * r
≠ 0` when using `Lean.Grind.CommSemiring`, but succeeded with
`Lean.Grind.Semiring`.

The `propagateMul` propagator handles `0 * a = 0` and `a * 0 = 0` rules
for semirings that don't have full ring support in grind. Previously,
`CommSemiring` was excluded because it uses a ring envelope for
normalization, but that approach doesn't propagate these equalities back
to the original terms. Now `CommSemiring` also uses `propagateMul`.

Reported as
https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Grind.20failure.20for.20CommSemiring.2C.20not.20Semiring

🤖 Prepared with Claude Code

---------

Co-authored-by: Claude Opus 4.5 <noreply@anthropic.com>
---
 .../Meta/Tactic/Grind/Arith/Propagate.lean    |  7 +++-
 tests/lean/run/grind_commsemiring.lean        | 35 +++++++++++++++++++
 2 files changed, 41 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/run/grind_commsemiring.lean

diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Propagate.lean b/src/Lean/Meta/Tactic/Grind/Arith/Propagate.lean
index 00a7f62138..5678875312 100644
--- a/src/Lean/Meta/Tactic/Grind/Arith/Propagate.lean
+++ b/src/Lean/Meta/Tactic/Grind/Arith/Propagate.lean
@@ -82,7 +82,12 @@ See comment at `propagateMul`.
 private def isUnsupportedSemiring? (type : Expr) : GoalM (Option Expr) := do
   if isSupportedSemiringQuick type then return none
   if (← getCommRingId? type).isSome then return none
-  if (← getCommSemiringId? type).isSome then return none
+  if let some id ← getCommSemiringId? type then
+    -- CommSemiring also needs `propagateMul` because the ring envelope approach
+    -- does not propagate `0 * a = 0` back to original terms.
+    -- In the future, we want to add support for propagating equalities when the
+    -- `CommSemiring` implements `AddRightCancel`.
+    return some (← SemiringM.run id (return (← getSemiring).semiringInst))
   if let some id ← getNonCommRingId? type then
     let inst ← NonCommRingM.run id do return (← getRing).semiringInst
     return some inst
diff --git a/tests/lean/run/grind_commsemiring.lean b/tests/lean/run/grind_commsemiring.lean
new file mode 100644
index 0000000000..5d2633f2e8
--- /dev/null
+++ b/tests/lean/run/grind_commsemiring.lean
@@ -0,0 +1,35 @@
+/-!
+# Tests for grind with CommSemiring
+
+These tests verify that grind properly propagates `0 * a = 0` and `a * 0 = 0`
+for CommSemiring types, not just Semiring types.
+
+See: https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Grind.20failure.20for.20CommSemiring.2C.20not.20Semiring
+-/
+
+-- Basic test with Semiring
+example {R : Type} [Lean.Grind.Semiring R] (f r : R) (hg : f * r ≠ 0) :
+    f ≠ 0 := by
+  grind
+
+-- Same test should also work with CommSemiring
+example {R : Type} [Lean.Grind.CommSemiring R] (f r : R) (hg : f * r ≠ 0) :
+    f ≠ 0 := by
+  grind
+
+-- Symmetric case: r * f ≠ 0 implies f ≠ 0
+example {R : Type} [Lean.Grind.CommSemiring R] (f r : R) (hg : r * f ≠ 0) :
+    f ≠ 0 := by
+  grind
+
+-- Both factors must be nonzero
+example {R : Type} [Lean.Grind.CommSemiring R] (f r : R) (hg : f * r ≠ 0) :
+    f ≠ 0 ∧ r ≠ 0 := by
+  grind
+
+-- mul_one and one_mul propagation
+example {R : Type} [Lean.Grind.CommSemiring R] (f g : R) (h1 : 1 * f = g) (h2 : g ≠ f) : False := by
+  grind
+
+example {R : Type} [Lean.Grind.CommSemiring R] (f g : R) (h1 : f * 1 = g) (h2 : g ≠ f) : False := by
+  grind