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 for the default typeclass instances, 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 div and mod, but have not yet renamed ediv and emod.

E-rounding division

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

@[extern lean_int_ediv]

def Int.ediv : Int → Int → Int

Integer division. This version of integer division 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) -- 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

• (Int.ofNat m).ediv (Int.ofNat n) = Int.ofNat (m / n)
• (Int.ofNat m).ediv (Int.negSucc n) = -Int.ofNat (m / n.succ)
• (Int.negSucc a).ediv 0 = 0
• (Int.negSucc m).ediv (Int.ofNat n.succ) = Int.negSucc (m / n.succ)
• (Int.negSucc m).ediv (Int.negSucc n) = Int.ofNat (m / n.succ).succ

@[extern lean_int_emod]

def Int.emod : Int → Int → Int

Integer modulus. This version of integer modulus 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

• (Int.ofNat m).emod x✝ = Int.ofNat (m % x✝.natAbs)
• (Int.negSucc m).emod x✝ = Int.subNatNat x✝.natAbs (m % x✝.natAbs).succ

instance Int.instDiv : Div Int

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 }

instance Int.instMod : Mod Int

Equations

• Int.instMod = { mod := Int.emod }

@[simp]

theorem Int.ofNat_ediv (m n : Nat) : ↑(m / n) = ↑m / ↑n

theorem Int.ofNat_ediv_ofNat {a b : Nat} : ↑a / ↑b = ↑(a / b)

theorem Int.negSucc_ediv_ofNat_succ {a b : Nat} : negSucc a / ↑(b + 1) = negSucc (a / b.succ)

theorem Int.negSucc_ediv_negSucc {a b : Nat} : negSucc a / negSucc b = ↑(a / (b + 1) + 1)

theorem Int.ofNat_ediv_negSucc {a b : Nat} : ofNat a / negSucc b = -↑(a / (b + 1))

theorem Int.negSucc_emod_ofNat {a b : Nat} : negSucc a % ↑b = subNatNat b (a % b).succ

theorem Int.negSucc_emod_negSucc {a b : Nat} : negSucc a % negSucc b = subNatNat (b + 1) (a % (b + 1)).succ

T-rounding division

@[extern lean_int_div]

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:

#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

• (Int.ofNat m).tdiv (Int.ofNat n) = Int.ofNat (m / n)
• (Int.ofNat m).tdiv (Int.negSucc n) = -Int.ofNat (m / n.succ)
• (Int.negSucc m).tdiv (Int.ofNat n) = -Int.ofNat (m.succ / n)
• (Int.negSucc m).tdiv (Int.negSucc n) = Int.ofNat (m.succ / n.succ)

@[extern lean_int_mod]

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:

#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

• (Int.ofNat m).tmod (Int.ofNat n) = Int.ofNat (m % n)
• (Int.ofNat m).tmod (Int.negSucc n) = Int.ofNat (m % n.succ)
• (Int.negSucc m).tmod (Int.ofNat n) = -Int.ofNat (m.succ % n)
• (Int.negSucc m).tmod (Int.negSucc n) = -Int.ofNat (m.succ % n.succ)

theorem Int.ofNat_tdiv (m n : Nat) : ↑(m / n) = (↑m).tdiv ↑n

F-rounding division

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

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:

#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)

def Int.fmod : Int → Int → Int

Integer modulus. This version of integer modulus 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

• Int.fmod 0 x✝ = 0
• (Int.ofNat m).fmod (Int.ofNat n) = Int.ofNat (m % n)
• (Int.ofNat m.succ).fmod (Int.negSucc n) = Int.subNatNat (m % n.succ) n
• (Int.negSucc m).fmod (Int.ofNat n) = Int.subNatNat n (m % n).succ
• (Int.negSucc m).fmod (Int.negSucc n) = -Int.ofNat (m.succ % n.succ)

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.

Note that unlike emod, fmod, and tmod, bmod takes a natural number as the second argument, rather than an integer.

This function is used in omega as well as signed bitvectors.

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.

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

• x.bmod m = if x % ↑m < (↑m + 1) / 2 then x % ↑m else x % ↑m - ↑m

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.

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

• x.bdiv m = if m = 0 then 0 else let q := x / ↑m; let r := x % ↑m; if r < (↑m + 1) / 2 then q else q + 1