Typeclasses for types that can be embedded into an interval of Int.

The typeclass ToInt α lo? hi? carries the data of a function ToInt.toInt : α → Int which is injective, lands between the (optional) lower and upper bounds lo? and hi?.

The function ToInt.wrap is the identity if either bound is none, and otherwise wraps the integers into the interval [lo, hi).

The typeclass ToInt.Add α lo? hi? then asserts that toInt (x + y) = wrap lo? hi? (toInt x + toInt y). There are many variants for other operations.

These typeclasses are used solely in the grind tactic to lift linear inequalities into Int.

inductive Lean.Grind.IntInterval : Type

An interval in the integers (either finite, half-infinite, or infinite).

• co (lo hi : Int) : IntInterval

  The finite interval [lo, hi).

• ci (lo : Int) : IntInterval

  The half-infinite interval [lo, ∞).

• io (hi : Int) : IntInterval

  The half-infinite interval (-∞, hi).

• ii : IntInterval

  The infinite interval (-∞, ∞).

instance Lean.Grind.instBEqIntInterval : BEq IntInterval

Equations

• Lean.Grind.instBEqIntInterval = { beq := Lean.Grind.beqIntInterval✝ }

instance Lean.Grind.instDecidableEqIntInterval : DecidableEq IntInterval

Equations

• Lean.Grind.instDecidableEqIntInterval = Lean.Grind.decEqIntInterval✝

instance Lean.Grind.instLawfulBEqIntInterval : LawfulBEq IntInterval

@[reducible, inline]

abbrev Lean.Grind.IntInterval.uint (n : Nat) : IntInterval

The interval [0, 2^n).

Equations

• Lean.Grind.IntInterval.uint n = Lean.Grind.IntInterval.co 0 (2 ^ n)

@[reducible, inline]

abbrev Lean.Grind.IntInterval.sint (n : Nat) : IntInterval

The interval [-2^(n-1), 2^(n-1)).

Equations

• Lean.Grind.IntInterval.sint n = Lean.Grind.IntInterval.co (-2 ^ (n - 1)) (2 ^ (n - 1))

def Lean.Grind.IntInterval.lo? (i : IntInterval) : Option Int

The lower bound of the interval, if finite.

Equations

• (Lean.Grind.IntInterval.co lo hi).lo? = some lo
• (Lean.Grind.IntInterval.ci lo).lo? = some lo
• (Lean.Grind.IntInterval.io hi).lo? = none
• Lean.Grind.IntInterval.ii.lo? = none

def Lean.Grind.IntInterval.hi? (i : IntInterval) : Option Int

The upper bound of the interval, if finite.

Equations

• (Lean.Grind.IntInterval.co lo hi).hi? = some hi
• (Lean.Grind.IntInterval.ci lo).hi? = none
• (Lean.Grind.IntInterval.io hi).hi? = some hi
• Lean.Grind.IntInterval.ii.hi? = none

def Lean.Grind.IntInterval.nonEmpty (i : IntInterval) : Bool

Equations

• (Lean.Grind.IntInterval.co lo hi).nonEmpty = decide (lo < hi)
• (Lean.Grind.IntInterval.ci lo).nonEmpty = true
• (Lean.Grind.IntInterval.io hi).nonEmpty = true
• Lean.Grind.IntInterval.ii.nonEmpty = true

def Lean.Grind.IntInterval.isFinite (i : IntInterval) : Bool

Equations

• (Lean.Grind.IntInterval.co lo hi).isFinite = true
• (Lean.Grind.IntInterval.ci lo).isFinite = false
• (Lean.Grind.IntInterval.io hi).isFinite = false
• Lean.Grind.IntInterval.ii.isFinite = false

def Lean.Grind.IntInterval.mem (i : IntInterval) (x : Int) : Prop

Equations

• (Lean.Grind.IntInterval.co lo hi).mem x = (lo ≤ x ∧ x < hi)
• (Lean.Grind.IntInterval.ci lo).mem x = (lo ≤ x)
• (Lean.Grind.IntInterval.io hi).mem x = (x < hi)
• Lean.Grind.IntInterval.ii.mem x = True

instance Lean.Grind.IntInterval.instMembershipInt : Membership Int IntInterval

Equations

• Lean.Grind.IntInterval.instMembershipInt = { mem := Lean.Grind.IntInterval.mem }

@[simp]

theorem Lean.Grind.IntInterval.mem_co (lo hi x : Int) : x ∈ co lo hi ↔ lo ≤ x ∧ x < hi

@[simp]

theorem Lean.Grind.IntInterval.mem_ci (lo x : Int) : x ∈ ci lo ↔ lo ≤ x

@[simp]

theorem Lean.Grind.IntInterval.mem_io (hi x : Int) : x ∈ io hi ↔ x < hi

@[simp]

theorem Lean.Grind.IntInterval.mem_ii (x : Int) : x ∈ ii ↔ True

theorem Lean.Grind.IntInterval.nonEmpty_of_mem {x : Int} {i : IntInterval} (h : x ∈ i) : i.nonEmpty = true

def Lean.Grind.IntInterval.wrap (i : IntInterval) (x : Int) : Int

Equations

• (Lean.Grind.IntInterval.co lo hi).wrap x = (x - lo) % (hi - lo) + lo
• (Lean.Grind.IntInterval.ci lo).wrap x = max x lo
• (Lean.Grind.IntInterval.io hi).wrap x = min x (hi - 1)
• Lean.Grind.IntInterval.ii.wrap x = x

theorem Lean.Grind.IntInterval.wrap_wrap (i : IntInterval) (x : Int) : i.wrap (i.wrap x) = i.wrap x

theorem Lean.Grind.IntInterval.wrap_mem (i : IntInterval) (h : i.nonEmpty = true) (x : Int) : i.wrap x ∈ i

theorem Lean.Grind.IntInterval.wrap_eq_self_iff (i : IntInterval) (h : i.nonEmpty = true) (x : Int) : i.wrap x = x ↔ x ∈ i

theorem Lean.Grind.IntInterval.wrap_add {i : IntInterval} (h : i.isFinite = true) (x y : Int) : i.wrap (x + y) = i.wrap (i.wrap x + i.wrap y)

theorem Lean.Grind.IntInterval.wrap_mul {i : IntInterval} (h : i.isFinite = true) (x y : Int) : i.wrap (x * y) = i.wrap (i.wrap x * i.wrap y)

theorem Lean.Grind.IntInterval.wrap_eq_bmod {x i : Int} (h : 0 ≤ i) : (co (-i) i).wrap x = x.bmod (2 * i).toNat

theorem Lean.Grind.IntInterval.wrap_eq_wrap_iff {lo hi x y : Int} : (co lo hi).wrap x = (co lo hi).wrap y ↔ (x - y) % (hi - lo) = 0

class Lean.Grind.ToInt (α : Type u) (range : outParam IntInterval) : Type u

ToInt α I asserts that α can be embedded faithfully into an interval I in the integers.

• toInt : α → Int

  The embedding function.

• toInt_inj (x y : α) : ↑x = ↑y → x = y

  The embedding function is injective.

• toInt_mem (x : α) : ↑x ∈ range

  The embedding function lands in the interval.

class Lean.Grind.ToInt.Zero (α : Type u) [_root_.Zero α] (I : outParam IntInterval) [ToInt α I] : Prop

The embedding into the integers takes 0 to 0.

• toInt_zero : ↑0 = 0

  The embedding takes 0 to 0.

class Lean.Grind.ToInt.OfNat (α : Type u) [(n : Nat) → _root_.OfNat α n] (I : outParam IntInterval) [ToInt α I] : Prop

The embedding into the integers takes numerals in the range interval to themselves.

• toInt_ofNat (n : Nat) : ↑(OfNat.ofNat n) = IntInterval.wrap I ↑n

  The embedding takes OfNat to OfNat.

class Lean.Grind.ToInt.Add (α : Type u) [_root_.Add α] (I : outParam IntInterval) [ToInt α I] : Prop

The embedding into the integers takes addition to addition, wrapped into the range interval.

• toInt_add (x y : α) : ↑(x + y) = IntInterval.wrap I (↑x + ↑y)

  The embedding takes addition to addition, wrapped into the range interval.

class Lean.Grind.ToInt.Neg (α : Type u) [_root_.Neg α] (I : outParam IntInterval) [ToInt α I] : Prop

The embedding into the integers takes negation to negation, wrapped into the range interval.

• toInt_neg (x : α) : ↑(-x) = IntInterval.wrap I (-↑x)

  The embedding takes negation to negation, wrapped into the range interval.

class Lean.Grind.ToInt.Sub (α : Type u) [_root_.Sub α] (I : outParam IntInterval) [ToInt α I] : Prop

The embedding into the integers takes subtraction to subtraction, wrapped into the range interval.

• toInt_sub (x y : α) : ↑(x - y) = IntInterval.wrap I (↑x - ↑y)

  The embedding takes subtraction to subtraction, wrapped into the range interval.

class Lean.Grind.ToInt.Mul (α : Type u) [_root_.Mul α] (I : outParam IntInterval) [ToInt α I] : Prop

The embedding into the integers takes multiplication to multiplication, wrapped into the range interval.

• toInt_mul (x y : α) : ↑(x * y) = IntInterval.wrap I (↑x * ↑y)

  The embedding takes multiplication to multiplication, wrapped into the range interval.

class Lean.Grind.ToInt.Pow (α : Type u) [HPow α Nat α] (I : outParam IntInterval) [ToInt α I] : Prop

The embedding into the integers takes exponentiation to exponentiation, wrapped into the range interval.

• toInt_pow (x : α) (n : Nat) : ↑(x ^ n) = IntInterval.wrap I (↑x ^ n)

  The embedding takes exponentiation to exponentiation, wrapped into the range interval.

class Lean.Grind.ToInt.Mod (α : Type u) [_root_.Mod α] (I : outParam IntInterval) [ToInt α I] : Prop

The embedding into the integers takes modulo to modulo (without needing to wrap into the range interval).

• toInt_mod (x y : α) : ↑(x % y) = ↑x % ↑y

  The embedding takes modulo to modulo (without needing to wrap into the range interval). One might expect a wrap on the right hand side, but in practice this stronger statement is usually true.

class Lean.Grind.ToInt.Div (α : Type u) [_root_.Div α] (I : outParam IntInterval) [ToInt α I] : Prop

The embedding into the integers takes division to division, wrapped into the range interval.

• toInt_div (x y : α) : ↑(x / y) = ↑x / ↑y

  The embedding takes division to division (without needing to wrap into the range interval). One might expect a wrap on the right hand side, but in practice this stronger statement is usually true.

class Lean.Grind.ToInt.LE (α : Type u) [_root_.LE α] (I : outParam IntInterval) [ToInt α I] : Prop

The embedding into the integers is monotone.

• le_iff (x y : α) : x ≤ y ↔ ↑x ≤ ↑y

  The embedding is monotone with respect to ≤.

class Lean.Grind.ToInt.LT (α : Type u) [_root_.LT α] (I : outParam IntInterval) [ToInt α I] : Prop

The embedding into the integers is strictly monotone.

• lt_iff (x y : α) : x < y ↔ ↑x < ↑y

  The embedding is strictly monotone with respect to <.

Helper theorems

theorem Lean.Grind.ToInt.Zero.wrap_zero {α : Type u_1} (I : IntInterval) [_root_.Zero α] [ToInt α I] [Zero α I] : I.wrap 0 = 0

@[simp]

theorem Lean.Grind.ToInt.wrap_toInt {α : Type u_1} (I : IntInterval) [ToInt α I] (x : α) : I.wrap ↑x = ↑x

def Lean.Grind.ToInt.Sub.of_sub_eq_add_neg {α : Type u} [_root_.Add α] [_root_.Neg α] [_root_.Sub α] (sub_eq_add_neg : ∀ (x y : α), x - y = x + -y) {I : IntInterval} (h : I.isFinite = true) [ToInt α I] [Add α I] [Neg α I] : Sub α I

Construct a ToInt.Sub instance from a ToInt.Add and ToInt.Neg instance and a sub_eq_add_neg assumption.

Equations

• ⋯ = ⋯

def Lean.Grind.toIntUnexpander : PrettyPrinter.Unexpander

Equations

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