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).

Equations

• Lean.Meta.Sym.Arith.PolyM = ReaderT Lean.Meta.Sym.Arith.PolyConfig (OptionT Lean.Meta.Sym.SymM)

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

Equations

• x.run cfg = (x cfg).run

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

Equations

• Lean.Meta.Sym.Arith.SafePoly.addConst p k = do let __do_lift ← read match __do_lift.char? with | some c => pure (p.addConstC k c) | x => pure (p.addConst k)

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• Lean.Meta.Sym.Arith.SafePoly.combine p₁ p₂ = do let p ← Lean.Meta.Sym.Arith.SafePoly.combineCore✝ p₁ p₂ Lean.Meta.Sym.Arith.SafePoly.checkBudget✝ p pure p

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.

Equations

• Lean.Meta.Sym.Arith.SafePoly.mul p₁ p₂ = Lean.Meta.Sym.Arith.SafePoly.mul.go✝ p₂ p₁ (Lean.Grind.CommRing.Poly.num 0)

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

Equations

• Lean.Meta.Sym.Arith.SafePoly.pow p k = do let __do_lift ← read if __do_lift.commutative = true then Lean.Meta.Sym.Arith.SafePoly.powComm✝ p k else Lean.Meta.Sym.Arith.SafePoly.powNC✝ p k

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

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

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• Lean.Meta.Sym.Arith.SafePoly.powNode (Lean.Grind.CommRing.Expr.num n) pa k = if (k == 0) = true then pure (Lean.Grind.CommRing.Poly.num 1) else Lean.Meta.Sym.Arith.SafePoly.powNode.numPow✝ k n
• Lean.Meta.Sym.Arith.SafePoly.powNode (Lean.Grind.CommRing.Expr.intCast n) pa k = if (k == 0) = true then pure (Lean.Grind.CommRing.Poly.num 1) else Lean.Meta.Sym.Arith.SafePoly.powNode.numPow✝ k n
• Lean.Meta.Sym.Arith.SafePoly.powNode (Lean.Grind.CommRing.Expr.natCast n) pa k = if (k == 0) = true then pure (Lean.Grind.CommRing.Poly.num 1) else Lean.Meta.Sym.Arith.SafePoly.powNode.numPow✝ k ↑n
• Lean.Meta.Sym.Arith.SafePoly.powNode (Lean.Grind.CommRing.Expr.var x) pa k = if (k == 0) = true then pure (Lean.Grind.CommRing.Poly.num 1) else Lean.Meta.Sym.Arith.SafePoly.mkPowVar✝ x k
• Lean.Meta.Sym.Arith.SafePoly.powNode a pa k = if (k == 0) = true then pure (Lean.Grind.CommRing.Poly.num 1) else Lean.Meta.Sym.Arith.SafePoly.pow pa k

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.

Equations

• Lean.Meta.Sym.Arith.toPoly? e = do let __do_lift ← read if __do_lift.semiring = true then Lean.Meta.Sym.Arith.SafePoly.toPolySemiring✝ e else Lean.Meta.Sym.Arith.SafePoly.toPolyRing✝ e