427e3bcdbc
This PR adds a `ringMaxDegree` configuration option (default `1024`) that bounds the maximum degree of polynomials processed by the `grind` ring solver. Equality constraints whose polynomial exceeds this threshold are discarded (with an issue reported once per goal), preventing pathological degree explosion on inputs such as `r ^ (2 ^ 250 - 1)`. This PR also introduces `Poly.simpM?`, a monadic version of `Poly.simp?` built on the existing safe arithmetic primitives (`mulMonM`, `combineM`, `mulConstM`) in `Grind.Arith.CommRing.SafePoly`. The previous reflection-oriented `Poly.simp?` in `Sym.Arith.Poly` lacked the abort mechanisms needed during proof search, so the simplification path used by `EqCnstr` now goes through the safe variant. A regression test `tests/elab/grind_ring_degree_explosion.lean` ensures `grind` fails quickly on high-degree problems.
46 lines
1.6 KiB
Text
46 lines
1.6 KiB
Text
module
|
|
import Lean.Meta.Sym.Arith.Poly
|
|
open Lean.Grind.CommRing
|
|
|
|
def w : Expr := .var 0
|
|
def x : Expr := .var 1
|
|
def y : Expr := .var 2
|
|
def z : Expr := .var 3
|
|
|
|
instance : Add Expr where
|
|
add a b := .add a b
|
|
instance : Sub Expr where
|
|
sub a b := .sub a b
|
|
instance : Neg Expr where
|
|
neg a := .neg a
|
|
instance : Mul Expr where
|
|
mul a b := .mul a b
|
|
instance : HPow Expr Nat Expr where
|
|
hPow a k := .pow a k
|
|
instance : OfNat Expr n where
|
|
ofNat := .num n
|
|
|
|
def spol' (p₁ p₂ : Poly) : Poly :=
|
|
p₁.spol p₂ |>.spol
|
|
|
|
def check_spoly (e₁ e₂ r : Expr) : Bool :=
|
|
let p₁ := e₁.toPoly
|
|
let p₂ := e₂.toPoly
|
|
let r := r.toPoly
|
|
let s := p₁.spol p₂
|
|
spol' p₁ p₂ == r &&
|
|
spol' p₂ p₁ == r.mulConst (-1) &&
|
|
s.spol == r &&
|
|
r == (p₁.mulMon s.k₁ s.m₁).combine (p₂.mulMon s.k₂ s.m₂)
|
|
|
|
example : check_spoly (y^2 - x + 1) (x*y - 1 + y) (-x^2 + y + x - y^2) := by native_decide
|
|
example : check_spoly (y - z + 1) (x*y - 1) (-x*z + 1 + x) := by native_decide
|
|
example : check_spoly (z^3 - x*y) (z*y - 1) (z^2 - x*y^2) := by native_decide
|
|
example : check_spoly (x + 1) (z + 1) (z - x) := by native_decide
|
|
example : check_spoly (w^2*x - y) (w*x^2 - z) (-y*x + z*w) := by native_decide
|
|
example : check_spoly (2*z^3 - x*y) (3*z*y - 1) (2*z^2 - 3*x*y^2) := by native_decide
|
|
example : check_spoly (2*x + 3) (3*z + 1) (9*z - 2*x) := by native_decide
|
|
|
|
example : check_spoly (2*y^2 - x + 1) (2*x*y - 1 + y) (-x^2 + y + x - y^2) := by native_decide
|
|
example : check_spoly (2*y^2 - x + 1) (4*x*y - 1 + y) (-2*x^2 + y + 2*x - y^2) := by native_decide
|
|
example : check_spoly (6*y^2 - x + 1) (4*x*y - 1 + y) (-2*x^2 + 3*y + 2*x - 3*y^2) := by native_decide
|