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 Std.Tactic.Omega.LowerBound : Type

An optional lower bound on a integer.

Equations

• Std.Tactic.Omega.LowerBound = Option Int

@[inline, reducible]

abbrev Std.Tactic.Omega.UpperBound : Type

An optional upper bound on a integer.

Equations

• Std.Tactic.Omega.UpperBound = Option Int

@[inline, reducible]

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

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

Equations

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

@[inline, reducible]

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

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

Equations

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

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

  A lower bound.

• upperBound : Std.Tactic.Omega.UpperBound

  An upper bound.

instance Std.Tactic.Omega.instBEqConstraint : BEq Std.Tactic.Omega.Constraint

Equations

• Std.Tactic.Omega.instBEqConstraint = { beq := Std.Tactic.Omega.beqConstraint✝ }

instance Std.Tactic.Omega.instDecidableEqConstraint : DecidableEq Std.Tactic.Omega.Constraint

Equations

• Std.Tactic.Omega.instDecidableEqConstraint = Std.Tactic.Omega.decEqConstraint✝

instance Std.Tactic.Omega.instReprConstraint : Repr Std.Tactic.Omega.Constraint

Equations

• Std.Tactic.Omega.instReprConstraint = { reprPrec := Std.Tactic.Omega.reprConstraint✝ }

instance Std.Tactic.Omega.Constraint.instToExprConstraint : Lean.ToExpr Std.Tactic.Omega.Constraint

Equations

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

instance Std.Tactic.Omega.Constraint.instToStringConstraint : ToString Std.Tactic.Omega.Constraint

Equations

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

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

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

Equations

• Std.Tactic.Omega.Constraint.sat c t = decide (Std.Tactic.Omega.LowerBound.sat c.lowerBound t = true ∧ Std.Tactic.Omega.UpperBound.sat c.upperBound t = true)

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

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

Equations

• Std.Tactic.Omega.Constraint.map c f = { lowerBound := Option.map f c.lowerBound, upperBound := Option.map f c.upperBound }

def Std.Tactic.Omega.Constraint.translate (c : Std.Tactic.Omega.Constraint) (t : Int) : Std.Tactic.Omega.Constraint

Translate a constraint.

Equations

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

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

def Std.Tactic.Omega.Constraint.flip (c : Std.Tactic.Omega.Constraint) : Std.Tactic.Omega.Constraint

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

Equations

• Std.Tactic.Omega.Constraint.flip c = { lowerBound := c.upperBound, upperBound := c.lowerBound }

def Std.Tactic.Omega.Constraint.neg (c : Std.Tactic.Omega.Constraint) : Std.Tactic.Omega.Constraint

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

Equations

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

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

def Std.Tactic.Omega.Constraint.trivial : Std.Tactic.Omega.Constraint

The trivial constraint, satisfied everywhere.

Equations

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

def Std.Tactic.Omega.Constraint.impossible : Std.Tactic.Omega.Constraint

The impossible constraint, unsatisfiable.

Equations

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

def Std.Tactic.Omega.Constraint.exact (r : Int) : Std.Tactic.Omega.Constraint

An exact constraint.

Equations

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

@[simp]

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

@[simp]

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

def Std.Tactic.Omega.Constraint.isImpossible : Std.Tactic.Omega.Constraint → Bool

Check if a constraint is unsatisfiable.

Equations

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

def Std.Tactic.Omega.Constraint.isExact : Std.Tactic.Omega.Constraint → Bool

Check if a constraint requires an exact value.

Equations

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

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

def Std.Tactic.Omega.Constraint.scale (k : Int) (c : Std.Tactic.Omega.Constraint) : Std.Tactic.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 Std.Tactic.Omega.Constraint.scale_sat {t : Int} {c : Std.Tactic.Omega.Constraint} (k : Int) (w : Std.Tactic.Omega.Constraint.sat c t = true) : Std.Tactic.Omega.Constraint.sat (Std.Tactic.Omega.Constraint.scale k c) (k * t) = true

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

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

A linear combination of two constraints.

Equations

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

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

def Std.Tactic.Omega.Constraint.combine (x : Std.Tactic.Omega.Constraint) (y : Std.Tactic.Omega.Constraint) : Std.Tactic.Omega.Constraint

The conjunction of two constraints.

Equations

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

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

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

• Std.Tactic.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 Std.Tactic.Omega.Constraint.div_sat (c : Std.Tactic.Omega.Constraint) (t : Int) (k : Nat) (n : k ≠ 0) (h : ↑k ∣ t) (w : Std.Tactic.Omega.Constraint.sat c t = true) : Std.Tactic.Omega.Constraint.sat (Std.Tactic.Omega.Constraint.div c k) (t / ↑k) = true

@[inline, reducible]

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

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

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

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

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