Guarded polynomial computation

The polynomial functions in Init (Expr.toPoly, Expr.toPolyC, Expr.toPolyS, and the operations they use) are pure and unbounded. The functions below compute the same results in SymM, so that the computation can be interrupted (checkSystem, withIncRecDepth), refuses exponents above the exp threshold (checkExp), and can be bounded by a budget on the number of monomials and the degree.

They must be case-by-case mirrors of the Init functions: proofs by reflection compare the kernel's evaluation of the Init function with the result computed here, so any divergence is a proof failure.

structure Lean.Meta.Sym.Arith.PolyConfig : Type

• char? : Option Nat

  Nonzero characteristic. When some c, mirrors Expr.toPolyC c (or toPolyS, which has no characteristic support).

• semiring : Bool

  When true, mirrors Expr.toPolyS (semiring: nonnegative coefficients, no subtraction).

• commutative : Bool

  When false, mirrors the non-commutative functions (toPoly_nc, toPolyC_nc, toPolyS_nc).

• maxTerms? : Option Nat

  Maximum number of monomials of any intermediate polynomial.

• maxDegree? : Option Nat

  Maximum degree of any intermediate polynomial.

@[reducible, inline]

abbrev Lean.Meta.Sym.Arith.PolyM (α : Type) : Type

Polynomial computations that may fail (budget, exponent threshold).

def Lean.Meta.Sym.Arith.PolyM.run {α : Type} (x : PolyM α) (cfg : PolyConfig := { }) : SymM (Option α)

def Lean.Meta.Sym.Arith.SafePoly.addConst (p : Poly) (k : Int) : PolyM Poly

def Lean.Meta.Sym.Arith.SafePoly.mulConst (k : Int) (p : Poly) : PolyM Poly

def Lean.Meta.Sym.Arith.SafePoly.mulMon (k : Int) (m : Mon) (p : Poly) : PolyM Poly

def Lean.Meta.Sym.Arith.SafePoly.combine (p₁ p₂ : Poly) : PolyM Poly

Mirror of Poly.combine (Poly.combineC with a characteristic).

def Lean.Meta.Sym.Arith.SafePoly.mul (p₁ p₂ : Poly) : PolyM Poly

Mirror of Poly.mul (Poly.mulC, Poly.mul_nc, Poly.mulC_nc); mulMon selects the variant.

def Lean.Meta.Sym.Arith.SafePoly.pow (p : Poly) (k : Nat) : PolyM Poly

def Lean.Meta.Sym.Arith.SafePoly.numNode (n : Int) : PolyM Poly

Mirror of the numeral cases (.num, .natCast, .intCast) of the toPoly functions.

def Lean.Meta.Sym.Arith.SafePoly.powNode (a : RingExpr) (pa : Poly) (k : Nat) : PolyM Poly

Mirror of the .pow a k case of the toPoly functions, given pa, the polynomial of a.

def Lean.Meta.Sym.Arith.toPoly? (e : RingExpr) : PolyM Poly

Converts e into a polynomial, mirroring Expr.toPoly, Expr.toPolyC c, Expr.toPolyS, or their non-commutative variants, depending on the configuration. Returns none if the computation exceeds the budget or the exponent threshold.