feat: polynomial operations with deep recursion and heartbeat checks (#9146)

This PR adds "safe" polynomial operations to `grind ring`. The use the
usual combinators: `withIncRecDepth` and `checkSystem`.

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

@@ -9,6 +9,7 @@ import Lean.Meta.Tactic.Grind.Diseq
 import Lean.Meta.Tactic.Grind.Arith.ProofUtil
 import Lean.Meta.Tactic.Grind.Arith.CommRing.RingId
 import Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr
+import Lean.Meta.Tactic.Grind.Arith.CommRing.SafePoly
 import Lean.Meta.Tactic.Grind.Arith.CommRing.ToExpr
 
 namespace Lean.Meta.Grind.Arith.CommRing

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

@@ -0,0 +1,112 @@
+/-
+Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr
+
+namespace Lean.Meta.Grind.Arith.CommRing
+
+/-!
+The polynomial functions at `Poly.lean` are used for constructing proofs-by-reflection,
+but they do not provide mechanisms for aborting expensive computations.
+-/
+
+private def applyChar (a : Int) : RingM Int := do
+  if let some c ← nonzeroChar? then
+    return a % c
+  else
+    return a
+
+private def addConst (p : Poly) (k : Int) : RingM Poly := do
+  if let some c ← nonzeroChar? then return .addConstC p k c else return .addConst p k
+
+private def mulConst (k : Int) (p : Poly) : RingM Poly := do
+  if let some c ← nonzeroChar? then return .mulConstC k p c else return .mulConst k p
+
+private def mulMon (k : Int) (m : Mon) (p : Poly) : RingM Poly := do
+  if let some c ← nonzeroChar? then return .mulMonC k m p c else return .mulMon k m p
+
+private def combine (p₁ p₂ : Poly) : RingM Poly := withIncRecDepth do
+  match p₁, p₂ with
+  | .num k₁, .num k₂ => return .num (← applyChar (k₁ + k₂))
+  | .num k₁, .add k₂ m₂ p₂ => addConst (.add k₂ m₂ p₂) k₁
+  | .add k₁ m₁ p₁, .num k₂ => addConst (.add k₁ m₁ p₁) k₂
+  | .add k₁ m₁ p₁, .add k₂ m₂ p₂ =>
+    match m₁.grevlex m₂ with
+    | .eq =>
+      let k ← applyChar (k₁ + k₂)
+      bif k == 0 then
+        combine p₁ p₂
+      else
+        return .add k m₁ (← combine p₁ p₂)
+    | .gt => return .add k₁ m₁ (← combine p₁ (.add k₂ m₂ p₂))
+    | .lt => return .add k₂ m₂ (← combine (.add k₁ m₁ p₁) p₂)
+
+private def mul (p₁ : Poly) (p₂ : Poly) : RingM Poly :=
+  go p₁ (.num 0)
+where
+  go (p₁ : Poly) (acc : Poly) : RingM Poly :=  withIncRecDepth do
+    match p₁ with
+    | .num k => combine acc (← mulConst k p₂)
+    | .add k m p₁ =>
+      checkSystem "grind ring"
+      go p₁ (← combine acc (← mulMon k m p₂))
+
+private def pow (p : Poly) (k : Nat) : RingM Poly := withIncRecDepth do
+  match k with
+  | 0 => return .num 1
+  | 1 => return p
+  | 2 => mul p p
+  | k+3 => mul p (← pow p (k+2))
+
+private def toPoly (e : RingExpr) : RingM Poly := do
+  match e with
+  | .num n   => return .num (← applyChar n)
+  | .var x   => return .ofVar x
+  | .add a b => combine (← toPoly a) (← toPoly b)
+  | .mul a b => mul (← toPoly a) (← toPoly b)
+  | .neg a   => mulConst (-1) (← toPoly a)
+  | .sub a b => combine (← toPoly a) (← mulConst (-1) (← toPoly b))
+  | .pow a k =>
+    match a with
+    | .num n => return .num (← applyChar (n^k))
+    | .var x => return .ofMon (.mult {x, k} .unit)
+    | _ => pow (← toPoly a) k
+
+/--
+Converts the given ring expression into a multivariate polynomial.
+If the ring has a nonzero characteristic, it is used during normalization.
+-/
+abbrev _root_.Lean.Grind.CommRing.Expr.toPolyM (e : RingExpr) : RingM Poly := do
+  toPoly e
+
+abbrev _root_.Lean.Grind.CommRing.Poly.mulConstM (p : Poly) (k : Int) : RingM Poly :=
+  mulConst k p
+
+abbrev _root_.Lean.Grind.CommRing.Poly.mulMonM (p : Poly) (k : Int) (m : Mon) : RingM Poly :=
+  mulMon k m p
+
+abbrev _root_.Lean.Grind.CommRing.Poly.mulM (p₁ p₂ : Poly) : RingM Poly := do
+  mul p₁ p₂
+
+abbrev _root_.Lean.Grind.CommRing.Poly.combineM (p₁ p₂ : Poly) : RingM Poly :=
+  combine p₁ p₂
+
+def _root_.Lean.Grind.CommRing.Poly.spolM (p₁ p₂ : Poly) : RingM Grind.CommRing.SPolResult := do
+  match p₁, p₂ with
+  | .add k₁ m₁ p₁, .add k₂ m₂ p₂ =>
+    let m    := m₁.lcm m₂
+    let m₁   := m.div m₁
+    let m₂   := m.div m₂
+    let g    := Nat.gcd k₁.natAbs k₂.natAbs
+    let c₁   := k₂/g
+    let c₂   := -k₁/g
+    let p₁   ← mulMon c₁ m₁ p₁
+    let p₂   ← mulMon c₂ m₂ p₂
+    let spol ← combine p₁ p₂
+    return { spol, m₁, m₂, k₁ := c₁, k₂ := c₂ }
+  | _, _ => return {}
+
+end Lean.Meta.Grind.Arith.CommRing

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

@@ -172,28 +172,6 @@ def getCharInst : RingM (Expr × Nat) := do
 def isField : RingM Bool :=
   return (← getRing).fieldInst?.isSome
 
-/--
-Converts the given ring expression into a multivariate polynomial.
-If the ring has a nonzero characteristic, it is used during normalization.
--/
-def _root_.Lean.Grind.CommRing.Expr.toPolyM (e : RingExpr) : RingM Poly := do
-  if let some c ← nonzeroChar? then return e.toPolyC c else return e.toPoly
-
-def _root_.Lean.Grind.CommRing.Poly.mulConstM (p : Poly) (k : Int) : RingM Poly :=
-  return p.mulConst' k (← nonzeroChar?)
-
-def _root_.Lean.Grind.CommRing.Poly.mulMonM (p : Poly) (k : Int) (m : Mon) : RingM Poly :=
-  return p.mulMon' k m (← nonzeroChar?)
-
-def _root_.Lean.Grind.CommRing.Poly.mulM (p₁ p₂ : Poly) : RingM Poly := do
-  if let some c ← nonzeroChar? then return p₁.mulC p₂ c else return p₁.mul p₂
-
-def _root_.Lean.Grind.CommRing.Poly.combineM (p₁ p₂ : Poly) : RingM Poly :=
-  return p₁.combine' p₂ (← nonzeroChar?)
-
-def _root_.Lean.Grind.CommRing.Poly.spolM (p₁ p₂ : Poly) : RingM Grind.CommRing.SPolResult := do
-  if let some c ← nonzeroChar? then return p₁.spol p₂ c else return p₁.spol p₂
-
 def isQueueEmpty : RingM Bool :=
   return (← getRing).queue.isEmpty
 

tests/lean/run/grind_big_poly.lean

@@ -0,0 +1,9 @@
+/--
+trace: [grind.issues] maximum recursion depth has been reached
+    use `set_option maxRecDepth <num>` to increase limit
+    use `set_option diagnostics true` to get diagnostic information
+-/
+#guard_msgs (drop error, trace) in
+set_option trace.grind.issues true in
+example (x y z w : Int) : (x + y + z + w)^5000 - 1 = 0 := by
+  grind -- should not crash