Frontend to the `omega` tactic. #

a Problem representing the integer linear constraints extracted so far, and their proofs
the unprocessed facts : List Expr taken from the local context,
the unprocessed disjunctions : List Expr, which will only be split one at a time if we can't otherwise find a contradiction.

We begin with facts := ← getLocalHyps and problem := .trivial, and progressively process the facts.

As we process the facts, we may generate additional facts (e.g. about coercions and integer divisions). To avoid duplicates, we maintain a HashSet of previously processed facts.

problem : Problem
An integer linear arithmetic problem.
facts : List Expr
Pending facts which have not been processed yet.
disjunctions : List Expr
Pending disjunctions, which we will case split one at a time if we can't get a contradiction.
processedFacts : Std.HashSet Expr
Facts which have already been processed; we keep these to avoid duplicates.

Instances For

source

def Lean.Elab.Tactic.Omega.mkEvalRflProof (e : Expr) (lc : Omega.LinearCombo) :

OmegaM Expr

Construct the rfl proof that lc.eval atoms = e.

Equations

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

Instances For

source

def Lean.Elab.Tactic.Omega.mkCoordinateEvalAtomsEq (e : Expr) (n : Nat) :

OmegaM Expr

If e : Expr is the n-th atom, construct the proof that e = (coordinate n).eval atoms.

Equations

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

Instances For

source

def Lean.Elab.Tactic.Omega.mkAtomLinearCombo (e : Expr) :

OmegaM (Omega.LinearCombo × OmegaM Expr × Std.HashSet Expr)

Construct the linear combination (and its associated proof and new facts) for an atom.

Equations

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

Instances For

source

partial def Lean.Elab.Tactic.Omega.asLinearCombo (e : Expr) :

OmegaM (Omega.LinearCombo × OmegaM Expr × Std.HashSet Expr)

Wrapper for asLinearComboImpl, using a cache for previously visited expressions.

Gives a small (10%) speedup in testing. I tried using a pointer based cache, but there was never enough subexpression sharing to make it effective.

source

partial def Lean.Elab.Tactic.Omega.asLinearComboImpl (e : Expr) :

OmegaM (Omega.LinearCombo × OmegaM Expr × Std.HashSet Expr)

Translates an expression into a LinearCombo. Also returns:

a proof that this linear combo evaluated at the atoms is equal to the original expression
a list of new facts which should be recorded:
- for each new atom a of the form ((x : Nat) : Int), the fact that 0 ≤ a
- for each new atom a of the form x / k, for k a positive numeral, the facts that k * a ≤ x < (k + 1) * a
- for each new atom of the form ((a - b : Nat) : Int), the fact: b ≤ a ∧ ((a - b : Nat) : Int) = a - b ∨ a < b ∧ ((a - b : Nat) : Int) = 0

We also transform the expression as we descend into it:

pushing coercions: ↑(x + y), ↑(x * y), ↑(x / k), ↑(x % k), ↑k
unfolding emod: x % k → x - x / k

source

partial def Lean.Elab.Tactic.Omega.asLinearComboImpl.rewrite (lhs rw : Expr) :

OmegaM (Omega.LinearCombo × OmegaM Expr × Std.HashSet Expr)

Apply a rewrite rule to an expression, and interpret the result as a LinearCombo. (We're not rewriting any subexpressions here, just the top level, for efficiency.)

source

partial def Lean.Elab.Tactic.Omega.asLinearComboImpl.handleNatCast (e i n : Expr) :

OmegaM (Omega.LinearCombo × OmegaM Expr × Std.HashSet Expr)

source

partial def Lean.Elab.Tactic.Omega.asLinearComboImpl.handleFinVal (e i n x : Expr) :

OmegaM (Omega.LinearCombo × OmegaM Expr × Std.HashSet Expr)

source

def Lean.Elab.Tactic.Omega.MetaProblem.trivial :

MetaProblem

The trivial MetaProblem, with no facts to process and a trivial Problem.

Equations

Lean.Elab.Tactic.Omega.MetaProblem.trivial = { }

Instances For

source

instance Lean.Elab.Tactic.Omega.MetaProblem.instInhabited :

Inhabited MetaProblem

Equations

Lean.Elab.Tactic.Omega.MetaProblem.instInhabited = { default := Lean.Elab.Tactic.Omega.MetaProblem.trivial }

source

def Lean.Elab.Tactic.Omega.MetaProblem.addIntEquality (p : MetaProblem) (h x : Expr) :

OmegaM MetaProblem

Add an integer equality to the Problem.

We solve equalities as they are discovered, as this often results in an earlier contradiction.

Equations

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

Instances For

source

def Lean.Elab.Tactic.Omega.MetaProblem.addIntInequality (p : MetaProblem) (h y : Expr) :

OmegaM MetaProblem

Add an integer inequality to the Problem.

We solve equalities as they are discovered, as this often results in an earlier contradiction.

Equations

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

Instances For

source

def Lean.Elab.Tactic.Omega.MetaProblem.pushNot (h P : Expr) :

MetaM (Option Expr)

Given a fact h with type ¬ P, return a more useful fact obtained by pushing the negation.

Equations

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

Instances For

source

partial def Lean.Elab.Tactic.Omega.MetaProblem.addFact (p : MetaProblem) (h : Expr) :

OmegaM (MetaProblem × Nat)

Parse an Expr and extract facts, also returning the number of new facts found.

source

partial def Lean.Elab.Tactic.Omega.MetaProblem.processFacts (p : MetaProblem) :

OmegaM (MetaProblem × Nat)

Process all the facts in a MetaProblem, returning the new problem, and the number of new facts.

This is partial because new facts may be generated along the way.

source

def Lean.Elab.Tactic.Omega.formatErrorMessage (p : Problem) :

OmegaM MessageData

Helpful error message when omega cannot find a solution

Equations

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

Instances For

source

def Lean.Elab.Tactic.Omega.formatErrorMessage.varNameOf (i : Nat) :

String

Equations

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

Instances For

source

def Lean.Elab.Tactic.Omega.formatErrorMessage.inScope (s : String) :

MetaM Bool

Equations

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

Instances For

source

def Lean.Elab.Tactic.Omega.formatErrorMessage.varNames (mask : Array Bool) :

MetaM (Array String)

Equations

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

Instances For

source

def Lean.Elab.Tactic.Omega.formatErrorMessage.prettyConstraints (names : Array String) (constraints : Std.HashMap Omega.Coeffs Fact) :

String

Equations

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

Instances For

source

def Lean.Elab.Tactic.Omega.formatErrorMessage.prettyConstraint (e : String) :

Omega.Constraint → String

Equations

One or more equations did not get rendered due to their size.
Lean.Elab.Tactic.Omega.formatErrorMessage.prettyConstraint e { lowerBound := none, upperBound := none } = toString "" ++ toString e ++ toString " is unconstrained"
Lean.Elab.Tactic.Omega.formatErrorMessage.prettyConstraint e { lowerBound := none, upperBound := some y } = toString "" ++ toString e ++ toString " ≤ " ++ toString y ++ toString ""
Lean.Elab.Tactic.Omega.formatErrorMessage.prettyConstraint e { lowerBound := some x_1, upperBound := none } = toString "" ++ toString e ++ toString " ≥ " ++ toString x_1 ++ toString ""

Instances For

source

def Lean.Elab.Tactic.Omega.formatErrorMessage.prettyCoeffs (names : Array String) (coeffs : Omega.Coeffs) :

String

Equations

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

Instances For

source

def Lean.Elab.Tactic.Omega.formatErrorMessage.mentioned (atoms : Array Expr) (constraints : Std.HashMap Omega.Coeffs Fact) :

MetaM (Array Bool)

Equations

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

Instances For

source

def Lean.Elab.Tactic.Omega.formatErrorMessage.prettyAtoms (names : Array String) (atoms : Array Expr) (mask : Array Bool) :

MessageData

Equations

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

Instances For

source

partial def Lean.Elab.Tactic.Omega.splitDisjunction (m : MetaProblem) :

OmegaM Expr

Split a disjunction in a MetaProblem, and if we find a new usable fact call omegaImpl in both branches.

source

partial def Lean.Elab.Tactic.Omega.omegaImpl (m : MetaProblem) :

OmegaM Expr

Implementation of the omega algorithm, and handling disjunctions.

source

def Lean.Elab.Tactic.Omega.omega (facts : List Expr) (g : MVarId) (cfg : Meta.Omega.OmegaConfig := { }) :

MetaM Unit

Given a collection of facts, try prove False using the omega algorithm, and close the goal using that.

Equations

Lean.Elab.Tactic.Omega.omega facts g cfg = g.withContext do let prf ← (Lean.Elab.Tactic.Omega.omegaImpl { facts := facts }).run cfg g.assign prf

Instances For

source

def Lean.Elab.Tactic.Omega.omegaTactic (cfg : Meta.Omega.OmegaConfig) :

TacticM Unit

The omega tactic, for resolving integer and natural linear arithmetic problems.

Equations

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

Instances For

source

def Lean.Elab.Tactic.Omega.omegaDefault :

TacticM Unit

The omega tactic, for resolving integer and natural linear arithmetic problems. This TacticM Unit frontend with default configuration can be used as an Aesop rule, for example via the tactic call aesop (add 50% tactic Lean.Elab.Tactic.Omega.omegaDefault).

Equations