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.

T-rounding division

@[extern lean_int_div]

def Int.div : Int → Int → Int

div uses the ["T-rounding"][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.mod_add_div which states that a % b + b * (a / b) = a, unconditionally.

[t-rounding]: https://dl.acm.org/doi/pdf/10.1145/128861.128862 [theo mod_add_div]: https://leanprover-community.github.io/mathlib4_docs/find/?pattern=Int.mod_add_div#doc

Examples:

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

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

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

Implemented by efficient native code.

Equations

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

@[extern lean_int_mod]

def Int.mod : Int → Int → Int

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

Examples:

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

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

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

Implemented by efficient native code.

Equations

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

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

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

theorem Int.ofNat_fdiv (m : Nat) (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