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.

Equations

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

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

Equations

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

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

Equations

• One or more equations did not get rendered due to their size.
• Lean.Meta.Grind.Arith.CommRing.getPolyConst (Lean.Grind.CommRing.Poly.num k) = pure k

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

Equations

• Lean.Meta.Grind.Arith.CommRing.Null.instInhabitedPreNullCert = { default := { qs := default, d := default } }

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

Equations

• Lean.Meta.Grind.Arith.CommRing.Null.PreNullCert.zero = { qs := #[] }

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

Equations

• Lean.Meta.Grind.Arith.CommRing.Null.PreNullCert.unit i n = { qs := (Array.replicate n (Lean.Grind.CommRing.Poly.num 0)).set! i (Lean.Grind.CommRing.Poly.num 1) }

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

Equations

• c.div k = pure { qs := c.qs, d := c.d * k }

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

Equations

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

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

Equations

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

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

Equations

• Lean.Meta.Grind.Arith.CommRing.Null.ProofM = StateRefT' IO.RealWorld Lean.Meta.Grind.Arith.CommRing.Null.ProofM.State Lean.Meta.Grind.Arith.CommRing.RingM

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

Equations

• One or more equations did not get rendered due to their size.
• (Lean.Meta.Grind.Arith.CommRing.PolyDerivation.input p).toPreNullCert = pure Lean.Meta.Grind.Arith.CommRing.Null.PreNullCert.zero

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

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

Equations

• d.getMultiplier = Lean.Meta.Grind.Arith.CommRing.PolyDerivation.getMultiplier.go d 1

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

Equations

• One or more equations did not get rendered due to their size.
• Lean.Meta.Grind.Arith.CommRing.PolyDerivation.getMultiplier.go (Lean.Meta.Grind.Arith.CommRing.PolyDerivation.input p) acc = acc

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

Equations

• c.mkNullCertExt = do let __discr ← StateRefT'.run c.toPreNullCert { } match __discr with | (nc, s) => pure { d := nc.d, qhs := nc.qs.zip s.hyps }

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

Equations

• d.mkNullCertExt = do let __discr ← StateRefT'.run d.toPreNullCert { } match __discr with | (nc, s) => pure { d := nc.d, qhs := nc.qs.zip s.hyps }

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

Equations

• c.mkNullCertExt = c.d.mkNullCertExt

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

Equations

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

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

Equations

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

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

Equations

• nc.toNullCert = Lean.Meta.Grind.Arith.CommRing.Null.NullCertExt.toNullCert.go nc nc.qhs.size Lean.Grind.CommRing.NullCert.empty ⋯

@[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

Equations

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

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.

Equations

• Lean.Meta.Grind.Arith.CommRing.Null.NullCertExt.applyEqs pr nc = Lean.Meta.Grind.Arith.CommRing.Null.NullCertExt.applyEqs.go nc 0 pr

@[irreducible]

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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