A Constraint consists of an optional lower and upper bound (inclusive), constraining a value to a set of the form ∅, {x}, [x, y], [x, ∞), (-∞, y], or (-∞, ∞).

@[reducible, inline]

abbrev Lean.Omega.LowerBound : Type

An optional lower bound on a integer.

@[reducible, inline]

abbrev Lean.Omega.UpperBound : Type

An optional upper bound on a integer.

@[reducible, inline]

abbrev Lean.Omega.LowerBound.sat (b : LowerBound) (t : Int) : Bool

A lower bound at x is satisfied at t if x ≤ t.

@[reducible, inline]

abbrev Lean.Omega.UpperBound.sat (b : UpperBound) (t : Int) : Bool

A upper bound at y is satisfied at t if t ≤ y.

structure Lean.Omega.Constraint : Type

A Constraint consists of an optional lower and upper bound (inclusive), constraining a value to a set of the form ∅, {x}, [x, y], [x, ∞), (-∞, y], or (-∞, ∞).

• lowerBound : LowerBound

  A lower bound.

• upperBound : UpperBound

  An upper bound.

instance Lean.Omega.instBEqConstraint : BEq Constraint

instance Lean.Omega.instDecidableEqConstraint : DecidableEq Constraint

instance Lean.Omega.instReprConstraint : Repr Constraint

instance Lean.Omega.Constraint.instToString : ToString Constraint

def Lean.Omega.Constraint.sat (c : Constraint) (t : Int) : Bool

A constraint is satisfied at t is both the lower bound and upper bound are satisfied.

def Lean.Omega.Constraint.map (c : Constraint) (f : Int → Int) : Constraint

Apply a function to both the lower bound and upper bound.

def Lean.Omega.Constraint.translate (c : Constraint) (t : Int) : Constraint

Translate a constraint.

theorem Lean.Omega.Constraint.translate_sat {t : Int} {c : Constraint} {v : Int} : c.sat v = true → (c.translate t).sat (v + t) = true

def Lean.Omega.Constraint.flip (c : Constraint) : Constraint

Flip a constraint. This operation is not useful by itself, but is used to implement neg and scale.

def Lean.Omega.Constraint.neg (c : Constraint) : Constraint

Negate a constraint. [x, y] becomes [-y, -x].

theorem Lean.Omega.Constraint.neg_sat {c : Constraint} {v : Int} : c.sat v = true → c.neg.sat (-v) = true

def Lean.Omega.Constraint.trivial : Constraint

The trivial constraint, satisfied everywhere.

def Lean.Omega.Constraint.impossible : Constraint

The impossible constraint, unsatisfiable.

def Lean.Omega.Constraint.exact (r : Int) : Constraint

An exact constraint.

@[simp]

theorem Lean.Omega.Constraint.trivial_say {t : Int} : trivial.sat t = true

@[simp]

theorem Lean.Omega.Constraint.exact_sat (r t : Int) : (exact r).sat t = decide (r = t)

def Lean.Omega.Constraint.isImpossible : Constraint → Bool

Check if a constraint is unsatisfiable.

def Lean.Omega.Constraint.isExact : Constraint → Bool

Check if a constraint requires an exact value.

theorem Lean.Omega.Constraint.not_sat_of_isImpossible {c : Constraint} (h : c.isImpossible = true) {t : Int} : ¬c.sat t = true

def Lean.Omega.Constraint.scale (k : Int) (c : Constraint) : Constraint

Scale a constraint by multiplying by an integer.

• If k = 0 this is either impossible, if the original constraint was impossible, or the = 0 exact constraint.
• If k is positive this takes [x, y] to [k * x, k * y]
• If k is negative this takes [x, y] to [k * y, k * x].

theorem Lean.Omega.Constraint.scale_sat {t : Int} {c : Constraint} (k : Int) (w : c.sat t = true) : (scale k c).sat (k * t) = true

def Lean.Omega.Constraint.add (x y : Constraint) : Constraint

The sum of two constraints. [a, b] + [c, d] = [a + c, b + d].

theorem Lean.Omega.Constraint.add_sat {c₁ c₂ : Constraint} {x₁ x₂ : Int} (w₁ : c₁.sat x₁ = true) (w₂ : c₂.sat x₂ = true) : (c₁.add c₂).sat (x₁ + x₂) = true

def Lean.Omega.Constraint.combo (a : Int) (x : Constraint) (b : Int) (y : Constraint) : Constraint

A linear combination of two constraints.

theorem Lean.Omega.Constraint.combo_sat {c₁ c₂ : Constraint} {x₁ x₂ : Int} (a : Int) (w₁ : c₁.sat x₁ = true) (b : Int) (w₂ : c₂.sat x₂ = true) : (combo a c₁ b c₂).sat (a * x₁ + b * x₂) = true

def Lean.Omega.Constraint.combine (x y : Constraint) : Constraint

The conjunction of two constraints.

theorem Lean.Omega.Constraint.combine_sat (c c' : Constraint) (t : Int) : ((c.combine c').sat t = true) = (c.sat t = true ∧ c'.sat t = true)

def Lean.Omega.Constraint.div (c : Constraint) (k : Nat) : Constraint

Dividing a constraint by a natural number, and tightened to integer bounds. Thus the lower bound is rounded up, and the upper bound is rounded down.

theorem Lean.Omega.Constraint.div_sat (c : Constraint) (t : Int) (k : Nat) (n : k ≠ 0) (h : ↑k ∣ t) (w : c.sat t = true) : (c.div k).sat (t / ↑k) = true

@[reducible, inline]

abbrev Lean.Omega.Constraint.sat' (c : Constraint) (x y : Coeffs) : Bool

It is convenient below to say that a constraint is satisfied at the dot product of two vectors, so we make an abbreviation sat' for this.

theorem Lean.Omega.Constraint.combine_sat' {s t : Constraint} {x y : Coeffs} (ws : s.sat' x y = true) (wt : t.sat' x y = true) : (s.combine t).sat' x y = true

theorem Lean.Omega.Constraint.div_sat' {c : Constraint} {x y : Coeffs} (h : x.gcd ≠ 0) (w : c.sat (x.dot y) = true) : (c.div x.gcd).sat' (x.sdiv ↑x.gcd) y = true

theorem Lean.Omega.Constraint.not_sat'_of_isImpossible {c : Constraint} (h : c.isImpossible = true) {x y : Coeffs} : ¬c.sat' x y = true

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

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

def Lean.Omega.normalize? : Constraint × Coeffs → Option (Constraint × 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.

def Lean.Omega.normalize (p : Constraint × Coeffs) : Constraint × Coeffs

Normalize a constraint, by dividing through by the GCD.

@[reducible, inline]

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

Shorthand for the first component of normalize.

@[reducible, inline]

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

Shorthand for the second component of normalize.

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

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

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

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

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

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

@[reducible, inline]

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

Shorthand for the first component of positivize.

@[reducible, inline]

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

Shorthand for the second component of positivize.

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

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

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

positivize and normalize, returning none if neither does anything.

def Lean.Omega.tidy (p : Constraint × Coeffs) : Constraint × Coeffs

positivize and normalize

@[reducible, inline]

abbrev Lean.Omega.tidyConstraint (s : Constraint) (x : Coeffs) : Constraint

Shorthand for the first component of tidy.

@[reducible, inline]

abbrev Lean.Omega.tidyCoeffs (s : Constraint) (x : Coeffs) : Coeffs

Shorthand for the second component of tidy.

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

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

@[reducible, inline]

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

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

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

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

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