From b4c4f265aade4524c885aebfc4f558583ae8daee Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 21 Mar 2026 19:52:44 -0700 Subject: [PATCH] fix: `grind` ring solver OOM on high-degree polynomials (#13032) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This PR fixes #12842 where `grind` exhausts memory on goals involving high-degree polynomials such as `(x + y)^2 = x^128 + y^2` over `Fin 2`. The root cause is that `incSteps` in the ring module's Groebner basis engine increments the step counter by 1 per simplification, regardless of polynomial size. For high-degree polynomials (e.g., degree 128), intermediate results can have hundreds of terms, making each operation extremely expensive — but the flat counter cannot catch this before memory is exhausted. The fix weights each step by `Poly.numTerms` of the result polynomial and increases the default `ringSteps` from 10 000 to 100 000 to accommodate the new cost model. Note: the example from #12842 will not be *proved* by `grind` even after this fix, because Frobenius / Fermat's little theorem (`x^p = x` in `Fin p`) is not available in core Lean. The long-term plan is to introduce a type class in core stating this property, with an instance provided by Mathlib, so that `grind` can exploit it when Mathlib is imported. Closes #12842 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 4.6 --- src/Init/Grind/Config.lean | 7 +++---- src/Lean/Meta/Tactic/Grind/Arith/CommRing/EqCnstr.lean | 4 ++-- src/Lean/Meta/Tactic/Grind/Arith/CommRing/Poly.lean | 9 +++++++++ src/Lean/Meta/Tactic/Grind/Arith/CommRing/RingM.lean | 4 ++-- 4 files changed, 16 insertions(+), 8 deletions(-) diff --git a/src/Init/Grind/Config.lean b/src/Init/Grind/Config.lean index b48070cb18..5eb9a2c636 100644 --- a/src/Init/Grind/Config.lean +++ b/src/Init/Grind/Config.lean @@ -111,11 +111,10 @@ structure Config where ring := true /-- Maximum number of steps performed by the `ring` solver. - A step is counted whenever one polynomial is used to simplify another. - For example, given `x^2 + 1` and `x^2 * y^3 + x * y`, the first can be - used to simplify the second to `-1 * y^3 + x * y`. + A step is counted whenever one polynomial is used to simplify another, + weighted by the number of terms in the resulting polynomial. -/ - ringSteps := 10000 + ringSteps := 100000 /-- When `true` (default: `true`), uses procedure for handling linear arithmetic for `IntModule`, and `CommRing`. diff --git a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/EqCnstr.lean b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/EqCnstr.lean index ffa2d1fe3c..34d7728594 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/EqCnstr.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/EqCnstr.lean @@ -109,7 +109,7 @@ def _root_.Lean.Grind.CommRing.Poly.findSimp? (p : Poly) : RingM (Option EqCnstr /-- Simplifies `d.p` using `c`, and returns an extended polynomial derivation. -/ def PolyDerivation.simplifyWith (d : PolyDerivation) (c : EqCnstr) : RingM PolyDerivation := do let some r := d.p.simp? c.p (← nonzeroChar?) | return d - incSteps + incSteps r.p.numTerms trace_goal[grind.ring.simp] "{← r.p.denoteExpr}" return .step r.p r.k₁ d r.k₂ r.m₂ c @@ -137,7 +137,7 @@ def EqCnstr.simplifyWithCore (c₁ c₂ : EqCnstr) : RingM (Option EqCnstr) := d p := r.p h := .simp r.k₁ c₁ r.k₂ r.m₂ c₂ } - incSteps + incSteps r.p.numTerms trace_goal[grind.ring.simp] "{← c.p.denoteExpr}" return some c diff --git a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Poly.lean b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Poly.lean index 9651a94161..0805cb0420 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Poly.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Poly.lean @@ -184,6 +184,15 @@ def Poly.degree : Poly → Nat | .num _ => 0 | .add _ m _ => m.degree +/-- Returns the number of monomials in the polynomial. -/ +def Poly.numTerms (p : Poly) : Nat := + go p 0 +where + go (p : Poly) (acc : Nat) : Nat := + match p with + | .num .. => acc + | .add _ _ p => go p (acc + 1) + /-- Returns `true` if the leading monomial of `p` divides `m`. -/ def Poly.divides (p : Poly) (m : Mon) : Bool := match p with diff --git a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/RingM.lean b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/RingM.lean index 06cc4fb099..1ed90897da 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/RingM.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/RingM.lean @@ -13,8 +13,8 @@ namespace Lean.Meta.Grind.Arith.CommRing def checkMaxSteps : GoalM Bool := do return (← get').steps >= (← getConfig).ringSteps -def incSteps : GoalM Unit := do - modify' fun s => { s with steps := s.steps + 1 } +def incSteps (n : Nat := 1) : GoalM Unit := do + modify' fun s => { s with steps := s.steps + n } structure RingM.Context where ringId : Nat