Init.Data.Int.Basic

Int inductive

: Type

Full source

/--
The integers.

This type is special-cased by the compiler and overridden with an efficient implementation. The
runtime has a special representation for `Int` that stores “small” signed numbers directly, while
larger numbers use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)). A “small number” is an integer that can be encoded with one fewer bits
than the platform's pointer size (i.e. 63 bits on 64-bit architectures and 31 bits on 32-bit
architectures).
-/
inductive Int : Type where
  /--
  A natural number is an integer.

  This constructor covers the non-negative integers (from `0` to `∞`).
  -/
  | ofNat   : Nat → Int
  /--
  The negation of the successor of a natural number is an integer.

  This constructor covers the negative integers (from `-1` to `-∞`).
  -/
  | negSucc : Nat → Int

Integers

Informal description

The type of integers, denoted as $\mathbb{Z}$. This type is implemented efficiently by the compiler, with small integers stored directly and larger integers using arbitrary-precision arithmetic. A "small integer" is defined as one that can be encoded with one fewer bits than the platform's pointer size (e.g., 63 bits on 64-bit systems).

instNatCastInt instance

: NatCast Int

Full source

instance : NatCast Int where natCast n := Int.ofNat n

Natural Number Coercion to Integers

Informal description

The integers $\mathbb{Z}$ have a canonical structure that allows natural numbers to be cast into them.

instOfNat instance

: OfNat Int n

Full source

instance instOfNat : OfNat Int n where
  ofNat := Int.ofNat n

Natural Number Literals as Integers

Informal description

For any natural number $n$, there is a canonical interpretation of $n$ as an integer in $\mathbb{Z}$.

Int.term-[_+1] definition

: Lean.ParserDescr✝

Full source

/--
`-[n+1]` is suggestive notation for `negSucc n`, which is the second constructor of
`Int` for making strictly negative numbers by mapping `n : Nat` to `-(n + 1)`.
-/
scoped notation "-[" n "+1]" => negSucc n

Negative integer notation `-[n+1]`

Informal description

The notation `-[n+1]` represents the strictly negative integer obtained by mapping a natural number `n` to `-(n + 1)`, which corresponds to the `negSucc` constructor of the `Int` type.

Int.instInhabited instance

: Inhabited Int

Full source

instance : Inhabited Int := ⟨ofNat 0⟩

Inhabited Type of Integers with Default Zero

Informal description

The type of integers $\mathbb{Z}$ is inhabited, with $0$ as its default element.

Int.default_eq_zero theorem

: default = (0 : Int)

Full source

@[simp] theorem default_eq_zero : default = (0 : Int) := rfl

Default Integer is Zero

Informal description

The default integer value is equal to $0$, i.e., $\text{default} = 0$.

Int.zero_ne_one theorem

: (0 : Int) ≠ 1

Full source

protected theorem zero_ne_one : (0 : Int) ≠ 1 := nofun

Non-equality of Zero and One in Integers

Informal description

The integer $0$ is not equal to the integer $1$, i.e., $0 \neq 1$.

Int.ofNat_eq_coe theorem

: Int.ofNat n = Nat.cast n

Full source

@[simp] theorem ofNat_eq_coe : Int.ofNat n = Nat.cast n := rfl

Equality of Natural Number to Integer Conversion Functions

Informal description

For any natural number $n$, the integer obtained by applying the `Int.ofNat` function to $n$ is equal to the canonical image of $n$ in the integers via the `Nat.cast` function, i.e., $\text{Int.ofNat}(n) = n$ where $n$ is interpreted as an integer.

Int.ofNat_zero theorem

: ((0 : Nat) : Int) = 0

Full source

@[simp] theorem ofNat_zero : ((0 : Nat) : Int) = 0 := rfl

Zero Coercion from Natural Numbers to Integers

Informal description

The canonical image of the natural number $0$ in the integers is equal to the integer $0$, i.e., $(0 : \mathbb{Z}) = 0$.

Int.ofNat_one theorem

: ((1 : Nat) : Int) = 1

Full source

@[simp] theorem ofNat_one  : ((1 : Nat) : Int) = 1 := rfl

Natural One Coerces to Integer One

Informal description

The canonical image of the natural number $1$ in the integers is equal to the integer $1$, i.e., $(1 : \mathbb{Z}) = 1$.

Int.ofNat_two theorem

: ((2 : Nat) : Int) = 2

Full source

theorem ofNat_two : ((2 : Nat) : Int) = 2 := rfl

Natural Two Coerces to Integer Two

Informal description

The canonical image of the natural number $2$ in the integers is equal to the integer $2$, i.e., $(2 : \mathbb{Z}) = 2$.

Int.negOfNat definition

: Nat → Int

Full source

/--
Negation of natural numbers.

Examples:
 * `Int.negOfNat 6 = -6`
 * `Int.negOfNat 0 = 0`
-/
def negOfNat : Nat → Int
  | 0      => 0
  | succ m => negSucc m

Negation of natural numbers as integers

Informal description

The function `Int.negOfNat` maps a natural number $n$ to its negation as an integer. Specifically: - If $n = 0$, it returns $0$. - If $n = m + 1$ for some natural number $m$, it returns the negative successor $- (m + 1)$.

Int.neg definition

(n : @& Int) : Int

Full source

/--
Negation of integers, usually accessed via the `-` prefix operator.

This function is overridden by the compiler with an efficient implementation. This definition is
the logical model.

Examples:
 * `-(6 : Int) = -6`
 * `-(-6 : Int) = 6`
 * `(12 : Int).neg = -12`
-/
@[extern "lean_int_neg"]
protected def neg (n : @& Int) : Int :=
  match n with
  | ofNat n   => negOfNat n
  | negSucc n => succ n

Integer negation

Informal description

The negation function on integers, which maps an integer $n$ to its additive inverse $-n$. For non-negative integers (represented as `ofNat n`), this is computed as the negation of the natural number $n$ (using `negOfNat`). For negative integers (represented as `negSucc n`), this is computed as the successor of the natural number $n$.

Int.instNegInt instance

: Neg Int

Full source

@[default_instance mid]
instance instNegInt : Neg Int where
  neg := Int.neg

Negation Operation on Integers

Informal description

The integers $\mathbb{Z}$ are equipped with a negation operation, where for any integer $n$, its negation $-n$ is defined as follows: - If $n$ is a non-negative integer (represented as `ofNat n`), then $-n$ is the negation of the natural number $n$. - If $n$ is a negative integer (represented as `negSucc n`), then $-n$ is the successor of the natural number $n$.

Int.subNatNat definition

(m n : Nat) : Int

Full source

/--
Non-truncating subtraction of two natural numbers.

Examples:
 * `Int.subNatNat 5 2 = 3`
 * `Int.subNatNat 2 5 = -3`
 * `Int.subNatNat 0 13 = -13`
-/
def subNatNat (m n : Nat) : Int :=
  match (n - m : Nat) with
  | 0        => ofNat (m - n)  -- m ≥ n
  | (succ k) => negSucc k

Non-truncating subtraction of natural numbers as integers

Informal description

The function `Int.subNatNat` computes the difference between two natural numbers $m$ and $n$ as an integer, without truncation. Specifically: - If $m \geq n$, it returns the natural number difference $m - n$. - If $m < n$, it returns the negative integer $- (n - m)$ (represented as `negSucc k` where $k = n - m - 1$). Examples: - `Int.subNatNat 5 2 = 3` - `Int.subNatNat 2 5 = -3` - `Int.subNatNat 0 13 = -13`

Int.add definition

(m n : @& Int) : Int

Full source

/--
Addition of integers, usually accessed via the `+` operator.

This function is overridden by the compiler with an efficient implementation. This definition is
the logical model.

Examples:
 * `(7 : Int) + (6 : Int) = 13`
 * `(6 : Int) + (-6 : Int) = 0`
-/
@[extern "lean_int_add"]
protected def add (m n : @& Int) : Int :=
  match m, n with
  | ofNat m, ofNat n => ofNat (m + n)
  | ofNat m, -[n +1] => subNatNat m (succ n)
  | -[m +1], ofNat n => subNatNat n (succ m)
  | -[m +1], -[n +1] => negSucc (succ (m + n))

Integer addition

Informal description

The addition operation on integers, defined by cases: - For non-negative integers $m$ and $n$, $m + n$ is their sum as natural numbers. - For a non-negative integer $m$ and a negative integer $- (n + 1)$, $m + (- (n + 1))$ is $m - (n + 1)$ (computed via `subNatNat`). - For a negative integer $- (m + 1)$ and a non-negative integer $n$, $- (m + 1) + n$ is $n - (m + 1)$ (computed via `subNatNat`). - For negative integers $- (m + 1)$ and $- (n + 1)$, $- (m + 1) + (- (n + 1)) = - (m + n + 2)$. This operation is the logical model for integer addition, though the compiler provides an optimized implementation.

Int.instAdd instance

: Add Int

Full source

instance : Add Int where
  add := Int.add

Addition on Integers

Informal description

The integers $\mathbb{Z}$ are equipped with a canonical addition operation.

Int.mul definition

(m n : @& Int) : Int

Full source

/--
Multiplication of integers, usually accessed via the `*` operator.

This function is overridden by the compiler with an efficient implementation. This definition is
the logical model.

Examples:
 * `(63 : Int) * (6 : Int) = 378`
 * `(6 : Int) * (-6 : Int) = -36`
 * `(7 : Int) * (0 : Int) = 0`
-/
@[extern "lean_int_mul"]
protected def mul (m n : @& Int) : Int :=
  match m, n with
  | ofNat m, ofNat n => ofNat (m * n)
  | ofNat m, -[n +1] => negOfNat (m * succ n)
  | -[m +1], ofNat n => negOfNat (succ m * n)
  | -[m +1], -[n +1] => ofNat (succ m * succ n)

Integer multiplication

Informal description

The multiplication operation on integers, denoted by $*$, is defined as follows: - For non-negative integers $m$ and $n$, $m * n$ is the product of $m$ and $n$ as natural numbers. - For a non-negative integer $m$ and a negative integer $-n-1$, $m * (-n-1)$ is the negation of the product of $m$ and $n+1$. - For a negative integer $-m-1$ and a non-negative integer $n$, $(-m-1) * n$ is the negation of the product of $m+1$ and $n$. - For negative integers $-m-1$ and $-n-1$, $(-m-1) * (-n-1)$ is the product of $m+1$ and $n+1$ as natural numbers. This definition serves as the logical model for integer multiplication, while the actual implementation is optimized by the compiler.

Int.instMul instance

: Mul Int

Full source

instance : Mul Int where
  mul := Int.mul

Multiplication Operation on Integers

Informal description

The integers $\mathbb{Z}$ are equipped with a canonical multiplication operation.

Int.sub definition

(m n : @& Int) : Int

Full source

/--
Subtraction of integers, usually accessed via the `-` operator.

This function is overridden by the compiler with an efficient implementation. This definition is
the logical model.

Examples:
* `(63 : Int) - (6 : Int) = 57`
* `(7 : Int) - (0 : Int) = 7`
* `(0 : Int) - (7 : Int) = -7`
-/
@[extern "lean_int_sub"]
protected def sub (m n : @& Int) : Int := m + (- n)

Integer subtraction

Informal description

The subtraction operation on integers, defined as $m - n = m + (-n)$ for any integers $m$ and $n$.

Int.instSub instance

: Sub Int

Full source

instance : Sub Int where
  sub := Int.sub

Subtraction Operation on Integers

Informal description

The integers $\mathbb{Z}$ are equipped with a canonical subtraction operation.

Int.NonNeg inductive

: Int → Prop

Full source

/--
An integer is non-negative if it is equal to a natural number.
-/
inductive NonNeg : Int → Prop where
  /--
  For all natural numbers `n`, `Int.ofNat n` is non-negative.
  -/
  | mk (n : Nat) : NonNeg (ofNat n)

Non-negative integer condition

Informal description

An integer $ z $ is said to be non-negative if there exists a natural number $ n $ such that $ z = n $. This is denoted by the predicate $\text{NonNeg}(z)$.

Int.le definition

(a b : Int) : Prop

Full source

/--
Non-strict inequality of integers, usually accessed via the `≤` operator.

`a ≤ b` is defined as `b - a ≥ 0`, using `Int.NonNeg`.
-/
protected def le (a b : Int) : Prop := NonNeg (b - a)

Integer non-strict inequality (≤)

Informal description

The non-strict inequality relation on integers, where $a \leq b$ is defined as $b - a$ being non-negative (i.e., $b - a$ can be expressed as a natural number).

Int.instLEInt instance

: LE Int

Full source

instance instLEInt : LE Int where
  le := Int.le

The Non-Strict Order on Integers

Informal description

The integers $\mathbb{Z}$ are equipped with a canonical non-strict order relation $\leq$.

Int.lt definition

(a b : Int) : Prop

Full source

/--
Strict inequality of integers, usually accessed via the `<` operator.

`a < b` when `a + 1 ≤ b`.
-/
protected def lt (a b : Int) : Prop := (a + 1) ≤ b

Integer strict inequality (<)

Informal description

The strict inequality relation on integers, where $a < b$ is defined as $a + 1 \leq b$.

Int.instLTInt instance

: LT Int

Full source

instance instLTInt : LT Int where
  lt := Int.lt

The Strict Order on Integers

Informal description

The integers $\mathbb{Z}$ are equipped with a canonical strict order relation $<$.

Int.decEq definition

(a b : @& Int) : Decidable (a = b)

Full source

/--
Decides whether two integers are equal. Usually accessed via the `DecidableEq Int` instance.

This function is overridden by the compiler with an efficient implementation. This definition is the
logical model.

Examples:
* `show (7 : Int) = (3 : Int) + (4 : Int) by decide`
* `if (6 : Int) = (3 : Int) * (2 : Int) then "yes" else "no" = "yes"`
* `(¬ (6 : Int) = (3 : Int)) = true`
-/
@[extern "lean_int_dec_eq"]
protected def decEq (a b : @& Int) : Decidable (a = b) :=
  match a, b with
  | ofNat a, ofNat b => match decEq a b with
    | isTrue h  => isTrue  <| h ▸ rfl
    | isFalse h => isFalse <| fun h' => Int.noConfusion h' (fun h' => absurd h' h)
  | ofNat _, -[_ +1] => isFalse <| fun h => Int.noConfusion h
  | -[_ +1], ofNat _ => isFalse <| fun h => Int.noConfusion h
  | -[a +1], -[b +1] => match decEq a b with
    | isTrue h  => isTrue  <| h ▸ rfl
    | isFalse h => isFalse <| fun h' => Int.noConfusion h' (fun h' => absurd h' h)

Decidable equality for integers

Informal description

The function `Int.decEq` takes two integers `a` and `b` and returns a `Decidable` instance for the proposition `a = b`. This provides a constructive way to determine whether two integers are equal. The function handles both non-negative integers (represented as `ofNat`) and negative integers (represented as `-[n +1]`) by pattern matching and recursively checking equality of their underlying natural number representations.

Int.instDecidableEq instance

: DecidableEq Int

Full source

@[inherit_doc Int.decEq]
instance : DecidableEq Int := Int.decEq

Decidable Equality for Integers

Informal description

The integers $\mathbb{Z}$ have decidable equality, meaning for any two integers $a$ and $b$, the equality $a = b$ can be constructively determined.

Int.decLe instance

(a b : @& Int) : Decidable (a ≤ b)

Full source

/-- Decides whether `a ≤ b`.

  ```
  #eval ¬ ( (7 : Int) ≤ (0 : Int) ) -- true
  #eval (0 : Int) ≤ (0 : Int) -- true
  #eval (7 : Int) ≤ (10 : Int) -- true
  ```

  Implemented by efficient native code. -/
@[extern "lean_int_dec_le"]
instance decLe (a b : @& Int) : Decidable (a ≤ b) :=
  decNonneg _

Decidability of Integer Ordering

Informal description

For any two integers $a$ and $b$, the inequality $a \leq b$ is decidable.

Int.decLt instance

(a b : @& Int) : Decidable (a < b)

Full source

/-- Decides whether `a < b`.

  ```
  #eval `¬ ( (7 : Int) < 0 )` -- true
  #eval `¬ ( (0 : Int) < 0 )` -- true
  #eval `(7 : Int) < 10` -- true
  ```

  Implemented by efficient native code. -/
@[extern "lean_int_dec_lt"]
instance decLt (a b : @& Int) : Decidable (a < b) :=
  decNonneg _

Decidability of Strict Integer Ordering

Informal description

For any two integers $a$ and $b$, the strict inequality $a < b$ is decidable.

Int.natAbs definition

(m : @& Int) : Nat

Full source

/--
The absolute value of an integer is its distance from `0`.

This function is overridden by the compiler with an efficient implementation. This definition is
the logical model.

Examples:
 * `(7 : Int).natAbs = 7`
 * `(0 : Int).natAbs = 0`
 * `((-11 : Int).natAbs = 11`
-/
@[extern "lean_nat_abs"]
def natAbs (m : @& Int) : Nat :=
  match m with
  | ofNat m => m
  | -[m +1] => m.succ

Absolute value of an integer (as natural number)

Informal description

The function maps an integer $ m $ to its absolute value as a natural number. Specifically: - If $ m $ is non-negative (of the form `ofNat m`), it returns $ m $ - If $ m $ is negative (of the form `-[m+1]`), it returns $ m + 1 $ This provides the logical model for integer absolute value, though in practice the compiler overrides this with a more efficient implementation.

Int.sign definition

: Int → Int

Full source

/--
Returns the “sign” of the integer as another integer:
 * `1` for positive numbers,
 * `-1` for negative numbers, and
 * `0` for `0`.

Examples:
 * `Int.sign 34 = 1`
 * `Int.sign 2 = 1`
 * `Int.sign 0 = 0`
 * `Int.sign -1 = -1`
 * `Int.sign -362 = -1`
-/
def sign : Int → Int
  | Int.ofNat (succ _) => 1
  | Int.ofNat 0 => 0
  | -[_+1]      => -1

Sign function on integers

Informal description

The function $\text{sign} : \mathbb{Z} \to \mathbb{Z}$ maps an integer to its sign: - $1$ if the integer is positive, - $-1$ if the integer is negative, and - $0$ if the integer is zero.

Int.toNat definition

: Int → Nat

Full source

/--
Converts an integer into a natural number. Negative numbers are converted to `0`.

Examples:
* `(7 : Int).toNat = 7`
* `(0 : Int).toNat = 0`
* `(-7 : Int).toNat = 0`
-/
def toNat : Int → Nat
  | ofNat n   => n
  | negSucc _ => 0

Integer to natural number conversion (negative to zero)

Informal description

The function converts an integer to a natural number, mapping non-negative integers to their natural number counterpart and negative integers to zero. Specifically: - For a non-negative integer `ofNat n`, returns `n` - For a negative integer `negSucc _`, returns `0`

Int.toNat? definition

: Int → Option Nat

Full source

/--
Converts an integer into a natural number. Returns `none` for negative numbers.

Examples:
* `(7 : Int).toNat? = some 7`
* `(0 : Int).toNat? = some 0`
* `(-7 : Int).toNat? = none`
-/
def toNat? : Int → Option Nat
  | (n : Nat) => some n
  | -[_+1] => none

Optional conversion from integer to natural number

Informal description

The function converts an integer $n$ to an optional natural number, returning $\text{some } n$ if $n$ is non-negative and $\text{none}$ if $n$ is negative.

Int.toNat' abbrev

Full source

@[deprecated toNat? (since := "2025-03-11"), inherit_doc toNat?]
abbrev toNat' := toNat?

Non-negative Integer to Natural Number Conversion with Zero Default

Informal description

The function `Int.toNat'` converts an integer $n$ to a natural number, returning $n$ if $n$ is non-negative and $0$ if $n$ is negative.

Int.instDvd instance

: Dvd Int

Full source

/--
Divisibility of integers. `a ∣ b` (typed as `\|`) says that
there is some `c` such that `b = a * c`.
-/
instance : Dvd Int where
  dvd a b := Exists (fun c => b = a * c)

Divisibility Relation on Integers

Informal description

The integers $\mathbb{Z}$ are equipped with a canonical divisibility relation, where $a \mid b$ means there exists an integer $c$ such that $b = a \cdot c$.

Int.pow definition

(m : Int) : Nat → Int

Full source

/--
Power of an integer to a natural number, usually accessed via the `^` operator.

Examples:
* `(2 : Int) ^ 4 = 16`
* `(10 : Int) ^ 0 = 1`
* `(0 : Int) ^ 10 = 0`
* `(-7 : Int) ^ 3 = -343`
-/
protected def pow (m : Int) : Nat → Int
  | 0      => 1
  | succ n => Int.pow m n * m

Integer power function

Informal description

The function `Int.pow` takes an integer $m$ and a natural number $n$, and returns $m$ raised to the power of $n$, defined recursively as: - $m^0 = 1$ - $m^{n+1} = m^n \cdot m$

Int.instNatPow instance

: NatPow Int

Full source

instance : NatPow Int where
  pow := Int.pow

Natural Number Power Operation on Integers

Informal description

The integers $\mathbb{Z}$ are equipped with a canonical power operation where the exponent is a natural number. This operation is defined recursively by $m^0 = 1$ and $m^{n+1} = m^n \cdot m$ for any integer $m$ and natural number $n$.

Int.instLawfulBEq instance

: LawfulBEq Int

Full source

instance : LawfulBEq Int where
  eq_of_beq h := by simp [BEq.beq] at h; assumption
  rfl := by simp [BEq.beq]

Lawful Boolean Equality on Integers

Informal description

The integers $\mathbb{Z}$ have a boolean equality structure that is lawful, meaning the boolean equality operator `==` coincides with the propositional equality `=` on $\mathbb{Z}$. Specifically: 1. For any integers $a$ and $b$, if `a == b` evaluates to `true`, then $a = b$. 2. For any integer $a$, the test `a == a` evaluates to `true$.

Int.instMin instance

: Min Int

Full source

instance : Min Int := minOfLe

The Minimum Operation on Integers

Informal description

The integers $\mathbb{Z}$ are equipped with a canonical minimum operation $\min$.

Int.instMax instance

: Max Int

Full source

instance : Max Int := maxOfLe

The Maximum Operation on Integers

Informal description

The integers $\mathbb{Z}$ are equipped with a canonical maximum operation $\max$ with respect to their natural order.

IntCast structure

(R : Type u)

Full source

/--
The canonical homomorphism `Int → R`. In most use cases, the target type will have a ring structure,
and this homomorphism should be a ring homomorphism.

`IntCast` and `NatCast` exist to allow different libraries with their own types that can be notated
as natural numbers to have consistent `simp` normal forms without needing to create coercion
simplification sets that are aware of all combinations. Libraries should make it easy to work with
`IntCast` where possible. For instance, in Mathlib there will be such a homomorphism (and thus an
`IntCast R` instance) whenever `R` is an additive group with a `1`.
-/
class IntCast (R : Type u) where
  /-- The canonical map `Int → R`. -/
  protected intCast : Int → R

Canonical integer homomorphism

Informal description

The structure `IntCast R` represents the canonical homomorphism from the integers to a type `R`. Typically, `R` is a ring, and this homomorphism preserves the ring structure. This structure allows different libraries to handle their own types that can be notated as integers while maintaining consistent simplification forms without needing to define specific coercion rules for each combination.

instIntCastInt instance

: IntCast Int

Full source

instance : IntCast Int where intCast n := n

Identity Homomorphism on Integers

Informal description

The integers $\mathbb{Z}$ have a canonical homomorphism from $\mathbb{Z}$ to itself, given by the identity map.

Int.cast definition

{R : Type u} [IntCast R] : Int → R

Full source

@[coe, reducible, match_pattern, inherit_doc IntCast]
protected def Int.cast {R : Type u} [IntCast R] : Int → R :=
  IntCast.intCast

Canonical integer homomorphism function

Informal description

The function maps an integer $n \in \mathbb{Z}$ to its canonical image in a type $R$ equipped with an integer homomorphism structure `[IntCast R]`. This is the underlying function of the `IntCast` structure.

instCoeTailIntOfIntCast instance

[IntCast R] : CoeTail Int R

Full source

instance [IntCast R] : CoeTail Int R where coe := Int.cast

Tail Coercion from Integers to Type with Integer Homomorphism

Informal description

For any type $R$ with a canonical integer homomorphism structure `[IntCast R]`, there exists a tail coercion from the integers $\mathbb{Z}$ to $R$.

instCoeHTCTIntOfIntCast instance

[IntCast R] : CoeHTCT Int R

Full source

instance [IntCast R] : CoeHTCT Int R where coe := Int.cast

Head-Tail Coercion from Integers to Type with Integer Homomorphism

Informal description

For any type $R$ with a canonical integer homomorphism structure `[IntCast R]`, there exists a head-tail coercion from the integers $\mathbb{Z}$ to $R$.