12.2. Integers🔗

The integers are whole numbers, both positive and negative. Integers are arbitrary-precision, limited only by the capability of the hardware on which Lean is running; for fixed-width integers that are used in programming and computer science, please see the section on fixed-precision integers.

Integers are specially supported by Lean's implementation. The logical model of the integers is based on the natural numbers: each integer is modeled as either a natural number or the negative successor of a natural number. Operations on the integers are specified using this model, which is used in the kernel and in interpreted code. In these contexts, integer code inherits the performance benefits of the natural numbers' special support. In compiled code, integers are represented as efficient arbitrary-precision integers, and sufficiently small numbers are stored as unboxed values that don't require indirection through a pointer. Arithmetic operations are implemented by primitives that take advantage of the efficient representations.

12.2.1. Logical Model🔗

Integers are represented either as a natural number or as the negation of the successor of a natural number.

inductive type

Int : Type

The type of integers. It is defined as an inductive type based on the natural number type Nat featuring two constructors: "a natural number is an integer", and "the negation of a successor of a natural number is an integer". The former represents integers between 0 (inclusive) and ∞, and the latter integers between -∞ and -1 (inclusive).

This type is special-cased by the compiler. The runtime has a special representation for Int which stores "small" signed numbers directly, and larger numbers use an arbitrary precision "bignum" library (usually GMP). A "small number" is an integer that can be encoded with 63 bits (31 bits on 32-bits architectures).

Constructors

ofNat : Nat → Int

A natural number is an integer (0 to ∞).

negSucc : Nat → Int

The negation of the successor of a natural number is an integer (-1 to -∞).

This representation of the integers has a number of useful properties. It is relatively simple to use and to understand. Unlike a pair of a sign and a Nat, there is a unique representation for 0, which simplifies reasoning about equality. Integers can also be represented as a pair of natural numbers in which one is subtracted from the other, but this requires a quotient type to be well-behaved, and quotient types can be laborious to work with due to the need to prove that functions respect the equivalence relation.

12.2.2. Run-Time Representation🔗

Like natural numbers, sufficiently-small integers are represented as unboxed values: the lowest-order bit in an object pointer is used to indicate that the value is not, in fact, a pointer. If an integer is too large to fit in the remaining bits, it is instead allocated as an ordinary Lean object that consists of an object header and an arbitrary-precision integer.

12.2.3. Syntax🔗

The OfNat Int instance allows numerals to be used as literals, both in expression and in pattern contexts. (OfNat.ofNat n : Int) reduces to the constructor application Int.ofNat n. The Neg Int instance allows negation to be used as well.

On top of these instances, there is special syntax for the constructor Int.negSucc that is available when the Int namespace is opened. The notation -[ n +1] is suggestive of -(n + 1), which is the meaning of Int.negSucc n.

syntaxNegative Successor

-[ n +1] is notation for Int.negSucc n.

term ::= ...
    | `-[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)`.
-[ term +1]

12.2.4. API Reference

12.2.4.1. Properties

def

Int.sign : Int → Int

Returns the "sign" of the integer as another integer: 1 for positive numbers, -1 for negative numbers, and 0 for 0.

12.2.4.2. Conversions

def

Int.natAbs (m : Int) : Nat

Absolute value (Nat) of an integer.

7#eval (7 : Int).natAbs -- 7
0#eval (0 : Int).natAbs -- 0
11#eval (-11 : Int).natAbs -- 11

Implemented by efficient native code.

def

Int.toNat : Int → Nat

Turns an integer into a natural number, negative numbers become 0.

7#eval (7 : Int).toNat -- 7
0#eval (0 : Int).toNat -- 0
0#eval (-7 : Int).toNat -- 0

def

Int.toNat' : Int → Option Nat

If n : Nat, then int.toNat' n = some n
If n : Int is negative, then int.toNat' n = none.

def

Int.toISize (i : Int) : ISize

def

Int.toInt16 (i : Int) : Int16

def

Int.toInt32 (i : Int) : Int32

def

Int.toInt64 (i : Int) : Int64

def

Int.toInt8 (i : Int) : Int8

def

Int.repr : Int → String

12.2.4.2.1. Casts

type class

IntCast.{u} (R : Type u) : Type u

The canonical homomorphism Int → R. In most use cases R will have a ring structure and this will be a ring homomorphism.

Instance Constructor

IntCast.mk.{u}

Methods

intCast : Int → R

The canonical map Int → R.

def

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

Apply the canonical homomorphism from Int to a type R from an IntCast R instance.

In Mathlib there will be such a homomorphism whenever R is an additive group with a 1.

12.2.4.3. Arithmetic

Typically, arithmetic operations on integers are accessed using Lean's overloaded arithmetic notation. In particular, the instances of Add Int, Neg Int, Sub Int, and Mul Int allow ordinary infix operators to be used. Division is somewhat more intricate, because there are multiple sensible notions of division on integers.

def

Int.add (m n : Int) : Int

Addition of two integers.

13#eval (7 : Int) + (6 : Int) -- 13
0#eval (6 : Int) + (-6 : Int) -- 0

Implemented by efficient native code.

def

Int.sub (m n : Int) : Int

Subtraction of two integers.

57#eval (63 : Int) - (6 : Int) -- 57
7#eval (7 : Int) - (0 : Int) -- 7
-7#eval (0 : Int) - (7 : Int) -- -7

Implemented by efficient native code.

def

Int.subNatNat (m n : Nat) : Int

Subtraction of two natural numbers.

def

Int.neg (n : Int) : Int

Negation of an integer.

Implemented by efficient native code.

def

Int.negOfNat : Nat → Int

Negation of a natural number.

def

Int.mul (m n : Int) : Int

Multiplication of two integers.

378#eval (63 : Int) * (6 : Int) -- 378
-36#eval (6 : Int) * (-6 : Int) -- -36
0#eval (7 : Int) * (0 : Int) -- 0

Implemented by efficient native code.

def

Int.pow (m : Int) : Nat → Int

Power of an integer to some natural number.

16#eval (2 : Int) ^ 4 -- 16
1#eval (10 : Int) ^ 0 -- 1
0#eval (0 : Int) ^ 10 -- 0
-343#eval (-7 : Int) ^ 3 -- -343

def

Int.gcd (m n : Int) : Nat

Computes the greatest common divisor of two integers, as a Nat.

def

Int.lcm (m n : Int) : Nat

Computes the least common multiple of two integers, as a Nat.

12.2.4.3.1. Division🔗

The Div Int and Mod Int instances implement Euclidean division, described in the reference for Int.ediv. This is not, however, the only sensible convention for rounding and remainders in division. Four pairs of division and modulus functions are available, implementing various conventions.

Division by 0

In all integer division conventions, division by 0 is defined to be 0:

0#eval Int.ediv 5 0
0#eval Int.ediv 0 0
0#eval Int.ediv (-5) 0
0#eval Int.bdiv 5 0
0#eval Int.bdiv 0 0
0#eval Int.bdiv (-5) 0
0#eval Int.fdiv 5 0
0#eval Int.fdiv 0 0
0#eval Int.fdiv (-5) 0
0#eval Int.tdiv 5 0
0#eval Int.tdiv 0 0
0#eval Int.tdiv (-5) 0

All evaluate to 0.

def

Int.ediv : Int → Int → Int

Integer division. This version of Int.div uses the E-rounding convention (euclidean division), in which Int.emod x y satisfies 0 ≤ mod x y < natAbs y for y ≠ 0 and Int.ediv is the unique function satisfying emod x y + (ediv x y) * y = x.

This is the function powering the / notation on integers.

Examples:

0#eval (7 : Int) / (0 : Int) -- 0
0#eval (0 : Int) / (7 : Int) -- 0

2#eval (12 : Int) / (6 : Int) -- 2
-2#eval (12 : Int) / (-6 : Int) -- -2
-2#eval (-12 : Int) / (6 : Int) -- -2
2#eval (-12 : Int) / (-6 : Int) -- 2

1#eval (12 : Int) / (7 : Int) -- 1
-1#eval (12 : Int) / (-7 : Int) -- -1
-2#eval (-12 : Int) / (7 : Int) -- -2
2#eval (-12 : Int) / (-7 : Int) -- 2

Implemented by efficient native code.

def

Int.emod : Int → Int → Int

Integer modulus. This version of Int.mod uses the E-rounding convention (euclidean division), in which Int.emod x y satisfies 0 ≤ emod x y < natAbs y for y ≠ 0 and Int.ediv is the unique function satisfying emod x y + (ediv x y) * y = x.

This is the function powering the % notation on integers.

Examples:

7#eval (7 : Int) % (0 : Int) -- 7
0#eval (0 : Int) % (7 : Int) -- 0

0#eval (12 : Int) % (6 : Int) -- 0
0#eval (12 : Int) % (-6 : Int) -- 0
0#eval (-12 : Int) % (6 : Int) -- 0
0#eval (-12 : Int) % (-6 : Int) -- 0

5#eval (12 : Int) % (7 : Int) -- 5
5#eval (12 : Int) % (-7 : Int) -- 5
2#eval (-12 : Int) % (7 : Int) -- 2
2#eval (-12 : Int) % (-7 : Int) -- 2

Implemented by efficient native code.

def

Int.bdiv (x : Int) (m : Nat) : Int

Balanced division. This returns the unique integer so that b * (Int.bdiv a b) + Int.bmod a b = a.

def

Int.bmod (x : Int) (m : Nat) : Int

Balanced modulus. This version of Integer modulus uses the balanced rounding convention, which guarantees that m/2 ≤ bmod x m < m/2 for m ≠ 0 and bmod x m is congruent to x modulo m.

If m = 0, then bmod x m = x.

def

Int.fdiv : Int → Int → Int

Integer division. This version of division uses the F-rounding convention (flooring division), in which Int.fdiv x y satisfies fdiv x y = floor (x / y) and Int.fmod is the unique function satisfying fmod x y + (fdiv x y) * y = x.

Examples:

0#eval (7 : Int).fdiv (0 : Int) -- 0
0#eval (0 : Int).fdiv (7 : Int) -- 0

2#eval (12 : Int).fdiv (6 : Int) -- 2
-2#eval (12 : Int).fdiv (-6 : Int) -- -2
-2#eval (-12 : Int).fdiv (6 : Int) -- -2
2#eval (-12 : Int).fdiv (-6 : Int) -- 2

1#eval (12 : Int).fdiv (7 : Int) -- 1
-2#eval (12 : Int).fdiv (-7 : Int) -- -2
-2#eval (-12 : Int).fdiv (7 : Int) -- -2
1#eval (-12 : Int).fdiv (-7 : Int) -- 1

def

Int.fmod : Int → Int → Int

Integer modulus. This version of Int.mod uses the F-rounding convention (flooring division), in which Int.fdiv x y satisfies fdiv x y = floor (x / y) and Int.fmod is the unique function satisfying fmod x y + (fdiv x y) * y = x.

Examples:

7#eval (7 : Int).fmod (0 : Int) -- 7
0#eval (0 : Int).fmod (7 : Int) -- 0

0#eval (12 : Int).fmod (6 : Int) -- 0
0#eval (12 : Int).fmod (-6 : Int) -- 0
0#eval (-12 : Int).fmod (6 : Int) -- 0
0#eval (-12 : Int).fmod (-6 : Int) -- 0

5#eval (12 : Int).fmod (7 : Int) -- 5
-2#eval (12 : Int).fmod (-7 : Int) -- -2
2#eval (-12 : Int).fmod (7 : Int) -- 2
-5#eval (-12 : Int).fmod (-7 : Int) -- -5

def

Int.tdiv : Int → Int → Int

tdiv uses the "T-rounding" (Truncation-rounding) convention, meaning that it rounds toward zero. Also note that division by zero is defined to equal zero.

The relation between integer division and modulo is found in Int.tmod_add_tdiv which states that tmod a b + b * (tdiv a b) = a, unconditionally.

Examples:

0#eval (7 : Int).tdiv (0 : Int) -- 0
0#eval (0 : Int).tdiv (7 : Int) -- 0

2#eval (12 : Int).tdiv (6 : Int) -- 2
-2#eval (12 : Int).tdiv (-6 : Int) -- -2
-2#eval (-12 : Int).tdiv (6 : Int) -- -2
2#eval (-12 : Int).tdiv (-6 : Int) -- 2

1#eval (12 : Int).tdiv (7 : Int) -- 1
-1#eval (12 : Int).tdiv (-7 : Int) -- -1
-1#eval (-12 : Int).tdiv (7 : Int) -- -1
1#eval (-12 : Int).tdiv (-7 : Int) -- 1

Implemented by efficient native code.

def

Int.tmod : Int → Int → Int

Integer modulo. This function uses the "T-rounding" (Truncation-rounding) convention to pair with Int.tdiv, meaning that tmod a b + b * (tdiv a b) = a unconditionally (see Int.tmod_add_tdiv). In particular, a % 0 = a.

Examples:

7#eval (7 : Int).tmod (0 : Int) -- 7
0#eval (0 : Int).tmod (7 : Int) -- 0

0#eval (12 : Int).tmod (6 : Int) -- 0
0#eval (12 : Int).tmod (-6 : Int) -- 0
0#eval (-12 : Int).tmod (6 : Int) -- 0
0#eval (-12 : Int).tmod (-6 : Int) -- 0

5#eval (12 : Int).tmod (7 : Int) -- 5
5#eval (12 : Int).tmod (-7 : Int) -- 5
-5#eval (-12 : Int).tmod (7 : Int) -- -5
-5#eval (-12 : Int).tmod (-7 : Int) -- -5

Implemented by efficient native code.

12.2.4.4. Bitwise Operators

Bitwise operators on Int can be understood as bitwise operators on an infinite stream of bits that are the twos-complement representation of integers.

def

Int.not : Int → Int

Bitwise not

Interprets the integer as an infinite sequence of bits in two's complement and complements each bit.

~~~(0:Int) = -1
~~~(1:Int) = -2
~~~(-1:Int) = 0

def

Int.shiftRight : Int → Nat → Int

Bitwise shift right.

Conceptually, this treats the integer as an infinite sequence of bits in two's complement and shifts the value to the right.

( 0b0111:Int) >>> 1 =  0b0011
( 0b1000:Int) >>> 1 =  0b0100
(-0b1000:Int) >>> 1 = -0b0100
(-0b0111:Int) >>> 1 = -0b0100

12.2.4.5. Comparisons

Equality and inequality tests on Int are typically performed using the decidability of its equality and ordering relations or using the BEq Int and Ord Int instances.

def

Int.le (a b : Int) : Prop

Definition of a ≤ b, encoded as b - a ≥ 0.

def

Int.lt (a b : Int) : Prop

Definition of a < b, encoded as a + 1 ≤ b.

def

Int.decEq (a b : Int) : Decidable (a = b)

Decides equality between two Ints.

true#eval (7 : Int) = (3 : Int) + (4 : Int) -- true
true#eval (6 : Int) = (3 : Int) * (2 : Int) -- true
true#eval ¬ (6 : Int) = (3 : Int) -- true

Implemented by efficient native code.

12.2.4.6. Proof Automation

The functions in this section are primarily parts of the implementation of simplification rules employed by simp. They are probably only of interest to users who are implementing custom proof automation that involves integers.

def

Int.fromExpr? (e : Lean.Expr)
    : Lean.Meta.SimpM (Option Int)

def

Int.isPosValue : Lean.Meta.Simp.DSimproc

Return .done for positive Int values. We don't want to unfold in the symbolic evaluator.

def

Int.reduceAbs : Lean.Meta.Simp.DSimproc

def

Int.reduceAdd : Lean.Meta.Simp.DSimproc

def

Int.reduceBEq : Lean.Meta.Simp.DSimproc

def

Int.reduceBNe : Lean.Meta.Simp.DSimproc

def

Int.reduceBdiv : Lean.Meta.Simp.DSimproc

def

Int.reduceBin (declName : Lean.Name)
    (arity : Nat) (op : Int → Int → Int)
    (e : Lean.Expr)
    : Lean.Meta.SimpM Lean.Meta.Simp.DStep

def

Int.reduceBinIntNatOp (name : Lean.Name)
    (op : Int → Nat → Int) (e : Lean.Expr)
    : Lean.Meta.SimpM Lean.Meta.Simp.DStep

def

Int.reduceBinPred (declName : Lean.Name)
    (arity : Nat) (op : Int → Int → Bool)
    (e : Lean.Expr)
    : Lean.Meta.SimpM Lean.Meta.Simp.Step

def

Int.reduceBmod : Lean.Meta.Simp.DSimproc

def

Int.reduceBoolPred (declName : Lean.Name)
    (arity : Nat) (op : Int → Int → Bool)
    (e : Lean.Expr)
    : Lean.Meta.SimpM Lean.Meta.Simp.DStep

def

Int.reduceDiv : Lean.Meta.Simp.DSimproc

def

Int.reduceEq : Lean.Meta.Simp.Simproc

def

Int.reduceFDiv : Lean.Meta.Simp.DSimproc

def

Int.reduceFMod : Lean.Meta.Simp.DSimproc

def

Int.reduceGE : Lean.Meta.Simp.Simproc

def

Int.reduceGT : Lean.Meta.Simp.Simproc

def

Int.reduceLE : Lean.Meta.Simp.Simproc

def

Int.reduceLT : Lean.Meta.Simp.Simproc

def

Int.reduceMod : Lean.Meta.Simp.DSimproc

def

Int.reduceMul : Lean.Meta.Simp.DSimproc

def

Int.reduceNatCore (declName : Lean.Name)
    (op : Int → Nat) (e : Lean.Expr)
    : Lean.Meta.SimpM Lean.Meta.Simp.DStep

def

Int.reduceNe : Lean.Meta.Simp.Simproc

def

Int.reduceNeg : Lean.Meta.Simp.DSimproc

def

Int.reduceNegSucc : Lean.Meta.Simp.DSimproc

def

Int.reduceOfNat : Lean.Meta.Simp.DSimproc

def

Int.reducePow : Lean.Meta.Simp.DSimproc

def

Int.reduceSub : Lean.Meta.Simp.DSimproc

def

Int.reduceTDiv : Lean.Meta.Simp.DSimproc

def

Int.reduceTMod : Lean.Meta.Simp.DSimproc

def

Int.reduceToNat : Lean.Meta.Simp.DSimproc

def

Int.reduceUnary (declName : Lean.Name)
    (arity : Nat) (op : Int → Int)
    (e : Lean.Expr)
    : Lean.Meta.SimpM Lean.Meta.Simp.DStep