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.

Equations

• Lean.Omega.LowerBound = Option Int

@[reducible, inline]

abbrev Lean.Omega.UpperBound : Type

An optional upper bound on a integer.

@[reducible, inline]

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

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

Equations

• b.sat t = Option.all (fun (x : Int) => decide (x ≤ t)) b

@[reducible, inline]

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

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

Equations

• b.sat t = Option.all (fun (y : Int) => decide (t ≤ y)) b

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 : Lean.Omega.LowerBound

  A lower bound.

• upperBound : Lean.Omega.UpperBound

  An upper bound.

instance Lean.Omega.instBEqConstraint : BEq Lean.Omega.Constraint

Equations

• Lean.Omega.instBEqConstraint = { beq := Lean.Omega.beqConstraint✝ }

instance Lean.Omega.instDecidableEqConstraint : DecidableEq Lean.Omega.Constraint

instance Lean.Omega.instReprConstraint : Repr Lean.Omega.Constraint

Equations

• Lean.Omega.instReprConstraint = { reprPrec := Lean.Omega.reprConstraint✝ }

instance Lean.Omega.Constraint.instToString : ToString Lean.Omega.Constraint

Equations

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

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

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

Equations

• c.sat t = decide (c.lowerBound.sat t = true ∧ c.upperBound.sat t = true)

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

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

Equations

• c.map f = { lowerBound := Option.map f c.lowerBound, upperBound := Option.map f c.upperBound }

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

Translate a constraint.

Equations

• c.translate t = c.map fun (x : Int) => x + t

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

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

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

Equations

• c.flip = { lowerBound := c.upperBound, upperBound := c.lowerBound }

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

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

Equations

• c.neg = c.flip.map fun (x : Int) => -x

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

def Lean.Omega.Constraint.trivial : Lean.Omega.Constraint

The trivial constraint, satisfied everywhere.

Equations

• Lean.Omega.Constraint.trivial = { lowerBound := none, upperBound := none }

def Lean.Omega.Constraint.impossible : Lean.Omega.Constraint

The impossible constraint, unsatisfiable.

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

An exact constraint.

Equations

• Lean.Omega.Constraint.exact r = { lowerBound := some r, upperBound := some r }

@[simp]

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

@[simp]

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

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

Check if a constraint is unsatisfiable.

Equations

• { lowerBound := some x_1, upperBound := some y }.isImpossible = decide (y < x_1)
• x.isImpossible = false

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

Check if a constraint requires an exact value.

Equations

• { lowerBound := some x_1, upperBound := some y }.isExact = decide (x_1 = y)
• x.isExact = false

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

def Lean.Omega.Constraint.scale (k : Int) (c : Lean.Omega.Constraint) : Lean.Omega.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].

Equations

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

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

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

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

Equations

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

theorem Lean.Omega.Constraint.add_sat {c₁ c₂ : Lean.Omega.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 : Lean.Omega.Constraint) (b : Int) (y : Lean.Omega.Constraint) : Lean.Omega.Constraint

A linear combination of two constraints.

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

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

The conjunction of two constraints.

Equations

• x.combine y = { lowerBound := max x.lowerBound y.lowerBound, upperBound := min x.upperBound y.upperBound }

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

def Lean.Omega.Constraint.div (c : Lean.Omega.Constraint) (k : Nat) : Lean.Omega.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.

Equations

• c.div k = { lowerBound := Option.map (fun (x : Int) => -(-x / ↑k)) c.lowerBound, upperBound := Option.map (fun (y : Int) => y / ↑k) c.upperBound }

theorem Lean.Omega.Constraint.div_sat (c : Lean.Omega.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 : Lean.Omega.Constraint) (x y : Lean.Omega.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.

Equations

• c.sat' x y = c.sat (x.dot y)

theorem Lean.Omega.Constraint.combine_sat' {s t : Lean.Omega.Constraint} {x y : Lean.Omega.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 : Lean.Omega.Constraint} {x y : Lean.Omega.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 : Lean.Omega.Constraint} (h : c.isImpossible = true) {x y : Lean.Omega.Coeffs} : ¬c.sat' x y = true

theorem Lean.Omega.Constraint.addInequality_sat {c : Int} {x y : Lean.Omega.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 : Lean.Omega.Coeffs} (w : c + x.dot y = 0) : { lowerBound := some (-c), upperBound := some (-c) }.sat' x y = true

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

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

Normalize a constraint, by dividing through by the GCD.

Equations

• Lean.Omega.normalize p = (Lean.Omega.normalize? p).getD p

@[reducible, inline]

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

Shorthand for the first component of normalize.

@[reducible, inline]

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

Shorthand for the second component of normalize.

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

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

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

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

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

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

Equations

• Lean.Omega.positivize p = (Lean.Omega.positivize? p).getD p

@[reducible, inline]

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

Shorthand for the first component of positivize.

@[reducible, inline]

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

Shorthand for the second component of positivize.

Equations

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

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

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

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

positivize and normalize, returning none if neither does anything.

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

positivize and normalize

Equations

• Lean.Omega.tidy p = (Lean.Omega.tidy? p).getD p

@[reducible, inline]

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

Shorthand for the first component of tidy.

@[reducible, inline]

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

Shorthand for the second component of tidy.

Equations

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

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

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

@[reducible, inline]

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

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

Equations

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

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

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

Equations

• Lean.Omega.bmod_coeffs m i x = (x.bmod m).set i ↑m

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