Frontend to the omega tactic.

See Std.Tactic.Omega for an overview of the tactic.

structure Std.Tactic.Omega.MetaProblem : Type

A partially processed omega context.

We have:

• 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 : Std.Tactic.Omega.Problem

  An integer linear arithmetic problem.

• facts : List Lean.Expr

  Pending facts which have not been processed yet.

• disjunctions : List Lean.Expr

  Pending disjunctions, which we will case split one at a time if we can't get a contradiction.

• processedFacts : Lean.HashSet Lean.Expr

  Facts which have already been processed; we keep these to avoid duplicates.

def Std.Tactic.Omega.mkEqReflWithExpectedType (a : Lean.Expr) (b : Lean.Expr) : Lean.MetaM Lean.Expr

Construct the term with type hint (Eq.refl a : a = b)

Equations

• Std.Tactic.Omega.mkEqReflWithExpectedType a b = do let __do_lift ← Lean.Meta.mkEqRefl a let __do_lift_1 ← Lean.Meta.mkEq a b Lean.Meta.mkExpectedTypeHint __do_lift __do_lift_1

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

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

Equations

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

def Std.Tactic.Omega.mkCoordinateEvalAtomsEq (e : Lean.Expr) (n : Nat) : Std.Tactic.Omega.OmegaM Lean.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.

def Std.Tactic.Omega.mkAtomLinearCombo (e : Lean.Expr) : Std.Tactic.Omega.OmegaM (Std.Tactic.Omega.LinearCombo × Std.Tactic.Omega.OmegaM Lean.Expr × Lean.HashSet Lean.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.

partial def Std.Tactic.Omega.asLinearCombo (e : Lean.Expr) : Std.Tactic.Omega.OmegaM (Std.Tactic.Omega.LinearCombo × Std.Tactic.Omega.OmegaM Lean.Expr × Lean.HashSet Lean.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.

partial def Std.Tactic.Omega.asLinearComboImpl (e : Lean.Expr) : Std.Tactic.Omega.OmegaM (Std.Tactic.Omega.LinearCombo × Std.Tactic.Omega.OmegaM Lean.Expr × Lean.HashSet Lean.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

partial def Std.Tactic.Omega.asLinearComboImpl.rewrite (lhs : Lean.Expr) (rw : Lean.Expr) : Std.Tactic.Omega.OmegaM (Std.Tactic.Omega.LinearCombo × Std.Tactic.Omega.OmegaM Lean.Expr × Lean.HashSet Lean.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.)

def Std.Tactic.Omega.MetaProblem.trivial : Std.Tactic.Omega.MetaProblem

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

Equations

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

instance Std.Tactic.Omega.MetaProblem.instInhabitedMetaProblem : Inhabited Std.Tactic.Omega.MetaProblem

Equations

• Std.Tactic.Omega.MetaProblem.instInhabitedMetaProblem = { default := Std.Tactic.Omega.MetaProblem.trivial }

def Std.Tactic.Omega.MetaProblem.addIntEquality (p : Std.Tactic.Omega.MetaProblem) (h : Lean.Expr) (x : Lean.Expr) : Std.Tactic.Omega.OmegaM Std.Tactic.Omega.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.

def Std.Tactic.Omega.MetaProblem.addIntInequality (p : Std.Tactic.Omega.MetaProblem) (h : Lean.Expr) (y : Lean.Expr) : Std.Tactic.Omega.OmegaM Std.Tactic.Omega.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.

def Std.Tactic.Omega.MetaProblem.pushNot (h : Lean.Expr) (P : Lean.Expr) : Lean.MetaM (Option Lean.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.

partial def Std.Tactic.Omega.MetaProblem.addFact (p : Std.Tactic.Omega.MetaProblem) (h : Lean.Expr) : Std.Tactic.Omega.OmegaM (Std.Tactic.Omega.MetaProblem × Nat)

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

partial def Std.Tactic.Omega.MetaProblem.processFacts (p : Std.Tactic.Omega.MetaProblem) : Std.Tactic.Omega.OmegaM (Std.Tactic.Omega.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.

def Std.Tactic.Omega.cases₂ (mvarId : Lean.MVarId) (p : Lean.Expr) (hName : optParam Lean.Name `h) : Lean.MetaM ((Lean.MVarId × Lean.FVarId) × Lean.MVarId × Lean.FVarId)

Given p : P ∨ Q (or any inductive type with two one-argument constructors), split the goal into two subgoals: one containing the hypothesis h : P and another containing h : Q.

Equations

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

partial def Std.Tactic.Omega.splitDisjunction (m : Std.Tactic.Omega.MetaProblem) (g : Lean.MVarId) : Std.Tactic.Omega.OmegaM Unit

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

partial def Std.Tactic.Omega.omegaImpl (m : Std.Tactic.Omega.MetaProblem) (g : Lean.MVarId) : Std.Tactic.Omega.OmegaM Unit

Implementation of the omega algorithm, and handling disjunctions.

def Std.Tactic.Omega.omega (facts : List Lean.Expr) (g : Lean.MVarId) (cfg : optParam Std.Tactic.Omega.OmegaConfig { splitDisjunctions := true, splitNatSub := true, splitNatAbs := true }) : Lean.MetaM Unit

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

Equations

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

def Std.Tactic.Omega.omegaTactic (cfg : Std.Tactic.Omega.OmegaConfig) : Lean.Elab.Tactic.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.

def Std.Tactic.Omega.omegaDefault : Lean.Elab.Tactic.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 Std.Tactic.Omega.omegaDefault).

Equations

• Std.Tactic.Omega.omegaDefault = Std.Tactic.Omega.omegaTactic { splitDisjunctions := true, splitNatSub := true, splitNatAbs := true }

def Std.Tactic.Omega.omegaSyntax : Lean.ParserDescr

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

It is not yet a full decision procedure (no "dark" or "grey" shadows), but should be effective on many problems.

We handle hypotheses of the form x = y, x < y, x ≤ y, and k ∣ x for x y in Nat or Int (and k a literal), along with negations of these statements.

We decompose the sides of the inequalities as linear combinations of atoms.

If we encounter x / k or x % k for literal integers k we introduce new auxiliary variables and the relevant inequalities.

On the first pass, we do not perform case splits on natural subtraction. If omega fails, we recursively perform a case split on a natural subtraction appearing in a hypothesis, and try again.

The options

omega (config := { splitDisjunctions := true, splitNatSub := true, splitNatAbs := true})

can be used to:

• splitDisjunctions: split any disjunctions found in the context, if the problem is not otherwise solvable.
• splitNatSub: for each appearance of ((a - b : Nat) : Int), split on a ≤ b if necessary.
• splitNatAbs: for each appearance of Int.natAbs a, split on 0 ≤ a if necessary. Currently, all of these are on by default.

Equations

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