-[n+1]
is suggestive notation for negSucc n
, which is the second constructor of
Int
for making strictly negative numbers by mapping n : Nat
to -(n + 1)
.
Equations
- One or more equations did not get rendered due to their size.
toNat' #
- If
n : Nat
, thenint.toNat' n = some n
- If
n : Int
is negative, thenint.toNat' n = none
.
Equations
- Int.toNat' x = match x with | Int.ofNat n => some n | Int.negSucc a => none
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
.
E-rounding division #
This pair satisfies 0 ≤ mod x y < natAbs y≤ mod x y < natAbs y
for y ≠ 0≠ 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≤ mod x y < natAbs y
for y ≠ 0≠ 0
and Int.ediv
is the unique function satisfying emod x y + (ediv x y) * y = x
.
Equations
- One or more equations did not get rendered due to their size.
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≤ emod x y < natAbs y
for y ≠ 0≠ 0
and Int.ediv
is the unique function satisfying emod x y + (ediv x y) * y = x
.
Equations
- Int.emod x x = match x, x with | Int.ofNat m, n => Int.ofNat (m % Int.natAbs n) | Int.negSucc m, n => Int.subNatNat (Int.natAbs n) (Nat.succ (m % Int.natAbs n))
F-rounding division #
This pair satisfies fdiv x y = floor (x / y)
.
T-rounding division #
This pair satisfies div x y = round_to_zero (x / y)
.
Int.div
and Int.mod
are defined in core lean.
Core Lean provides instances using T-rounding division, i.e. Int.div
and Int.mod
.
We override these here.
Equations
- Int.instDivInt_1 = { div := Int.ediv }
gcd #
divisibility #
Divisibility of integers. a ∣ b∣ b
(typed as \|
) says that
there is some c
such that b = a * c
.
Equations
- Int.instDvdInt = { dvd := fun a b => ∃ c, b = a * c }