Helper functions for constructing proof terms in the offset constraint procedure.

def Lean.Meta.Grind.Arith.Offset.rfl_true : Expr

Returns a proof for true = true

Equations

• Lean.Meta.Grind.Arith.Offset.rfl_true = Lean.mkConst `Lean.Grind.rfl_true

def Lean.Meta.Grind.Arith.Offset.mkTrans (nodes : PArray Expr) (pi₁ pi₂ : ProofInfo) (v : NodeId) : ProofInfo

Assume pi₁ is { w := u, k := k₁, proof := p₁ } and pi₂ is { w := w, k := k₂, proof := p₂ } p₁ is the proof for edge u -(k₁) → w and p₂ the proof for edge w -(k₂)-> v. Then, this function returns a proof for edge u -(k₁+k₂) -> v.

Equations

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

def Lean.Meta.Grind.Arith.Offset.mkOfNegEqFalse (nodes : PArray Expr) (c : Cnstr NodeId) (h : Expr) : Expr

Equations

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

def Lean.Meta.Grind.Arith.Offset.mkUnsatProof (u v : Expr) (kuv : Int) (huv : Expr) (kvu : Int) (hvu : Expr) : Expr

Returns a proof of False using a negative cycle composed of

• u --(kuv)--> v with proof huv
• v --(kvu)--> u with proof hvu

Equations

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

def Lean.Meta.Grind.Arith.Offset.mkPropagateEqTrueProof (u v : Expr) (k : Int) (huv : Expr) (k' : Int) : Expr

Given a path u --(kuv)--> v justified by proof huv, construct a proof of e = True where e is a term corresponding to the edgen u --(k') --> v s.t. k ≤ k'

Equations

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

def Lean.Meta.Grind.Arith.Offset.mkPropagateEqFalseProof (u v : Expr) (k : Int) (huv : Expr) (k' : Int) : Expr

Given a path u --(kuv)--> v justified by proof huv, construct a proof of e = False where e is a term corresponding to the edgen v --(k') --> u s.t. k+k' < 0

Equations

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