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 #
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.
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.
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
- Int.fdiv 0 x✝ = 0
- (Int.ofNat m).fdiv (Int.ofNat n) = Int.ofNat (m / n)
- (Int.ofNat m.succ).fdiv (Int.negSucc n) = Int.negSucc (m / n.succ)
- (Int.negSucc a).fdiv 0 = 0
- (Int.negSucc m).fdiv (Int.ofNat n.succ) = Int.negSucc (m / n.succ)
- (Int.negSucc m).fdiv (Int.negSucc n) = Int.ofNat (m.succ / n.succ)
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
E-rounding division #
This pair satisfies 0 ≤ mod x y < natAbs y
for y ≠ 0
.
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.
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.
The Div and Mod syntax uses ediv and emod for compatibility with SMTLIb and mathematical reasoning tends to be easier.
Equations
- Int.instDiv = { div := Int.ediv }
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.
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
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