Lean.Meta.Tactic.Grind.Arith.Offset.Main

This module implements a decision procedure for offset constraints of the form:

x + k ≤ y
x ≤ y + k

where k is a numeral. Each constraint is represented as an edge in a weighted graph. The constraint x + k ≤ y is represented as a negative edge. The shortest path between two nodes in the graph corresponds to an implied inequality. When adding a new edge, the state is considered unsatisfiable if the new edge creates a negative cycle. An incremental Floyd-Warshall algorithm is used to find the shortest paths between all nodes. This module can also handle offset equalities of the form x + k = y by representing them with two edges:

x + k ≤ y
y ≤ x + k

The main advantage of this module over a full linear integer arithmetic procedure is its ability to efficiently detect all implied equalities and inequalities.

source

def Lean.Meta.Grind.Arith.Offset.get' :

GoalM State

Equations

Lean.Meta.Grind.Arith.Offset.get' = do let __do_lift ← get pure __do_lift.arith.offset

source

@[inline]

def Lean.Meta.Grind.Arith.Offset.modify' (f : State → State) :

GoalM Unit

Equations

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

source

def Lean.Meta.Grind.Arith.Offset.mkNode (expr : Expr) :

GoalM NodeId

Equations

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

source

def Lean.Meta.Grind.Arith.Offset.Cnstr.toExpr (c : Cnstr NodeId) :

GoalM Expr

Equations

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

source

def Lean.Meta.Grind.Arith.Offset.checkInvariants :

GoalM Unit

Equations

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

source

def Lean.Meta.Grind.Arith.Offset.addEdge (u v : NodeId) (k : Int) (p : Expr) :

GoalM Unit

Adds an edge u --(k) --> v justified by the proof term p, and then if no negative cycle was created, updates the shortest distance of affected node pairs.

Equations