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 (-∞, ∞).

@[inline, reducible]

abbrev Lean.Omega.LowerBound : Type

An optional lower bound on a integer.

Equations

• Lean.Omega.LowerBound = Option Int

@[inline, reducible]

abbrev Lean.Omega.UpperBound : Type

An optional upper bound on a integer.

Equations

• Lean.Omega.UpperBound = Option Int

@[inline, reducible]

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

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

@[inline, reducible]

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

• Lean.Omega.UpperBound.sat b 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

Equations

• Lean.Omega.instDecidableEqConstraint = Lean.Omega.decEqConstraint✝

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

Equations

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

instance Lean.Omega.Constraint.instToStringConstraint : 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

• Lean.Omega.Constraint.sat c t = decide (Lean.Omega.LowerBound.sat c.lowerBound t = true ∧ Lean.Omega.UpperBound.sat c.upperBound 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

• Lean.Omega.Constraint.map c 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

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

theorem Lean.Omega.Constraint.translate_sat {t : Int} {c : Lean.Omega.Constraint} {v : Int} : Lean.Omega.Constraint.sat c v = true → Lean.Omega.Constraint.sat (Lean.Omega.Constraint.translate c t) (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

• Lean.Omega.Constraint.flip c = { 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

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

theorem Lean.Omega.Constraint.neg_sat {c : Lean.Omega.Constraint} {v : Int} : Lean.Omega.Constraint.sat c v = true → Lean.Omega.Constraint.sat (Lean.Omega.Constraint.neg c) (-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.

Equations

• Lean.Omega.Constraint.impossible = { lowerBound := some 1, upperBound := some 0 }

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.sat Lean.Omega.Constraint.trivial t = true

@[simp]

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

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

Check if a constraint is unsatisfiable.

Equations

• Lean.Omega.Constraint.isImpossible x = match x with | { lowerBound := some x, upperBound := some y } => decide (y < x) | x => false

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

Check if a constraint requires an exact value.

Equations

• Lean.Omega.Constraint.isExact x = match x with | { lowerBound := some x, upperBound := some y } => decide (x = y) | x => false

theorem Lean.Omega.Constraint.not_sat_of_isImpossible {c : Lean.Omega.Constraint} (h : Lean.Omega.Constraint.isImpossible c = true) {t : Int} : ¬Lean.Omega.Constraint.sat c 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 : Lean.Omega.Constraint.sat c t = true) : Lean.Omega.Constraint.sat (Lean.Omega.Constraint.scale k c) (k * t) = true

def Lean.Omega.Constraint.add (x : Lean.Omega.Constraint) (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₁ : Lean.Omega.Constraint} {c₂ : Lean.Omega.Constraint} {x₁ : Int} {x₂ : Int} (w₁ : Lean.Omega.Constraint.sat c₁ x₁ = true) (w₂ : Lean.Omega.Constraint.sat c₂ x₂ = true) : Lean.Omega.Constraint.sat (Lean.Omega.Constraint.add c₁ c₂) (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.

Equations

• Lean.Omega.Constraint.combo a x b y = Lean.Omega.Constraint.add (Lean.Omega.Constraint.scale a x) (Lean.Omega.Constraint.scale b y)

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

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

The conjunction of two constraints.

Equations

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

theorem Lean.Omega.Constraint.combine_sat (c : Lean.Omega.Constraint) (c' : Lean.Omega.Constraint) (t : Int) : (Lean.Omega.Constraint.sat (Lean.Omega.Constraint.combine c c') t = true) = (Lean.Omega.Constraint.sat c t = true ∧ Lean.Omega.Constraint.sat c' 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

• Lean.Omega.Constraint.div c 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 : Lean.Omega.Constraint.sat c t = true) : Lean.Omega.Constraint.sat (Lean.Omega.Constraint.div c k) (t / ↑k) = true

@[inline, reducible]

abbrev Lean.Omega.Constraint.sat' (c : Lean.Omega.Constraint) (x : Lean.Omega.Coeffs) (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

• Lean.Omega.Constraint.sat' c x y = Lean.Omega.Constraint.sat c (Lean.Omega.Coeffs.dot x y)

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

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

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

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

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

Equations

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

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 = Option.getD (Lean.Omega.normalize? p) p

@[inline, reducible]

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

Shorthand for the first component of normalize.

Equations

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

@[inline, reducible]

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

Shorthand for the second component of normalize.

Equations

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

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 : Lean.Omega.Coeffs} {v : Lean.Omega.Coeffs} (w : Lean.Omega.Constraint.sat' s x v = true) : Lean.Omega.Constraint.sat' (Lean.Omega.normalizeConstraint s x) (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.

Equations

• Lean.Omega.positivize? x = match x with | (s, x) => if 0 ≤ Lean.Omega.Coeffs.leading x then none else some (Lean.Omega.Constraint.neg s, Lean.Omega.Coeffs.smul x (-1))

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 = Option.getD (Lean.Omega.positivize? p) p

@[inline, reducible]

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

Shorthand for the first component of positivize.

Equations

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

@[inline, reducible]

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 : Lean.Omega.Coeffs} {v : Lean.Omega.Coeffs} (w : Lean.Omega.Constraint.sat' s x v = true) : Lean.Omega.Constraint.sat' (Lean.Omega.positivizeConstraint s x) (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.

Equations

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

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 = Option.getD (Lean.Omega.tidy? p) p

@[inline, reducible]

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

Shorthand for the first component of tidy.

Equations

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

@[inline, reducible]

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 : Lean.Omega.Coeffs} {v : Lean.Omega.Coeffs} (w : Lean.Omega.Constraint.sat' s x v = true) : Lean.Omega.Constraint.sat' (Lean.Omega.tidyConstraint s x) (Lean.Omega.tidyCoeffs s x) v = true

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

@[inline, reducible]

abbrev Lean.Omega.bmod_div_term (m : Nat) (a : Lean.Omega.Coeffs) (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 : Nat) (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 = Lean.Omega.Coeffs.set (Lean.Omega.Coeffs.bmod x m) i ↑m

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