fix: grind ring approximation (#14390)

This PR fixes an issue in the `grind` ring solver. When a ring `R` does
not satisfy `[NoNatZeroDivisors R]`, polynomial simplification could
lose information, affecting completeness.

This PR may increase memory consumption for examples that relied on this
approximation. If this becomes a performance issue in practice, we can
add a flag to control whether the approximation is used.

Here is the example that exposed the issue:

```lean
open Lean.Grind

example {R : Type u} [CommRing R] (A B : R) (H₀ : B ^ 2 = 0) (H : A * B = -2) :
    B + A * B = B - 2 := by
  grind
```

Author: leodemoura

src/Lean/Meta/Tactic/Grind/Arith/CommRing/EqCnstr.lean

@@ -156,8 +156,30 @@ def EqCnstr.simplifyUsingNumEq0 (c : EqCnstr) : RingM EqCnstr := do
   let .num k := c'.p | return c
   return { c with p := c.p.normEq0 k.natAbs, h := .numEq0 k.natAbs c' c }
 
-/-- Simplify the given equation constraint using the current basis. -/
-def EqCnstr.simplify (c : EqCnstr) : RingM EqCnstr := do
+/--
+Simplify the given equation constraint using the current basis.
+
+**Note**: This function (and `simplifyBasis`) runs with `checkCoeffDvd := true`. It rewrites a
+monomial `k'*m'` using an equation with leading term `k*m` only if `k ∣ k'` (or the ring
+implements `NoNatZeroDivisors`). Rewriting without this restriction requires multiplying the
+equation by `k/gcd k k' ≠ ±1` first, and *replacing* an equation with the result loses
+information: `p = 0` cannot be recovered from `(k/gcd k k') * p = 0` in an arbitrary
+commutative ring. The consequences of the skipped rewrites are not lost: a skipped rewrite at
+the leading monomial coincides with the S-polynomial computed by `superposeWith`, so it is
+derived non-destructively. The price is that the basis is not
+fully interreduced (e.g., `2*x = 0` and `3*x = 0` may coexist), and reduction is an incomplete
+ideal-membership test in rings without `NoNatZeroDivisors` (e.g., `x = 0` is not derived from
+`2*x = 0` and `3*x = 0`). The complete alternative is a strong Gröbner basis over `Int`
+(Kandri-Rody & Kapur): replace multiply-through rewriting with Euclidean remainder reduction
+on coefficients (`k' = q*k + r`, so the equation is never multiplied by a constant), and
+additionally superpose gcd-polynomials (Bézout combinations producing `gcd k k'` times the lcm
+of the leading monomials). We should consider this option in the future.
+
+**Note**: If using `withCheckCoeffDvd` becomes too expensive when one does not have
+`NoNatZeroDivisors`, we will add a flag to perform the simplification anyway even if
+information is lost.
+-/
+def EqCnstr.simplify (c : EqCnstr) : RingM EqCnstr := withCheckCoeffDvd do
   let mut c := c
   repeat
     c ← simplifyUsingNumEq0 c
@@ -186,6 +208,14 @@ def EqCnstr.checkConstant (c : EqCnstr) : RingM Bool := do
     if let some c' := (← getCommRing).numEq0? then
       let .num m := c'.p | unreachable!
       let (g, a, b) := gcdExt n m
+      if g == m then
+        /-
+        `n` is a multiple of the current `numEq0`; the new constraint is redundant.
+        We must not set `numEq0Updated` here: superposition may keep regenerating the
+        same constant, and requeueing the basis each time would loop until `maxSteps`.
+        -/
+        trace_goal[grind.ring.assert.trivial] "{← c.denoteExpr}"
+        return true
       c := { c with p := .num g, h := .gcd a b c c' }
     modifyCommRing fun s => { s with numEq0? := some c, numEq0Updated := true }
     trace_goal[grind.ring.assert.store] "{← c.denoteExpr}"
@@ -220,6 +250,12 @@ def addToBasisCore (c : EqCnstr) : RingM Unit := do
 
 def EqCnstr.addToQueue (c : EqCnstr) : RingM Unit := do
   if (← checkMaxSteps) then return ()
+  /-
+  Superposition may produce constant polynomials since the basis is not fully
+  interreduced (see **Note** at `EqCnstr.simplify`). `checkConstant` processes them
+  immediately; the queue must not contain constant polynomials.
+  -/
+  if (← c.checkConstant) then return ()
   trace_goal[grind.ring.assert.queue] "{← c.denoteExpr}"
   if (← checkMaxDegree c.p) then return () -- discard
   modifyCommRing fun s => { s with queue := s.queue.insert c }
@@ -265,7 +301,13 @@ def EqCnstr.toMonic (c : EqCnstr) : RingM EqCnstr := do
     return { c with p := c.p.mulConst (-1), h := .mul (-1) c }
   return c
 
-def EqCnstr.simplifyBasis (c : EqCnstr) : RingM Unit := do
+/--
+Simplifies the basis using `c`. Every equation that `c` rewrites is removed from the basis
+and requeued in its rewritten form.
+
+See **Note** at `EqCnstr.simplify` for why `checkCoeffDvd` must be enabled here.
+-/
+def EqCnstr.simplifyBasis (c : EqCnstr) : RingM Unit := withCheckCoeffDvd do
   trace[grind.debug.ring.simpBasis] "using: {← c.denoteExpr}"
   let .add _ m _ := c.p | return ()
   let rec go (basis : List EqCnstr) (acc : List EqCnstr) : RingM (List EqCnstr) := do
@@ -275,11 +317,20 @@ def EqCnstr.simplifyBasis (c : EqCnstr) : RingM Unit := do
       match c'.p with
       | .add _ m' _ =>
         if m.divides m' then
-          let c'' ← c'.simplifyWithExhaustively c
-          trace[grind.debug.ring.simpBasis] "simplified: {← c''.denoteExpr}"
-          unless (← checkConstant c'') do
-            addToQueue c''
-          go basis acc
+          /-
+          **Note**: Only the first `simplifyWithCore` step is inspected because it decides basis
+          membership: if it returns `none` (the leading monomial divides, but the rewrite is blocked by
+          the `checkCoeffDvd` restriction), `c'` must remain in the basis untouched.
+          -/
+          if let some c'' ← c'.simplifyWithCore c then
+            let c'' ← c''.simplifyWithExhaustively c
+            trace[grind.debug.ring.simpBasis] "simplified: {← c''.denoteExpr}"
+            unless (← checkConstant c'') do
+              addToQueue c''
+            go basis acc
+          else
+            -- The rewrite was skipped because of the `checkCoeffDvd` restriction. Keep `c'`.
+            go basis (c' :: acc)
         else
           go basis (c' :: acc)
       | _ => go basis (c' :: acc)

src/Lean/Meta/Tactic/Grind/Arith/CommRing/RingM.lean

@@ -39,6 +39,11 @@ structure RingM.Context where
   the simplification anyway, we may end up with a proof that `k * q = 0`, but
   we cannot deduce `q = 0` since the ring does not implement `NoNatZeroDivisors`
   See comment at `PolyDerivation`.
+
+  We also need it when destructively simplifying equations, i.e., when *replacing* an
+  equation with its simplified form (`EqCnstr.simplify` and `EqCnstr.simplifyBasis`):
+  the rewrite multiplies the equation by `k₁ = k/gcd k k'`, and the result is weaker than
+  the original equation when `k₁ ≠ ±1`. See **Note** at `EqCnstr.simplify`.
   -/
   checkCoeffDvd : Bool := false
 

src/Lean/Meta/Tactic/Grind/Arith/CommRing/SafePoly.lean

@@ -156,14 +156,20 @@ Simplifies polynomial `p₁` using polynomial `p₂` by rewriting.
 
 This function attempts to rewrite `p₁` by eliminating the first occurrence of
 the leading monomial of `p₂`.
+
+If `checkCoeffDvd` is `true` (and the ring does not implement `NoNatZeroDivisors`),
+a monomial is rewritten only if its coefficient is divisible by the leading
+coefficient of `p₂`, i.e., only if the rewrite does not multiply `p₁` by a
+constant `k₁ ≠ ±1`. See `RingM.Context.checkCoeffDvd`.
 -/
 def _root_.Lean.Grind.CommRing.Poly.simpM? (p₁ p₂ : Poly) : RingM (Option SimpResult) := do
   match p₂ with
   | .add k₂' m₂ p₂ =>
+    let checkCoeff := (← checkCoeffDvd) && !(← noZeroDivisors)
     let rec go? (p₁ : Poly) : RingM (Option SimpResult) := do
       match p₁ with
       | .add k₁' m₁ p₁ =>
-        if m₂.divides m₁ then
+        if m₂.divides m₁ && (!checkCoeff || k₂' ∣ k₁') then
           let m₂ := m₁.div m₂
           let g  := Nat.gcd k₁'.natAbs k₂'.natAbs
           let k₁ := k₂'/g

tests/elab/grind_ring_2.lean

@@ -1,6 +1,7 @@
 -- In this file we use the `grobner` frontend for `grind`.
 module
 set_option grind.debug true
+set_option warn.sorry false
 open Lean.Grind
 
 example [CommRing α] [NoNatZeroDivisors α] (x y : α) : 3*x = 1 → 3*y = 2 → x + y = 1 := by
@@ -70,6 +71,10 @@ example [CommRing α] (a b c : α)
 /--
 trace: [grind.ring.assert.basis] a + b + c + -3 = 0
 [grind.ring.assert.basis] 2 * b ^ 2 + 2 * (b * c) + 2 * c ^ 2 + -6 * b + -6 * c + 4 = 0
+[grind.ring.assert.basis] 3 * (b ^ 2 * c) + 3 * (b * c ^ 2) + -9 * b ^ 2 + -18 * (b * c) + -9 * c ^ 2 + 27 * b +
+          27 * c +
+        -20 =
+      0
 [grind.ring.assert.basis] 6 * c ^ 3 + -18 * c ^ 2 + 12 * c + 4 = 0
 -/
 #guard_msgs (trace) in
@@ -128,7 +133,7 @@ example (a b c : Int) (f : Int → Nat)
     a^2 + b^2 + c^2 = 5 →
     a^3 + b^3 + c^3 = 7 →
     f (a^4 + b^4) + f (9 - c^4) ≠ 1 := by
-  cutsat +ring
+  lia +ring
 
 example [CommRing α] [NoNatZeroDivisors α] (a b c : α) (f : α → Nat)
   : a + b + c = 3 →
@@ -167,7 +172,7 @@ example (x y : Fin 3) (h : x = y) : ((x + y) ^ 3 : Fin 3) = - x^3 := by grobner
 -- Verify that `cutsat` is disabled when calling `grobner` directly.
 example (x : Nat) : x % 2 = 0 ∨ x % 2 = 1 := by
   fail_if_success grobner
-  cutsat
+  lia
 
 -- Verify that `grobner` will not perform case splits unless explicitly asked for.
 example (x : Int) (h : x^2 = 0) : (if x > 0 then x else x)^3 = 0 := by

tests/elab/grind_ring_2.lean.out.expected

@@ -0,0 +1,36 @@
+module
+
+/-!
+Tests that the `grind` ring solver does not lose basis equations to destructive
+pseudo-reduction. Rewriting an equation with a rule whose leading coefficient does not
+divide the target coefficient multiplies the equation by a constant `k ≠ ±1`; replacing
+the original equation with the result loses information in rings without
+`NoNatZeroDivisors`. For example, below, the basis contains `B ^ 2 = 0` and `B * A + 2 = 0`,
+superposition derives `2 * B = 0`, and inserting the latter into the basis used to destroy
+both original equations (`B ^ 2 = 0` became `0 = 0` and `B * A + 2 = 0` became `4 = 0`),
+making the goal, which follows from `H` alone, unprovable.
+-/
+
+open Lean.Grind
+
+-- Basis interreduction path (`EqCnstr.simplifyBasis`): `2 * B = 0` is derived by
+-- superposition and used to be applied destructively to the rest of the basis.
+example {R : Type u} [CommRing R] (A B : R) (H₀ : B ^ 2 = 0) (H : A * B = -2) :
+    B + A * B = B - 2 := by
+  grind
+
+-- Assertion path (`EqCnstr.simplify`): with `2 * B = 0` already in the basis,
+-- `A * B = -2` used to be destroyed while being simplified during assertion.
+example {R : Type u} [CommRing R] (A B : R) (H₀ : 2 * B = 0) (H : A * B = -2) :
+    B + A * B = B - 2 := by
+  grind
+
+-- With `NoNatZeroDivisors` the rewrites are information-preserving and this always worked.
+example {R : Type u} [CommRing R] [NoNatZeroDivisors R] (A B : R)
+    (H₀ : B ^ 2 = 0) (H : A * B = -2) : B + A * B = B - 2 := by
+  grind
+
+-- The consequences of the skipped rewrites must still be derived via superposition:
+-- here `4 = 0` follows from the hypotheses, which is absurd in `Int`.
+example (A B : Int) (H₀ : B ^ 2 = 0) (H : A * B = -2) : False := by
+  grind

tests/elab/grind_ring_coeff_dvd.lean

@@ -34,6 +34,8 @@ example [CommSemiring α] [AddRightCancel α] [IsCharP α 0] (x y : α) : x^2*y
 trace: [grind.ring.assert.basis] ↑x + ↑y + -2 = 0
 [grind.ring.assert.basis] ↑y ^ 3 + -4 * ↑y ^ 2 + 4 * ↑y + -1 = 0
 [grind.ring.assert.basis] 2 * ↑y ^ 2 + -3 * ↑y + 1 = 0
+[grind.ring.assert.basis] ↑y ^ 3 + -2 * ↑y + 1 = 0
+[grind.ring.assert.basis] 3 * ↑y ^ 2 + -5 * ↑y + 2 = 0
 [grind.ring.assert.basis] ↑y + -1 = 0
 -/
 #guard_msgs (drop error, trace) in