def Lean.Meta.Grind.Arith.Linear.toContextExpr : LinearM Expr

Returns a context of type RArray α containing the variables of the given structure, where α is (← getStruct).type.

Equations

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

def Lean.Meta.Grind.Arith.Linear.toRingContextExpr : LinearM Expr

Similar to toContextExpr, but for the CommRing module. Recall that this module interfaces with the CommRing module and their variable contexts may not be necessarily identical. For example, for this module, the term x*y does not have an interpretation and we have a "variable" representing it, but it is interpreted in the CommRing module, and such variable does not exist there. On the other direction, suppose we have the inequality z < 0, and z does not occur in any equality or disequality. Then, the CommRing does not even "see" z, and z does not occur in its context, but it occurs in the variable context created by this module.

Equations

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

structure Lean.Meta.Grind.Arith.Linear.ProofM.State : Type

• cache : Std.HashMap UInt64 Expr
• polyMap : Std.HashMap Poly Expr
• exprMap : Std.HashMap LinExpr Expr
• ringPolyMap : Std.HashMap CommRing.Poly Expr
• ringExprMap : Std.HashMap CommRing.RingExpr Expr

structure Lean.Meta.Grind.Arith.Linear.ProofM.Context : Type

• ctx : Expr
• ringCtx : Expr

@[reducible, inline]

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

Auxiliary monad for constructing linarith proofs.

Equations

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

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

Equations

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

def Lean.Meta.Grind.Arith.Linear.mkExprDecl (e : LinExpr) : ProofM Expr

Equations

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

def Lean.Meta.Grind.Arith.Linear.mkRingPolyDecl (p : CommRing.Poly) : ProofM Expr

Equations

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

def Lean.Meta.Grind.Arith.Linear.mkRingExprDecl (e : CommRing.RingExpr) : ProofM Expr

Equations

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

partial def Lean.Meta.Grind.Arith.Linear.IneqCnstr.toExprProof (c' : IneqCnstr) : ProofM Expr

partial def Lean.Meta.Grind.Arith.Linear.DiseqCnstr.toExprProof (c' : DiseqCnstr) : ProofM Expr

partial def Lean.Meta.Grind.Arith.Linear.EqCnstr.toExprProof (c' : EqCnstr) : ProofM Expr

partial def Lean.Meta.Grind.Arith.Linear.UnsatProof.toExprProofCore (h : UnsatProof) : ProofM Expr

def Lean.Meta.Grind.Arith.Linear.UnsatProof.toExprProof (h : UnsatProof) : LinearM Expr

Equations

• h.toExprProof = Lean.Meta.Grind.Arith.Linear.withProofContext✝ h.toExprProofCore

def Lean.Meta.Grind.Arith.Linear.setInconsistent (h : UnsatProof) : LinearM Unit

Equations

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

A linarith proof may depend on decision variables. We collect them and perform non chronological backtracking.

partial def Lean.Meta.Grind.Arith.Linear.IneqCnstr.collectDecVars (c' : IneqCnstr) : CollectDecVarsM Unit

partial def Lean.Meta.Grind.Arith.Linear.DiseqCnstr.collectDecVars (c' : DiseqCnstr) : CollectDecVarsM Unit

partial def Lean.Meta.Grind.Arith.Linear.EqCnstr.collectDecVars (c' : EqCnstr) : CollectDecVarsM Unit

def Lean.Meta.Grind.Arith.Linear.UnsatProof.collectDecVars (h : UnsatProof) : CollectDecVarsM Unit

Equations

• (Lean.Meta.Grind.Arith.Linear.UnsatProof.lt c).collectDecVars = c.collectDecVars
• (Lean.Meta.Grind.Arith.Linear.UnsatProof.diseq c).collectDecVars = c.collectDecVars