def Lean.Meta.Grind.Arith.CommRing.toContextExpr : RingM Expr

Returns a context of type RArray α containing the variables of the given ring. α is the type of the ring.

def Lean.Meta.Grind.Arith.CommRing.throwNoNatZeroDivisors {α : Type} : RingM α

def Lean.Meta.Grind.Arith.CommRing.getPolyConst (p : Poly) : RingM Int

Proof term for a Nullstellensatz certificate.

structure Lean.Meta.Grind.Arith.CommRing.Null.PreNullCert : Type

A "pre" Nullstellensatz certificate. Recall that, given the hypotheses h₁ : lhs₁ = rhs₁ ... hₙ : lhsₙ = rhsₙ, a Nullstellensatz certificate is of the form

q₁*(lhs₁ - rhs₁) + ... + qₙ*(lhsₙ - rhsₙ)

Each hypothesis is an EqCnstr justified by a .core .. EqnCnstrProof. We dynamically associate them with unique indices based on the order we find them during traversal. For the other EqCnstrs we compute a "pre" certificate as a dense array containing q₁ ... qₙ needed to create the EqCnstr.

We are assuming the number of hypotheses used to derive a conclusion is small and a dense array is a reasonable representation.

• qs : Array Poly
• d : Int

  We don't use rational coefficients in the polynomials. Thus, we need to track a denominator to justify the proof step div.

instance Lean.Meta.Grind.Arith.CommRing.Null.instInhabitedPreNullCert : Inhabited PreNullCert

def Lean.Meta.Grind.Arith.CommRing.Null.PreNullCert.zero : PreNullCert

def Lean.Meta.Grind.Arith.CommRing.Null.PreNullCert.unit (i n : Nat) : PreNullCert

def Lean.Meta.Grind.Arith.CommRing.Null.PreNullCert.div (c : PreNullCert) (k : Int) : RingM PreNullCert

def Lean.Meta.Grind.Arith.CommRing.Null.PreNullCert.mul (c : PreNullCert) (k : Int) : RingM PreNullCert

def Lean.Meta.Grind.Arith.CommRing.Null.PreNullCert.combine (k₁ : Int) (m₁ : Mon) (c₁ : PreNullCert) (k₂ : Int) (m₂ : Mon) (c₂ : PreNullCert) : RingM PreNullCert

structure Lean.Meta.Grind.Arith.CommRing.Null.NullCertHypothesis : Type

• h : Expr
• lhs : RingExpr
• rhs : RingExpr

structure Lean.Meta.Grind.Arith.CommRing.Null.ProofM.State : Type

• cache : Std.HashMap UInt64 PreNullCert

  Mapping from EqCnstr to PreNullCert

• hyps : Array NullCertHypothesis

@[reducible, inline]

abbrev Lean.Meta.Grind.Arith.CommRing.Null.ProofM (α : Type) : Type

structure Lean.Meta.Grind.Arith.CommRing.Null.NullCertExt : Type

• d : Int
• qhs : Array (Poly × NullCertHypothesis)

partial def Lean.Meta.Grind.Arith.CommRing.EqCnstr.toPreNullCert (c : EqCnstr) : Null.ProofM Null.PreNullCert

def Lean.Meta.Grind.Arith.CommRing.PolyDerivation.toPreNullCert (d : PolyDerivation) : Null.ProofM Null.PreNullCert

def Lean.Meta.Grind.Arith.CommRing.PolyDerivation.getMultiplier (d : PolyDerivation) : Int

Returns the multiplier k for the input polynomial. See comment at PolyDerivation.step.

def Lean.Meta.Grind.Arith.CommRing.PolyDerivation.getMultiplier.go (d : PolyDerivation) (acc : Int) : Int

def Lean.Meta.Grind.Arith.CommRing.EqCnstr.mkNullCertExt (c : EqCnstr) : RingM Null.NullCertExt

def Lean.Meta.Grind.Arith.CommRing.PolyDerivation.mkNullCertExt (d : PolyDerivation) : RingM Null.NullCertExt

def Lean.Meta.Grind.Arith.CommRing.DiseqCnstr.mkNullCertExt (c : DiseqCnstr) : RingM Null.NullCertExt

def Lean.Meta.Grind.Arith.CommRing.Null.NullCertExt.toPoly (nc : NullCertExt) : RingM Poly

def Lean.Meta.Grind.Arith.CommRing.Null.NullCertExt.check (c : EqCnstr) (nc : NullCertExt) : RingM Bool

def Lean.Meta.Grind.Arith.CommRing.Null.NullCertExt.toNullCert (nc : NullCertExt) : Grind.CommRing.NullCert

@[irreducible]

def Lean.Meta.Grind.Arith.CommRing.Null.NullCertExt.toNullCert.go (nc : NullCertExt) (i : Nat) (acc : Grind.CommRing.NullCert) (h : i ≤ nc.qhs.size) : Grind.CommRing.NullCert

def Lean.Meta.Grind.Arith.CommRing.Null.NullCertExt.applyEqs (pr : Expr) (nc : NullCertExt) : Expr

Given a pr, returns pr h₁ ... hₙ, where n is size nc.qhs.size, and hᵢs are the equalities in the certificate.

@[irreducible]

def Lean.Meta.Grind.Arith.CommRing.Null.NullCertExt.applyEqs.go (nc : NullCertExt) (i : Nat) (pr : Expr) : Expr

def Lean.Meta.Grind.Arith.CommRing.Null.setEqUnsat (c : EqCnstr) : RingM Unit

def Lean.Meta.Grind.Arith.CommRing.Null.setDiseqUnsat (c : DiseqCnstr) : RingM Unit

def Lean.Meta.Grind.Arith.CommRing.Null.propagateEq (a b : Expr) (ra rb : RingExpr) (d : PolyDerivation) : RingM Unit

Alternative proof term construction where we generate a sub-term for each step in the derivation.

structure Lean.Meta.Grind.Arith.CommRing.Stepwise.ProofM.State : Type

• cache : Std.HashMap UInt64 Expr
• polyMap : Std.HashMap Poly Expr
• monMap : Std.HashMap Mon Expr
• exprMap : Std.HashMap RingExpr Expr

structure Lean.Meta.Grind.Arith.CommRing.Stepwise.ProofM.Context : Type

• ctx : Expr

@[reducible, inline]

abbrev Lean.Meta.Grind.Arith.CommRing.Stepwise.ProofM (α : Type) : Type

def Lean.Meta.Grind.Arith.CommRing.Stepwise.mkPolyDecl (p : Poly) : ProofM Expr

def Lean.Meta.Grind.Arith.CommRing.Stepwise.mkExprDecl (e : RingExpr) : ProofM Expr

def Lean.Meta.Grind.Arith.CommRing.Stepwise.mkMonDecl (m : Mon) : ProofM Expr

partial def Lean.Meta.Grind.Arith.CommRing.EqCnstr.toExprProof (c : EqCnstr) : Stepwise.ProofM Expr

def Lean.Meta.Grind.Arith.CommRing.Stepwise.setEqUnsat (c : EqCnstr) : RingM Unit

def Lean.Meta.Grind.Arith.CommRing.Stepwise.setDiseqUnsat (c : DiseqCnstr) : RingM Unit

def Lean.Meta.Grind.Arith.CommRing.Stepwise.propagateEq (a b : Expr) (ra rb : RingExpr) (d : PolyDerivation) : RingM Unit

def Lean.Meta.Grind.Arith.CommRing.EqCnstr.setUnsat (c : EqCnstr) : RingM Unit

def Lean.Meta.Grind.Arith.CommRing.DiseqCnstr.setUnsat (c : DiseqCnstr) : RingM Unit

def Lean.Meta.Grind.Arith.CommRing.propagateEq (a b : Expr) (ra rb : RingExpr) (d : PolyDerivation) : RingM Unit