Documentation

Init.Data.Int.DivMod.Basic

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 SMT-LIB, 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]

Int → Int → Int

Integer division that uses the E-rounding convention. Usually accessed via the / operator. Division by zero is defined to be zero, rather than an error.

In the E-rounding convention (Euclidean division), Int.emod x y satisfies 0 ≤ Int.emod x y < Int.natAbs y for y ≠ 0 and Int.ediv is the unique function satisfying Int.emod x y + (Int.edivx y) * y = x for y ≠ 0.

This means that Int.ediv x y is ⌊x / y⌋ when y > 0 and ⌈x / y⌉ when y < 0.

This function is overridden by the compiler with an efficient implementation. This definition is the logical model.

Examples:

(7 : Int) / (0 : Int) = 0
(0 : Int) / (7 : Int) = 0
(12 : Int) / (6 : Int) = 2
(12 : Int) / (-6 : Int) = -2
(-12 : Int) / (6 : Int) = -2
(-12 : Int) / (-6 : Int) = 2
(12 : Int) / (7 : Int) = 1
(12 : Int) / (-7 : Int) = -1
(-12 : Int) / (7 : Int) = -2
(-12 : Int) / (-7 : Int) = 2

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

Instances For

@[extern lean_int_emod]

Int → Int → Int

Integer modulus that uses the E-rounding convention. Usually accessed via the % operator.

In the E-rounding convention (Euclidean division), Int.emod x y satisfies 0 ≤ Int.emod x y < Int.natAbs y for y ≠ 0 and Int.ediv is the unique function satisfying Int.emod x y + (Int.edivx y) * y = x for y ≠ 0.

This function is overridden by the compiler with an efficient implementation. This definition is the logical model.

Examples:

(7 : Int) % (0 : Int) = 7
(0 : Int) % (7 : Int) = 0
(12 : Int) % (6 : Int) = 0
(12 : Int) % (-6 : Int) = 0
(-12 : Int) % (6 : Int) = 0
(-12 : Int) % (-6 : Int) = 0
(12 : Int) % (7 : Int) = 5
(12 : Int) % (-7 : Int) = 5
(-12 : Int) % (7 : Int) = 2
(-12 : Int) % (-7 : Int) = 2

Equations

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

Instances For

instance Int.instDiv :

The Div Int and Mod Int instances use Int.ediv and Int.emod for compatibility with SMT-LIB and because mathematical reasoning tends to be easier.

Equations

Int.instDiv = { div := Int.ediv }

instance Int.instMod :

The Div Int and Mod Int instances use Int.ediv and Int.emod for compatibility with SMT-LIB and because mathematical reasoning tends to be easier.

Equations

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

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]

Int → Int → Int

Integer division using the T-rounding convention.

In the T-rounding convention (division with truncation), all rounding is towards zero. Division by 0 is defined to be 0. In this convention, Int.tmod a b + b * (Int.tdiv a b) = a.

This function is overridden by the compiler with an efficient implementation. This definition is the logical model.

Examples:

(7 : Int).tdiv (0 : Int) = 0
(0 : Int).tdiv (7 : Int) = 0
(12 : Int).tdiv (6 : Int) = 2
(12 : Int).tdiv (-6 : Int) = -2
(-12 : Int).tdiv (6 : Int) = -2
(-12 : Int).tdiv (-6 : Int) = 2
(12 : Int).tdiv (7 : Int) = 1
(12 : Int).tdiv (-7 : Int) = -1
(-12 : Int).tdiv (7 : Int) = -1
(-12 : Int).tdiv (-7 : Int) = 1

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)

Instances For

@[extern lean_int_mod]

Int → Int → Int

Integer modulo using the T-rounding convention.

In the T-rounding convention (division with truncation), all rounding is towards zero. Division by 0 is defined to be 0 and Int.tmod a 0 = a.

In this convention, Int.tmod a b + b * (Int.tdiv a b) = a. Additionally, Int.natAbs (Int.tmod a b) = Int.natAbs a % Int.natAbs b, and when b does not divide a, Int.tmod a b has the same sign as a.

This function is overridden by the compiler with an efficient implementation. This definition is the logical model.

Examples:

(7 : Int).tmod (0 : Int) = 7
(0 : Int).tmod (7 : Int) = 0
(12 : Int).tmod (6 : Int) = 0
(12 : Int).tmod (-6 : Int) = 0
(-12 : Int).tmod (6 : Int) = 0
(-12 : Int).tmod (-6 : Int) = 0
(12 : Int).tmod (7 : Int) = 5
(12 : Int).tmod (-7 : Int) = 5
(-12 : Int).tmod (7 : Int) = -5
(-12 : Int).tmod (-7 : Int) = -5

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)

Instances For

theorem Int.ofNat_tdiv (m n : Nat) :

↑(m / n) = (↑m).tdiv ↑n

F-rounding division #

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

Int → Int → Int

Integer division using the F-rounding convention.

In the F-rounding convention (flooring division), Int.fdiv x y satisfies Int.fdiv x y = ⌊x / y⌋ and Int.fmod is the unique function satisfying Int.fmod x y + (Int.fdiv x y) * y = x.

Examples:

(7 : Int).fdiv (0 : Int) = 0
(0 : Int).fdiv (7 : Int) = 0
(12 : Int).fdiv (6 : Int) = 2
(12 : Int).fdiv (-6 : Int) = -2
(-12 : Int).fdiv (6 : Int) = -2
(-12 : Int).fdiv (-6 : Int) = 2
(12 : Int).fdiv (7 : Int) = 1
(12 : Int).fdiv (-7 : Int) = -2
(-12 : Int).fdiv (7 : Int) = -2
(-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)

Instances For

Int → Int → Int

Integer modulus using the F-rounding convention.

In the F-rounding convention (flooring division), Int.fdiv x y satisfies Int.fdiv x y = ⌊x / y⌋ and Int.fmod is the unique function satisfying Int.fmod x y + (Int.fdiv x y) * y = x.

Examples:

(7 : Int).fmod (0 : Int) = 7
(0 : Int).fmod (7 : Int) = 0
(12 : Int).fmod (6 : Int) = 0
(12 : Int).fmod (-6 : Int) = 0
(-12 : Int).fmod (6 : Int) = 0
(-12 : Int).fmod (-6 : Int) = 0
(12 : Int).fmod (7 : Int) = 5
(12 : Int).fmod (-7 : Int) = -2
(-12 : Int).fmod (7 : Int) = 2
(-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)

Instances For

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

Balanced modulus.

This version of integer modulus uses the balanced rounding convention, which guarantees that -m / 2 ≤ Int.bmod x m < m/2 for m ≠ 0 and Int.bmod x m is congruent to x modulo m.

If m = 0, then Int.bmod x m = x.

Examples:

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

Equations

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

Instances For

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:

(7 : Int).bdiv 0 = 0
(0 : Int).bdiv 7 = 0
(12 : Int).bdiv 6 = 2
(12 : Int).bdiv 7 = 2
(12 : Int).bdiv 8 = 2
(12 : Int).bdiv 9 = 1
(-12 : Int).bdiv 6 = -2
(-12 : Int).bdiv 7 = -2
(-12 : Int).bdiv 8 = -1
(-12 : Int).bdiv 9 = -1

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

Instances For