# 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`.

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

Instances For

source
instance Lean.Grind.instBEqIntInterval :
BEq IntInterval
Equations

- Lean.Grind.instBEqIntInterval = { beq := Lean.Grind.instBEqIntInterval.beq }

source
def Lean.Grind.instBEqIntInterval.beq :
IntInterval → IntInterval → Bool
Equations

- Lean.Grind.instBEqIntInterval.beq (Lean.Grind.IntInterval.co a a_1) (Lean.Grind.IntInterval.co b b_1) = (a == b && a_1 == b_1)
- Lean.Grind.instBEqIntInterval.beq (Lean.Grind.IntInterval.ci a) (Lean.Grind.IntInterval.ci b) = (a == b)
- Lean.Grind.instBEqIntInterval.beq (Lean.Grind.IntInterval.io a) (Lean.Grind.IntInterval.io b) = (a == b)
- Lean.Grind.instBEqIntInterval.beq Lean.Grind.IntInterval.ii Lean.Grind.IntInterval.ii = true
- Lean.Grind.instBEqIntInterval.beq x✝¹ x✝ = false

Instances For

source
instance Lean.Grind.instReflBEqIntInterval :
ReflBEq IntInterval
source
instance Lean.Grind.instLawfulBEqIntInterval :
LawfulBEq IntInterval
source
def Lean.Grind.instDecidableEqIntInterval.decEq (x✝ x✝¹ : IntInterval) :
Decidable (x✝ = x✝¹)
Equations

- One or more equations did not get rendered due to their size.
- Lean.Grind.instDecidableEqIntInterval.decEq (Lean.Grind.IntInterval.co lo hi) (Lean.Grind.IntInterval.ci lo_1) = isFalse ⋯
- Lean.Grind.instDecidableEqIntInterval.decEq (Lean.Grind.IntInterval.co lo hi) (Lean.Grind.IntInterval.io hi_1) = isFalse ⋯
- Lean.Grind.instDecidableEqIntInterval.decEq (Lean.Grind.IntInterval.co lo hi) Lean.Grind.IntInterval.ii = isFalse ⋯
- Lean.Grind.instDecidableEqIntInterval.decEq (Lean.Grind.IntInterval.ci lo) (Lean.Grind.IntInterval.co lo_1 hi) = isFalse ⋯
- Lean.Grind.instDecidableEqIntInterval.decEq (Lean.Grind.IntInterval.ci a) (Lean.Grind.IntInterval.ci b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
- Lean.Grind.instDecidableEqIntInterval.decEq (Lean.Grind.IntInterval.ci lo) (Lean.Grind.IntInterval.io hi) = isFalse ⋯
- Lean.Grind.instDecidableEqIntInterval.decEq (Lean.Grind.IntInterval.ci lo) Lean.Grind.IntInterval.ii = isFalse ⋯
- Lean.Grind.instDecidableEqIntInterval.decEq (Lean.Grind.IntInterval.io hi) (Lean.Grind.IntInterval.co lo hi_1) = isFalse ⋯
- Lean.Grind.instDecidableEqIntInterval.decEq (Lean.Grind.IntInterval.io hi) (Lean.Grind.IntInterval.ci lo) = isFalse ⋯
- Lean.Grind.instDecidableEqIntInterval.decEq (Lean.Grind.IntInterval.io a) (Lean.Grind.IntInterval.io b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
- Lean.Grind.instDecidableEqIntInterval.decEq (Lean.Grind.IntInterval.io hi) Lean.Grind.IntInterval.ii = isFalse ⋯
- Lean.Grind.instDecidableEqIntInterval.decEq Lean.Grind.IntInterval.ii (Lean.Grind.IntInterval.co lo hi) = isFalse ⋯
- Lean.Grind.instDecidableEqIntInterval.decEq Lean.Grind.IntInterval.ii (Lean.Grind.IntInterval.ci lo) = isFalse ⋯
- Lean.Grind.instDecidableEqIntInterval.decEq Lean.Grind.IntInterval.ii (Lean.Grind.IntInterval.io hi) = isFalse ⋯
- Lean.Grind.instDecidableEqIntInterval.decEq Lean.Grind.IntInterval.ii Lean.Grind.IntInterval.ii = isTrue ⋯

Instances For

source
instance Lean.Grind.instDecidableEqIntInterval :
DecidableEq IntInterval
Equations

- Lean.Grind.instDecidableEqIntInterval = Lean.Grind.instDecidableEqIntInterval.decEq

source
def Lean.Grind.instInhabitedIntInterval.default :
IntInterval
Equations

- Lean.Grind.instInhabitedIntInterval.default = Lean.Grind.IntInterval.co default default

Instances For

source
instance Lean.Grind.instInhabitedIntInterval :
Inhabited IntInterval
Equations

- Lean.Grind.instInhabitedIntInterval = { default := Lean.Grind.instInhabitedIntInterval.default }

source
@[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)

Instances For

source
@[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))

Instances For

source
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

Instances For

source
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

Instances For

source
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

Instances For

source
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

Instances For

source
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

Instances For

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

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

source
@[simp]
theorem Lean.Grind.IntInterval.mem_co (lo hi x : Int) :
x ∈ co lo hi ↔ lo ≤ x ∧ x < hi
source
@[simp]
theorem Lean.Grind.IntInterval.mem_ci (lo x : Int) :
x ∈ ci lo ↔ lo ≤ x
source
@[simp]
theorem Lean.Grind.IntInterval.mem_io (hi x : Int) :
x ∈ io hi ↔ x < hi
source
@[simp]
theorem Lean.Grind.IntInterval.mem_ii (x : Int) :
x ∈ ii ↔ True
source
theorem Lean.Grind.IntInterval.nonEmpty_of_mem {x : Int} {i : IntInterval} (h : x ∈ i) :
i.nonEmpty = true
source
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

Instances For

source
theorem Lean.Grind.IntInterval.wrap_wrap (i : IntInterval) (x : Int) :
i.wrap (i.wrap x) = i.wrap x
source
theorem Lean.Grind.IntInterval.wrap_mem (i : IntInterval) (h : i.nonEmpty = true) (x : Int) :
i.wrap x ∈ i
source
theorem Lean.Grind.IntInterval.wrap_eq_self_iff (i : IntInterval) (h : i.nonEmpty = true) (x : Int) :
i.wrap x = x ↔ x ∈ i
source
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)
source
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)
source
theorem Lean.Grind.IntInterval.wrap_eq_bmod {x i : Int} (h : 0 ≤ i) :
(co (-i) i).wrap x = x.bmod (2 * i).toNat
source
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
source
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.

Instances

source
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`.

Instances

source
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) = I.wrap ↑n

  The embedding takes `OfNat` to `OfNat`.

Instances

source
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) = I.wrap (↑x + ↑y)

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

Instances

source
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) = I.wrap (-↑x)

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

Instances

source
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) = I.wrap (↑x - ↑y)

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

Instances

source
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) = I.wrap (↑x * ↑y)

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

Instances

source
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) = I.wrap (↑x ^ n)

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

Instances

source
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.

Instances

source
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.

Instances

source
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 `≤`.

Instances

source
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 `<`.

Instances

## Helper theorems #

source
theorem Lean.Grind.ToInt.Zero.wrap_zero {α : Type u_1} (I : IntInterval) [_root_.Zero α] [ToInt α I] [Zero α I] :
I.wrap 0 = 0
source
@[simp]
theorem Lean.Grind.ToInt.wrap_toInt {α : Type u_1} (I : IntInterval) [ToInt α I] (x : α) :
I.wrap ↑x = ↑x
source
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

- ⋯ = ⋯

Instances For

source
def Lean.Grind.toIntUnexpander :
PrettyPrinter.Unexpander
Equations

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

Instances For