@[inline, reducible]

abbrev Std.Tactic.Omega.Proof : Type

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

Equations

• Std.Tactic.Omega.Proof = Std.Tactic.Omega.OmegaM Lean.Expr

def Std.Tactic.Omega.normalize? : Std.Tactic.Omega.Constraint × Std.Tactic.Omega.Coeffs → Option (Std.Tactic.Omega.Constraint × Std.Tactic.Omega.Coeffs)

Normalize a constraint, by dividing through by the GCD.

Return none if there is nothing to do, to avoid adding unnecessary steps to the proof term.

Equations

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

def Std.Tactic.Omega.normalize (p : Std.Tactic.Omega.Constraint × Std.Tactic.Omega.Coeffs) : Std.Tactic.Omega.Constraint × Std.Tactic.Omega.Coeffs

Normalize a constraint, by dividing through by the GCD.

Equations

• Std.Tactic.Omega.normalize p = Option.getD (Std.Tactic.Omega.normalize? p) p

@[inline, reducible]

noncomputable abbrev Std.Tactic.Omega.normalizeConstraint (s : Std.Tactic.Omega.Constraint) (x : Std.Tactic.Omega.Coeffs) : Std.Tactic.Omega.Constraint

Shorthand for the first component of normalize.

Equations

• Std.Tactic.Omega.normalizeConstraint s x = (Std.Tactic.Omega.normalize (s, x)).fst

@[inline, reducible]

noncomputable abbrev Std.Tactic.Omega.normalizeCoeffs (s : Std.Tactic.Omega.Constraint) (x : Std.Tactic.Omega.Coeffs) : Std.Tactic.Omega.Coeffs

Shorthand for the second component of normalize.

Equations

• Std.Tactic.Omega.normalizeCoeffs s x = (Std.Tactic.Omega.normalize (s, x)).snd

theorem Std.Tactic.Omega.normalize?_eq_some {s : Std.Tactic.Omega.Constraint} {x : Std.Tactic.Omega.Coeffs} {s' : Std.Tactic.Omega.Constraint} {x' : Std.Tactic.Omega.Coeffs} (w : Std.Tactic.Omega.normalize? (s, x) = some (s', x')) : Std.Tactic.Omega.normalizeConstraint s x = s' ∧ Std.Tactic.Omega.normalizeCoeffs s x = x'

theorem Std.Tactic.Omega.normalize_sat {s : Std.Tactic.Omega.Constraint} {x : Std.Tactic.Omega.Coeffs} {v : Std.Tactic.Omega.Coeffs} (w : Std.Tactic.Omega.Constraint.sat' s x v = true) : Std.Tactic.Omega.Constraint.sat' (Std.Tactic.Omega.normalizeConstraint s x) (Std.Tactic.Omega.normalizeCoeffs s x) v = true

def Std.Tactic.Omega.positivize? : Std.Tactic.Omega.Constraint × Std.Tactic.Omega.Coeffs → Option (Std.Tactic.Omega.Constraint × Std.Tactic.Omega.Coeffs)

Multiply by -1 if the leading coefficient is negative, otherwise return none.

Equations

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

noncomputable def Std.Tactic.Omega.positivize (p : Std.Tactic.Omega.Constraint × Std.Tactic.Omega.Coeffs) : Std.Tactic.Omega.Constraint × Std.Tactic.Omega.Coeffs

Multiply by -1 if the leading coefficient is negative, otherwise do nothing.

Equations

• Std.Tactic.Omega.positivize p = Option.getD (Std.Tactic.Omega.positivize? p) p

@[inline, reducible]

noncomputable abbrev Std.Tactic.Omega.positivizeConstraint (s : Std.Tactic.Omega.Constraint) (x : Std.Tactic.Omega.Coeffs) : Std.Tactic.Omega.Constraint

Shorthand for the first component of positivize.

Equations

• Std.Tactic.Omega.positivizeConstraint s x = (Std.Tactic.Omega.positivize (s, x)).fst

@[inline, reducible]

noncomputable abbrev Std.Tactic.Omega.positivizeCoeffs (s : Std.Tactic.Omega.Constraint) (x : Std.Tactic.Omega.Coeffs) : Std.Tactic.Omega.Coeffs

Shorthand for the second component of positivize.

Equations

• Std.Tactic.Omega.positivizeCoeffs s x = (Std.Tactic.Omega.positivize (s, x)).snd

theorem Std.Tactic.Omega.positivize?_eq_some {s : Std.Tactic.Omega.Constraint} {x : Std.Tactic.Omega.Coeffs} {s' : Std.Tactic.Omega.Constraint} {x' : Std.Tactic.Omega.Coeffs} (w : Std.Tactic.Omega.positivize? (s, x) = some (s', x')) : Std.Tactic.Omega.positivizeConstraint s x = s' ∧ Std.Tactic.Omega.positivizeCoeffs s x = x'

theorem Std.Tactic.Omega.positivize_sat {s : Std.Tactic.Omega.Constraint} {x : Std.Tactic.Omega.Coeffs} {v : Std.Tactic.Omega.Coeffs} (w : Std.Tactic.Omega.Constraint.sat' s x v = true) : Std.Tactic.Omega.Constraint.sat' (Std.Tactic.Omega.positivizeConstraint s x) (Std.Tactic.Omega.positivizeCoeffs s x) v = true

def Std.Tactic.Omega.tidy? : Std.Tactic.Omega.Constraint × Std.Tactic.Omega.Coeffs → Option (Std.Tactic.Omega.Constraint × Std.Tactic.Omega.Coeffs)

positivize and normalize, returning none if neither does anything.

Equations

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

def Std.Tactic.Omega.tidy (p : Std.Tactic.Omega.Constraint × Std.Tactic.Omega.Coeffs) : Std.Tactic.Omega.Constraint × Std.Tactic.Omega.Coeffs

positivize and normalize

Equations

• Std.Tactic.Omega.tidy p = Option.getD (Std.Tactic.Omega.tidy? p) p

@[inline, reducible]

abbrev Std.Tactic.Omega.tidyConstraint (s : Std.Tactic.Omega.Constraint) (x : Std.Tactic.Omega.Coeffs) : Std.Tactic.Omega.Constraint

Shorthand for the first component of tidy.

Equations

• Std.Tactic.Omega.tidyConstraint s x = (Std.Tactic.Omega.tidy (s, x)).fst

@[inline, reducible]

abbrev Std.Tactic.Omega.tidyCoeffs (s : Std.Tactic.Omega.Constraint) (x : Std.Tactic.Omega.Coeffs) : Std.Tactic.Omega.Coeffs

Shorthand for the second component of tidy.

Equations

• Std.Tactic.Omega.tidyCoeffs s x = (Std.Tactic.Omega.tidy (s, x)).snd

theorem Std.Tactic.Omega.tidy_sat {s : Std.Tactic.Omega.Constraint} {x : Std.Tactic.Omega.Coeffs} {v : Std.Tactic.Omega.Coeffs} (w : Std.Tactic.Omega.Constraint.sat' s x v = true) : Std.Tactic.Omega.Constraint.sat' (Std.Tactic.Omega.tidyConstraint s x) (Std.Tactic.Omega.tidyCoeffs s x) v = true

theorem Std.Tactic.Omega.combo_sat' (s : Std.Tactic.Omega.Constraint) (t : Std.Tactic.Omega.Constraint) (a : Int) (x : Std.Tactic.Omega.Coeffs) (b : Int) (y : Std.Tactic.Omega.Coeffs) (v : Std.Tactic.Omega.Coeffs) (wx : Std.Tactic.Omega.Constraint.sat' s x v = true) (wy : Std.Tactic.Omega.Constraint.sat' t y v = true) : Std.Tactic.Omega.Constraint.sat' (Std.Tactic.Omega.Constraint.combo a s b t) (Std.Tactic.Omega.Coeffs.combo a x b y) v = true

@[inline, reducible]

abbrev Std.Tactic.Omega.bmod_div_term (m : Nat) (a : Std.Tactic.Omega.Coeffs) (b : Std.Tactic.Omega.Coeffs) : Int

The value of the new variable introduced when solving a hard equality.

Equations

• Std.Tactic.Omega.bmod_div_term m a b = Std.Tactic.Omega.Coeffs.bmod_dot_sub_dot_bmod m a b / ↑m

def Std.Tactic.Omega.bmod_coeffs (m : Nat) (i : Nat) (x : Std.Tactic.Omega.Coeffs) : Std.Tactic.Omega.Coeffs

The coefficients of the new equation generated when solving a hard equality.

Equations

• Std.Tactic.Omega.bmod_coeffs m i x = Std.Tactic.Omega.Coeffs.set (Std.Tactic.Omega.Coeffs.bmod x m) i ↑m

theorem Std.Tactic.Omega.bmod_sat (m : Nat) (r : Int) (i : Nat) (x : Std.Tactic.Omega.Coeffs) (v : Std.Tactic.Omega.Coeffs) (h : Std.Tactic.Omega.Coeffs.length x ≤ i) (p : Std.Tactic.Omega.Coeffs.get v i = Std.Tactic.Omega.bmod_div_term m x v) (w : Std.Tactic.Omega.Constraint.sat' (Std.Tactic.Omega.Constraint.exact r) x v = true) : Std.Tactic.Omega.Constraint.sat' (Std.Tactic.Omega.Constraint.exact (Int.bmod r m)) (Std.Tactic.Omega.bmod_coeffs m i x) v = true

inductive Std.Tactic.Omega.Justification : Std.Tactic.Omega.Constraint → Std.Tactic.Omega.Coeffs → Type

Our internal representation of 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 : Std.Tactic.Omega.Constraint) → (x : Std.Tactic.Omega.Coeffs) → Nat → Std.Tactic.Omega.Justification s x

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

• tidy: {s : Std.Tactic.Omega.Constraint} → {c : Std.Tactic.Omega.Coeffs} → Std.Tactic.Omega.Justification s c → Std.Tactic.Omega.Justification (Std.Tactic.Omega.tidyConstraint s c) (Std.Tactic.Omega.tidyCoeffs s c)

  The result of tidy on another Justification.

• combine: {s t : Std.Tactic.Omega.Constraint} → {c : Std.Tactic.Omega.Coeffs} → Std.Tactic.Omega.Justification s c → Std.Tactic.Omega.Justification t c → Std.Tactic.Omega.Justification (Std.Tactic.Omega.Constraint.combine s t) c

  The result of combine on two Justifications.

• combo: {s t : Std.Tactic.Omega.Constraint} → {x y : Std.Tactic.Omega.Coeffs} → (a : Int) → Std.Tactic.Omega.Justification s x → (b : Int) → Std.Tactic.Omega.Justification t y → Std.Tactic.Omega.Justification (Std.Tactic.Omega.Constraint.combo a s b t) (Std.Tactic.Omega.Coeffs.combo a x b y)

  A linear combo of two Justifications.

• bmod: (m : Nat) → (r : Int) → (i : Nat) → {x : Std.Tactic.Omega.Coeffs} → Std.Tactic.Omega.Justification (Std.Tactic.Omega.Constraint.exact r) x → Std.Tactic.Omega.Justification (Std.Tactic.Omega.Constraint.exact (Int.bmod r m)) (Std.Tactic.Omega.bmod_coeffs m i x)

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

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

Wrapping for Justification.tidy when tidy? is nonempty.

Equations

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

def Std.Tactic.Omega.Justification.toString {s : Std.Tactic.Omega.Constraint} {x : Std.Tactic.Omega.Coeffs} : Std.Tactic.Omega.Justification s x → String

Print a Justification as an indented tree structure.

instance Std.Tactic.Omega.Justification.instToStringJustification {s : Std.Tactic.Omega.Constraint} {x : Std.Tactic.Omega.Coeffs} : ToString (Std.Tactic.Omega.Justification s x)

Equations

• Std.Tactic.Omega.Justification.instToStringJustification = { toString := Std.Tactic.Omega.Justification.toString }

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

Construct the proof term associated to a tidy step.

Equations

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

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

Construct the proof term associated to a combine step.

Equations

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

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

Construct the proof term associated to a combo step.

Equations

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

def Std.Tactic.Omega.Justification.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.Justification.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.Justification.bmodProof (m : Nat) (r : Int) (i : Nat) (x : Std.Tactic.Omega.Coeffs) (v : Lean.Expr) (w : Lean.Expr) : Lean.MetaM Lean.Expr

Construct the proof term associated to a bmod step.

Equations

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

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

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

Equations

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

structure Std.Tactic.Omega.Fact : Type

A Justification bundled together with its parameters.

• coeffs : Std.Tactic.Omega.Coeffs

  The coefficients of a constraint.

• constraint : Std.Tactic.Omega.Constraint

  The constraint.

• justification : Std.Tactic.Omega.Justification s.constraint s.coeffs

  The justification of a derived fact.

instance Std.Tactic.Omega.Fact.instToStringFact : ToString Std.Tactic.Omega.Fact

Equations

• Std.Tactic.Omega.Fact.instToStringFact = { toString := fun (f : Std.Tactic.Omega.Fact) => toString f.justification }

def Std.Tactic.Omega.Fact.tidy (f : Std.Tactic.Omega.Fact) : Std.Tactic.Omega.Fact

tidy, implemented on Fact.

Equations

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

def Std.Tactic.Omega.Fact.combo (a : Int) (f : Std.Tactic.Omega.Fact) (b : Int) (g : Std.Tactic.Omega.Fact) : Std.Tactic.Omega.Fact

combo, implemented on Fact.

Equations

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

structure Std.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 Std.Tactic.Omega.Proof

  The ground assumptions that the algorithm starts from.

• numVars : Nat

  The number of variables in the problem.

• constraints : Std.HashMap Std.Tactic.Omega.Coeffs Std.Tactic.Omega.Fact

  The current constraints, indexed by their coefficients.

• equalities : Lean.HashSet Std.Tactic.Omega.Coeffs

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

• eliminations : List (Std.Tactic.Omega.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 Std.Tactic.Omega.Proof

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

• proveFalse?_spec : (s.possible || Option.isSome s.proveFalse?) = true

  Invariant between possible and proveFalse?.

• explanation? : Thunk String

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

def Std.Tactic.Omega.Problem.isEmpty (p : Std.Tactic.Omega.Problem) : Bool

Check if a problem has no constraints.

Equations

• Std.Tactic.Omega.Problem.isEmpty p = Std.HashMap.isEmpty p.constraints

instance Std.Tactic.Omega.Problem.instToStringProblem : ToString Std.Tactic.Omega.Problem

Equations

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

def Std.Tactic.Omega.Problem.proveFalse {s : Std.Tactic.Omega.Constraint} {x : Std.Tactic.Omega.Coeffs} (j : Std.Tactic.Omega.Justification s x) (assumptions : Array Std.Tactic.Omega.Proof) : Std.Tactic.Omega.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.

def Std.Tactic.Omega.Problem.insertConstraint (p : Std.Tactic.Omega.Problem) : Std.Tactic.Omega.Fact → Std.Tactic.Omega.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.

def Std.Tactic.Omega.Problem.addConstraint (p : Std.Tactic.Omega.Problem) : Std.Tactic.Omega.Fact → Std.Tactic.Omega.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.

def Std.Tactic.Omega.Problem.selectEquality (p : Std.Tactic.Omega.Problem) : Option (Std.Tactic.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.

def Std.Tactic.Omega.Problem.replayEliminations (p : Std.Tactic.Omega.Problem) (f : Std.Tactic.Omega.Fact) : Std.Tactic.Omega.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.

def Std.Tactic.Omega.Problem.solveEasyEquality (p : Std.Tactic.Omega.Problem) (c : Std.Tactic.Omega.Coeffs) : Std.Tactic.Omega.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.

def Std.Tactic.Omega.Problem.dealWithHardEquality (p : Std.Tactic.Omega.Problem) (c : Std.Tactic.Omega.Coeffs) : Std.Tactic.Omega.OmegaM Std.Tactic.Omega.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.

def Std.Tactic.Omega.Problem.solveEquality (p : Std.Tactic.Omega.Problem) (c : Std.Tactic.Omega.Coeffs) (m : Nat) : Std.Tactic.Omega.OmegaM Std.Tactic.Omega.Problem

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

Equations

• Std.Tactic.Omega.Problem.solveEquality p c m = if m = 1 then pure (Std.Tactic.Omega.Problem.solveEasyEquality p c) else Std.Tactic.Omega.Problem.dealWithHardEquality p c

partial def Std.Tactic.Omega.Problem.solveEqualities (p : Std.Tactic.Omega.Problem) : Std.Tactic.Omega.OmegaM Std.Tactic.Omega.Problem

Recursively solve all equalities.

theorem Std.Tactic.Omega.Problem.addInequality_sat {c : Int} {x : Std.Tactic.Omega.Coeffs} {y : Std.Tactic.Omega.Coeffs} (w : c + Std.Tactic.Omega.Coeffs.dot x y ≥ 0) : Std.Tactic.Omega.Constraint.sat' { lowerBound := some (-c), upperBound := none } x y = true

def Std.Tactic.Omega.Problem.addInequality_proof (c : Int) (x : Std.Tactic.Omega.Coeffs) (p : Std.Tactic.Omega.Proof) : Std.Tactic.Omega.Proof

Constructing the proof term for addInequality.

Equations

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

theorem Std.Tactic.Omega.Problem.addEquality_sat {c : Int} {x : Std.Tactic.Omega.Coeffs} {y : Std.Tactic.Omega.Coeffs} (w : c + Std.Tactic.Omega.Coeffs.dot x y = 0) : Std.Tactic.Omega.Constraint.sat' { lowerBound := some (-c), upperBound := some (-c) } x y = true

def Std.Tactic.Omega.Problem.addEquality_proof (c : Int) (x : Std.Tactic.Omega.Coeffs) (p : Std.Tactic.Omega.Proof) : Std.Tactic.Omega.Proof

Constructing the proof term for addEquality.

Equations

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

def Std.Tactic.Omega.Problem.addInequality (p : Std.Tactic.Omega.Problem) (const : Int) (coeffs : Std.Tactic.Omega.Coeffs) (prf? : Option Std.Tactic.Omega.Proof) : Std.Tactic.Omega.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.

def Std.Tactic.Omega.Problem.addEquality (p : Std.Tactic.Omega.Problem) (const : Int) (coeffs : Std.Tactic.Omega.Coeffs) (prf? : Option Std.Tactic.Omega.Proof) : Std.Tactic.Omega.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.

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

Folding addInequality over a list.

Equations

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

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

Folding addEquality over a list.

Equations

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

structure Std.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 Std.Tactic.Omega.Fact

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

• lowerBounds : List (Std.Tactic.Omega.Fact × Int)

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

• upperBounds : List (Std.Tactic.Omega.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.

instance Std.Tactic.Omega.Problem.instInhabitedFourierMotzkinData : Inhabited Std.Tactic.Omega.Problem.FourierMotzkinData

Equations

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

instance Std.Tactic.Omega.Problem.instToStringFourierMotzkinData : ToString Std.Tactic.Omega.Problem.FourierMotzkinData

Equations

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

def Std.Tactic.Omega.Problem.FourierMotzkinData.isEmpty (d : Std.Tactic.Omega.Problem.FourierMotzkinData) : Bool

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

Equations

• Std.Tactic.Omega.Problem.FourierMotzkinData.isEmpty d = (List.isEmpty d.lowerBounds && List.isEmpty d.upperBounds)

def Std.Tactic.Omega.Problem.FourierMotzkinData.size (d : Std.Tactic.Omega.Problem.FourierMotzkinData) : Nat

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

Equations

• Std.Tactic.Omega.Problem.FourierMotzkinData.size d = List.length d.lowerBounds * List.length d.upperBounds

def Std.Tactic.Omega.Problem.FourierMotzkinData.exact (d : Std.Tactic.Omega.Problem.FourierMotzkinData) : Bool

Is the Fourier-Motzkin elimination known to be exact?

Equations

• Std.Tactic.Omega.Problem.FourierMotzkinData.exact d = (d.lowerExact || d.upperExact)

def Std.Tactic.Omega.Problem.fourierMotzkinData (p : Std.Tactic.Omega.Problem) : Array Std.Tactic.Omega.Problem.FourierMotzkinData

Prepare the Fourier-Motzkin elimination data for each variable.

Equations

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

def Std.Tactic.Omega.Problem.fourierMotzkinSelect (data : Array Std.Tactic.Omega.Problem.FourierMotzkinData) : Std.Tactic.Omega.Problem.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.

def Std.Tactic.Omega.Problem.fourierMotzkin (p : Std.Tactic.Omega.Problem) : Std.Tactic.Omega.Problem

Run Fourier-Motzkin elimination on one variable.

Equations

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

partial def Std.Tactic.Omega.Problem.runOmega (p : Std.Tactic.Omega.Problem) : Std.Tactic.Omega.OmegaM Std.Tactic.Omega.Problem

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

partial def Std.Tactic.Omega.Problem.elimination (p : Std.Tactic.Omega.Problem) : Std.Tactic.Omega.OmegaM Std.Tactic.Omega.Problem

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