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

source
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

Instances For

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

Instances For

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

Instances For

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

Instances For

source
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 edge `u --(k') --> v` s.t. `k ≤ k'`

Equations

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

Instances For

source
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 edge `v --(k') --> u` s.t. `k+k' < 0`

Equations

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

Instances For