Documentation

Init.Data.Int.DivMod

Quotient and remainder #

There are three main conventions for integer division, referred here as the E, F, T rounding conventions. All three pairs satisfy the identity x % y + (x / y) * y = x unconditionally, and satisfy x / 0 = 0 and x % 0 = x.

Historical notes #

In early versions of Lean, the typeclasses provided by / and % were defined in terms of tdiv and tmod, and these were named simply as div and mod.

However we decided it was better to use ediv and emod, as they are consistent with the conventions used in SMTLib, and Mathlib, and often mathematical reasoning is easier with these conventions.

At that time, we did not rename div and mod to tdiv and tmod (along with all their lemma). In September 2024, we decided to do this rename (with deprecations in place), and later we intend to rename ediv and emod to div and mod, as nearly all users will only ever need to use these functions and their associated lemmas.

In December 2024, we removed tdiv and tmod, but have not yet renamed ediv and emod.

T-rounding division #

@[extern lean_int_div]
def Int.tdiv :
IntIntInt

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:

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

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

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

Implemented by efficient native code.

Equations
@[extern lean_int_mod]
def Int.tmod :
IntIntInt

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:

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

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

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

Implemented by efficient native code.

Equations

F-rounding division #

This pair satisfies fdiv x y = floor (x / y).

def Int.fdiv :
IntIntInt

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:

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

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

#eval (12 : Int).fdiv (7 : Int) -- 1
#eval (12 : Int).fdiv (-7 : Int) -- -2
#eval (-12 : Int).fdiv (7 : Int) -- -2
#eval (-12 : Int).fdiv (-7 : Int) -- 1
Equations
def Int.fmod :
IntIntInt

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:

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

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

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

E-rounding division #

This pair satisfies 0 ≤ mod x y < natAbs y for y ≠ 0.

@[extern lean_int_ediv]
def Int.ediv :
IntIntInt

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:

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

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

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

Implemented by efficient native code.

Equations
@[extern lean_int_emod]
def Int.emod :
IntIntInt

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:

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

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

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

Implemented by efficient native code.

Equations
instance Int.instDiv :

The Div and Mod syntax uses ediv and emod for compatibility with SMTLIb and mathematical reasoning tends to be easier.

Equations
instance Int.instMod :
Equations
@[simp]
theorem Int.ofNat_ediv (m n : Nat) :
↑(m / n) = m / n
theorem Int.ofNat_tdiv (m n : Nat) :
↑(m / n) = (↑m).tdiv n
theorem Int.ofNat_fdiv (m n : Nat) :
↑(m / n) = (↑m).fdiv n

bmod ("balanced" mod) #

Balanced mod (and balanced div) are a division and modulus pair such that b * (Int.bdiv a b) + Int.bmod a b = a and -b/2 ≤ Int.bmod a b < b/2 for all a : Int and b > 0.

This is used in Omega as well as signed bitvectors.

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

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.

Examples:

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

#eval (12 : Int).bdiv 6 -- 2
#eval (12 : Int).bdiv 7 -- 2
#eval (12 : Int).bdiv 8 -- 2
#eval (12 : Int).bdiv 9 -- 1

#eval (-12 : Int).bdiv 6 -- -2
#eval (-12 : Int).bdiv 7 -- -2
#eval (-12 : Int).bdiv 8 -- -1
#eval (-12 : Int).bdiv 9 -- -1
Equations
def Int.bdiv (x : Int) (m : Nat) :

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

Examples:

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

#eval (12 : Int).bmod 6 -- 0
#eval (12 : Int).bmod 7 -- -2
#eval (12 : Int).bmod 8 -- -4
#eval (12 : Int).bmod 9 -- 3

#eval (-12 : Int).bmod 6 -- 0
#eval (-12 : Int).bmod 7 -- 2
#eval (-12 : Int).bmod 8 -- -4
#eval (-12 : Int).bmod 9 -- -3
Equations