source
instance Lean.Elab.Tactic.Omega.instToExprLinearCombo :
ToExpr Omega.LinearCombo
Equations

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

source
instance Lean.Elab.Tactic.Omega.instToExprConstraint :
ToExpr Omega.Constraint
Equations

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

source
@[reducible, inline]
abbrev Lean.Elab.Tactic.Omega.Proof :
Type

A delayed proof that a constraint is satisfied at the atoms.

Equations

- Lean.Elab.Tactic.Omega.Proof = Lean.Elab.Tactic.Omega.OmegaM Lean.Expr

Instances For

source
inductive Lean.Elab.Tactic.Omega.Justification :
Omega.Constraint → Omega.Coeffs → Type

Our internal representation of an argument "justifying" that a constraint holds on some coefficients. We'll use this to construct the proof term once a contradiction is found.

- assumption (s : Omega.Constraint) (x : Omega.Coeffs) (i : Nat) : Justification s x

  `Problem.assumptions[i]` generates a proof that `s.sat' coeffs atoms`

- tidy {s : Omega.Constraint} {c : Omega.Coeffs} (j : Justification s c) : Justification (Omega.tidyConstraint s c) (Omega.tidyCoeffs s c)

  The result of `tidy` on another `Justification`.

- combine {s t : Omega.Constraint} {c : Omega.Coeffs} (j : Justification s c) (k : Justification t c) : Justification (s.combine t) c

  The result of `combine` on two `Justifications`.

- combo {s t : Omega.Constraint} {x y : Omega.Coeffs} (a : Int) (j : Justification s x) (b : Int) (k : Justification t y) : Justification (Omega.Constraint.combo a s b t) (Omega.Coeffs.combo a x b y)

  A linear `combo` of two `Justifications`.

- bmod (m : Nat) (r : Int) (i : Nat) {x : Omega.Coeffs} (j : Justification (Omega.Constraint.exact r) x) : Justification (Omega.Constraint.exact (r.bmod m)) (Omega.bmod_coeffs m i x)

  The justification for the constraint constructed using "balanced mod" while eliminating an equality.

Instances For

source
def Lean.Elab.Tactic.Omega.Justification.tidy? {s : Omega.Constraint} {c : Omega.Coeffs} (j : Justification s c) :
Option ((s' : Omega.Constraint) × (c' : Omega.Coeffs) × Justification s' c')

Wrapping for `Justification.tidy` when `tidy?` is nonempty.

Equations

- j.tidy? = match Lean.Omega.tidy? (s, c) with | some val => some ⟨Lean.Omega.tidyConstraint s c, ⟨Lean.Omega.tidyCoeffs s c, j.tidy⟩⟩ | none => none

Instances For

source
def Lean.Elab.Tactic.Omega.Justification.toString {s : Omega.Constraint} {x : Omega.Coeffs} :
Justification s x → String

Print a `Justification` as an indented tree structure.

Equations

- One or more equations did not get rendered due to their size.
- (Lean.Elab.Tactic.Omega.Justification.assumption s x i).toString = toString x ++ toString " ∈ " ++ toString s ++ toString ": assumption " ++ toString i

Instances For

source
instance Lean.Elab.Tactic.Omega.Justification.instToString {s : Omega.Constraint} {x : Omega.Coeffs} :
ToString (Justification s x)
Equations

- Lean.Elab.Tactic.Omega.Justification.instToString = { toString := Lean.Elab.Tactic.Omega.Justification.toString }

source
def Lean.Elab.Tactic.Omega.Justification.tidyProof (s : Omega.Constraint) (x : Omega.Coeffs) (v prf : Expr) :
Expr

Construct the proof term associated to a `tidy` step.

Equations

- Lean.Elab.Tactic.Omega.Justification.tidyProof s x v prf = Lean.mkApp4 (Lean.Expr.const `Lean.Omega.tidy_sat []) (Lean.toExpr s) (Lean.toExpr x) v prf

Instances For

source
def Lean.Elab.Tactic.Omega.Justification.combineProof (s t : Omega.Constraint) (x : Omega.Coeffs) (v ps pt : Expr) :
Expr

Construct the proof term associated to a `combine` step.

Equations

- Lean.Elab.Tactic.Omega.Justification.combineProof s t x v ps pt = Lean.mkApp6 (Lean.Expr.const `Lean.Omega.Constraint.combine_sat' []) (Lean.toExpr s) (Lean.toExpr t) (Lean.toExpr x) v ps pt

Instances For

source
def Lean.Elab.Tactic.Omega.Justification.comboProof (s t : Omega.Constraint) (a : Int) (x : Omega.Coeffs) (b : Int) (y : Omega.Coeffs) (v px py : Expr) :
Expr

Construct the proof term associated to a `combo` step.

Equations

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

Instances For

source
def Lean.Elab.Tactic.Omega.Justification.bmodProof (m : Nat) (r : Int) (i : Nat) (x : Omega.Coeffs) (v w : Expr) :
MetaM Expr

Construct the proof term associated to a `bmod` step.

Equations

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

Instances For

source
def Lean.Elab.Tactic.Omega.Justification.proof {s : Omega.Constraint} {c : Omega.Coeffs} (v : Expr) (assumptions : Array Proof) :
Justification s c → Proof

Constructs a proof that `s.sat' c v = true`

Equations

- One or more equations did not get rendered due to their size.
- Lean.Elab.Tactic.Omega.Justification.proof v assumptions (Lean.Elab.Tactic.Omega.Justification.assumption s c i) = assumptions[i]!

Instances For

source
structure Lean.Elab.Tactic.Omega.Fact :
Type

A `Justification` bundled together with its parameters.

- coeffs : Omega.Coeffs

  The coefficients of a constraint.

- constraint : Omega.Constraint

  The constraint.

- justification : Justification self.constraint self.coeffs

  The justification of a derived fact.

Instances For

source
instance Lean.Elab.Tactic.Omega.Fact.instToString :
ToString Fact
Equations

- Lean.Elab.Tactic.Omega.Fact.instToString = { toString := fun (f : Lean.Elab.Tactic.Omega.Fact) => toString f.justification }

source
def Lean.Elab.Tactic.Omega.Fact.tidy (f : Fact) :
Fact

`tidy`, implemented on `Fact`.

Equations

- f.tidy = match f.justification.tidy? with | some ⟨constraint, ⟨coeffs, justification⟩⟩ => { coeffs := coeffs, constraint := constraint, justification := justification } | none => f

Instances For

source
def Lean.Elab.Tactic.Omega.Fact.combo (a : Int) (f : Fact) (b : Int) (g : Fact) :
Fact

`combo`, implemented on `Fact`.

Equations

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

Instances For

source
structure Lean.Elab.Tactic.Omega.Problem :
Type

A `omega` problem.

This is a hybrid structure: it contains both `Expr` objects giving proofs of the "ground" assumptions (or rather continuations which will produce the proofs when needed) and internal representations of the linear constraints that we manipulate in the algorithm.

While the algorithm is running we do not synthesize any new `Expr` proofs: proof extraction happens only once we've found a contradiction.

- assumptions : Array Proof

  The ground assumptions that the algorithm starts from.

- numVars : Nat

  The number of variables in the problem.

- constraints : Std.HashMap Omega.Coeffs Fact

  The current constraints, indexed by their coefficients.

- equalities : Std.HashSet Omega.Coeffs

  The coefficients for which `constraints` contains an exact constraint (i.e. an equality).

- eliminations : List (Fact × Nat × Int)

  Equations that have already been used to eliminate variables, along with the variable which was removed, and its coefficient (either `1` or `-1`). The earlier elements are more recent, so if these are being reapplied it is essential to use `List.foldr`.

- possible : Bool

  Whether the problem is possible.

- proveFalse? : Option Proof

  If the problem is impossible, then `proveFalse?` will contain a proof of `False`.

- proveFalse?_spec : (self.possible || self.proveFalse?.isSome) = true

  Invariant between `possible` and `proveFalse?`.

- explanation? : Thunk String

  If we have found a contradiction, `explanation?` will contain a human readable account of the derivation.

Instances For

source
def Lean.Elab.Tactic.Omega.Problem.isEmpty (p : Problem) :
Bool

Check if a problem has no constraints.

Equations

- p.isEmpty = p.constraints.isEmpty

Instances For

source
instance Lean.Elab.Tactic.Omega.Problem.instToString :
ToString Problem
Equations

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

source
def Lean.Elab.Tactic.Omega.Problem.proveFalse {s : Omega.Constraint} {x : Omega.Coeffs} (j : Justification s x) (assumptions : Array Proof) :
Proof

Takes a proof that `s.sat' x v` for some `s` such that `s.isImpossible`, and constructs a proof of `False`.

Equations

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

Instances For

source
def Lean.Elab.Tactic.Omega.Problem.insertConstraint (p : Problem) :
Fact → Problem

Insert a constraint into the problem, without checking if there is already a constraint for these coefficients.

Equations

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

Instances For

source
def Lean.Elab.Tactic.Omega.Problem.addConstraint (p : Problem) :
Fact → Problem

Add a constraint into the problem, combining it with any existing constraints for the same coefficients.

Equations

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

Instances For

source
def Lean.Elab.Tactic.Omega.Problem.selectEquality (p : Problem) :
Option (Omega.Coeffs × Nat)

Walk through the equalities, finding either the first equality with minimal coefficient `±1`, or otherwise the equality with minimal `(r.minNatAbs, r.maxNatAbs)` (ordered lexicographically).

Returns the coefficients of the equality, along with the value of `minNatAbs`.

Although we don't need to run a termination proof here, it's nevertheless important that we use this ordering so the algorithm terminates in practice!

Equations

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

Instances For

source
def Lean.Elab.Tactic.Omega.Problem.replayEliminations (p : Problem) (f : Fact) :
Fact

If we have already solved some equalities, apply those to some new `Fact`.

Equations

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

Instances For

source
def Lean.Elab.Tactic.Omega.Problem.solveEasyEquality (p : Problem) (c : Omega.Coeffs) :
Problem

Solve an "easy" equality, i.e. one with a coefficient that is `±1`.

After solving, the variable will have been eliminated from all constraints.

Equations

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

Instances For

source
def Lean.Elab.Tactic.Omega.Problem.dealWithHardEquality (p : Problem) (c : Omega.Coeffs) :
OmegaM Problem

We deal with a hard equality by introducing a new easy equality.

After solving the easy equality, the minimum lexicographic value of `(c.minNatAbs, c.maxNatAbs)` will have been reduced.

Equations

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

Instances For

source
def Lean.Elab.Tactic.Omega.Problem.solveEquality (p : Problem) (c : Omega.Coeffs) (m : Nat) :
OmegaM Problem

Solve an equality, by deciding whether it is easy (has a `±1` coefficient) or hard, and delegating to the appropriate function.

Equations

- p.solveEquality c m = if m = 1 then pure (p.solveEasyEquality c) else p.dealWithHardEquality c

Instances For

source
partial def Lean.Elab.Tactic.Omega.Problem.solveEqualities (p : Problem) :
OmegaM Problem

Recursively solve all equalities.

source
def Lean.Elab.Tactic.Omega.Problem.addInequality_proof (c : Int) (x : Omega.Coeffs) (p : Proof) :
Proof

Constructing the proof term for `addInequality`.

Equations

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

Instances For

source
def Lean.Elab.Tactic.Omega.Problem.addEquality_proof (c : Int) (x : Omega.Coeffs) (p : Proof) :
Proof

Constructing the proof term for `addEquality`.

Equations

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

Instances For

source
def Lean.Elab.Tactic.Omega.Problem.addInequality (p : Problem) (const : Int) (coeffs : Omega.Coeffs) (prf? : Option Proof) :
Problem

Helper function for adding an inequality of the form `const + Coeffs.dot coeffs atoms ≥ 0` to a `Problem`.

(This is only used while initializing a `Problem`. During elimination we use `addConstraint`.)

Equations

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

Instances For

source
def Lean.Elab.Tactic.Omega.Problem.addEquality (p : Problem) (const : Int) (coeffs : Omega.Coeffs) (prf? : Option Proof) :
Problem

Helper function for adding an equality of the form `const + Coeffs.dot coeffs atoms = 0` to a `Problem`.

(This is only used while initializing a `Problem`. During elimination we use `addConstraint`.)

Equations

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

Instances For

source
def Lean.Elab.Tactic.Omega.Problem.addInequalities (p : Problem) (ineqs : List (Int × Omega.Coeffs × Option Proof)) :
Problem

Folding `addInequality` over a list.

Equations

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

Instances For

source
def Lean.Elab.Tactic.Omega.Problem.addEqualities (p : Problem) (eqs : List (Int × Omega.Coeffs × Option Proof)) :
Problem

Folding `addEquality` over a list.

Equations

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

Instances For

source
structure Lean.Elab.Tactic.Omega.Problem.FourierMotzkinData :
Type

Representation of the data required to run Fourier-Motzkin elimination on a variable.

- var : Nat

  Which variable is being eliminated.

- irrelevant : List Fact

  The "irrelevant" facts which do not involve the target variable.

- lowerBounds : List (Fact × Int)

  The facts which give a lower bound on the target variable, and the coefficient of the target variable in each.

- upperBounds : List (Fact × Int)

  The facts which give an upper bound on the target variable, and the coefficient of the target variable in each.

- lowerExact : Bool

  Whether the elimination would be exact, because all of the lower bound coefficients are `±1`.

- upperExact : Bool

  Whether the elimination would be exact, because all of the upper bound coefficients are `±1`.

Instances For

source
instance Lean.Elab.Tactic.Omega.Problem.instInhabitedFourierMotzkinData :
Inhabited FourierMotzkinData
Equations

- Lean.Elab.Tactic.Omega.Problem.instInhabitedFourierMotzkinData = { default := Lean.Elab.Tactic.Omega.Problem.instInhabitedFourierMotzkinData.default }

source
def Lean.Elab.Tactic.Omega.Problem.instInhabitedFourierMotzkinData.default :
FourierMotzkinData
Equations

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

Instances For

source
instance Lean.Elab.Tactic.Omega.Problem.instToStringFourierMotzkinData :
ToString FourierMotzkinData
Equations

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

source
def Lean.Elab.Tactic.Omega.Problem.FourierMotzkinData.isEmpty (d : FourierMotzkinData) :
Bool

Is a Fourier-Motzkin elimination empty (i.e. there are no relevant constraints).

Equations

- d.isEmpty = (d.lowerBounds.isEmpty && d.upperBounds.isEmpty)

Instances For

source
def Lean.Elab.Tactic.Omega.Problem.FourierMotzkinData.size (d : FourierMotzkinData) :
Nat

The number of new constraints that would be introduced by Fourier-Motzkin elimination.

Equations

- d.size = d.lowerBounds.length * d.upperBounds.length

Instances For

source
def Lean.Elab.Tactic.Omega.Problem.FourierMotzkinData.exact (d : FourierMotzkinData) :
Bool

Is the Fourier-Motzkin elimination known to be exact?

Equations

- d.exact = (d.lowerExact || d.upperExact)

Instances For

source
def Lean.Elab.Tactic.Omega.Problem.fourierMotzkinData (p : Problem) :
Array FourierMotzkinData

Prepare the Fourier-Motzkin elimination data for each variable.

Equations

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

Instances For

source
def Lean.Elab.Tactic.Omega.Problem.fourierMotzkinSelect (data : Array FourierMotzkinData) :
MetaM FourierMotzkinData

Decides which variable to run Fourier-Motzkin elimination on, and returns the associated data.

We prefer eliminations which introduce no new inequalities, or otherwise exact eliminations, and break ties by the number of new inequalities introduced.

Equations

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

Instances For

source
def Lean.Elab.Tactic.Omega.Problem.fourierMotzkin (p : Problem) :
MetaM Problem

Run Fourier-Motzkin elimination on one variable.

Equations

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

Instances For

source
partial def Lean.Elab.Tactic.Omega.Problem.runOmega (p : Problem) :
OmegaM Problem

Run the `omega` algorithm (for now without dark and grey shadows!) on a problem.

source
partial def Lean.Elab.Tactic.Omega.Problem.elimination (p : Problem) :
OmegaM Problem

As for `runOmega`, but assuming the first round of solving equalities has already happened.