feat: polynomial operations with deep recursion and heartbeat checks This PR adds "safe" polynomial operations to `grind ring`. The use the usual combinators: `withIncRecDepth` and `checkSystem`.
diff --git a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Proof.lean b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Proof.lean index 441c94d..e22bdae 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Proof.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Proof.lean
@@ -9,6 +9,7 @@ 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
diff --git a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/SafePoly.lean b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/SafePoly.lean new file mode 100644 index 0000000..5a8d992 --- /dev/null +++ b/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
diff --git a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Util.lean b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Util.lean index 0972441..ed87248 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Util.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Util.lean
@@ -172,28 +172,6 @@ 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
diff --git a/tests/lean/run/grind_big_poly.lean b/tests/lean/run/grind_big_poly.lean new file mode 100644 index 0000000..f9f87e5 --- /dev/null +++ b/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