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.

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)

@[reducible, inline, deprecated Int.tdiv]

abbrev Int.div : Int → Int → Int

Equations

• Int.div = Int.tdiv

@[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)

@[reducible, inline, deprecated Int.tmod]

abbrev Int.mod : Int → Int → Int

Equations

• Int.mod = Int.tmod

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

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

E-rounding division

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

@[extern lean_int_ediv]

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:

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

• (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_tdiv (m n : Nat) : ↑(m / n) = (↑m).tdiv ↑n

@[reducible, inline, deprecated Int.ofNat_tdiv]

abbrev Int.ofNat_div (m n : Nat) : ↑(m / n) = (↑m).tdiv ↑n

Equations

• Int.ofNat_div = Int.ofNat_tdiv

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) : 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.

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.

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