mathlib documentation

data.num.basic

Binary representation of integers using inductive types #

Note: Unlike in Coq, where this representation is preferred because of the reliance on kernel reduction, in Lean this representation is discouraged in favor of the "Peano" natural numbers nat, and the purpose of this collection of theorems is to show the equivalence of the different approaches.

source
@[protected, instance]
meta def pos_num.has_reflect  :
has_reflect pos_num
source
inductive pos_num  :
Type

The type of positive binary numbers.

13 = 1101(base 2) = bit1 (bit0 (bit1 one))
source
@[protected, instance]
def pos_num.decidable_eq  :
decidable_eq pos_num
source
@[protected, instance]
def pos_num.has_one  :
has_one pos_num
Equations
source
@[protected, instance]
def pos_num.inhabited  :
inhabited pos_num
Equations
source
inductive num  :
Type

The type of nonnegative binary numbers, using pos_num.

13 = 1101(base 2) = pos (bit1 (bit0 (bit1 one)))
source
@[protected, instance]
def num.decidable_eq  :
decidable_eq num
source
@[protected, instance]
meta def num.has_reflect  :
has_reflect num
source
@[protected, instance]
def num.has_zero  :
has_zero num
Equations
source
@[protected, instance]
def num.has_one  :
has_one num
Equations
source
@[protected, instance]
def num.inhabited  :
inhabited num
Equations
source
@[protected, instance]
def znum.decidable_eq  :
decidable_eq znum
source
@[protected, instance]
meta def znum.has_reflect  :
has_reflect znum
source
inductive znum  :
Type

Representation of integers using trichotomy around zero.

13 = 1101(base 2) = pos (bit1 (bit0 (bit1 one)))
-13 = -1101(base 2) = neg (bit1 (bit0 (bit1 one)))
source
@[protected, instance]
def znum.has_zero  :
has_zero znum
Equations
source
@[protected, instance]
def znum.has_one  :
has_one znum
Equations
source
@[protected, instance]
def znum.inhabited  :
inhabited znum
Equations
source
def pos_num.bit (b : bool) :
pos_num → pos_num

bit b n appends the bit b to the end of n, where bit tt x = x1 and bit ff x = x0.

Equations
source
def pos_num.succ  :
pos_num → pos_num

The successor of a pos_num.

Equations
source
def pos_num.is_one  :
pos_num → bool

Returns a boolean for whether the pos_num is one.

Equations
source
@[protected]
def pos_num.add  :
pos_num → pos_num → pos_num

Addition of two pos_nums.

Equations
source
@[protected, instance]
def pos_num.has_add  :
has_add pos_num
Equations
source
def pos_num.pred'  :
pos_num → num

The predecessor of a pos_num as a num.

Equations
source
def pos_num.pred (a : pos_num) :
pos_num

The predecessor of a pos_num as a pos_num. This means that pred 1 = 1.

Equations
source
def pos_num.size  :
pos_num → pos_num

The number of bits of a pos_num, as a pos_num.

Equations
source
def pos_num.nat_size  :
pos_num → ℕ

The number of bits of a pos_num, as a nat.

Equations
source
@[protected]
def pos_num.mul (a : pos_num) :
pos_num → pos_num

Multiplication of two pos_nums.

Equations
source
@[protected, instance]
def pos_num.has_mul  :
has_mul pos_num
Equations
source
def pos_num.of_nat_succ  :
ℕ → pos_num

of_nat_succ n is the pos_num corresponding to n + 1.

Equations
source
def pos_num.of_nat (n : ℕ) :
pos_num

of_nat n is the pos_num corresponding to n, except for of_nat 0 = 1.

Equations
source
def pos_num.cmp  :
pos_num → pos_num → ordering

Ordering of pos_nums.

Equations
source
@[protected, instance]
def pos_num.has_lt  :
has_lt pos_num
Equations
source
@[protected, instance]
def pos_num.has_le  :
has_le pos_num
Equations
source
@[protected, instance]
def pos_num.decidable_lt  :
decidable_rel has_lt.lt
Equations
source
@[protected, instance]
def pos_num.decidable_le  :
decidable_rel has_le.le
Equations
source
def cast_pos_num {α : Type u_1} [has_one α] [has_add α] :
pos_num → α

cast_pos_num casts a pos_num into any type which has 1 and +.

Equations
source
def cast_num {α : Type u_1} [has_one α] [has_add α] [z : has_zero α] :
num → α

cast_num casts a num into any type which has 0, 1 and +.

Equations
source
@[protected, instance]
def pos_num_coe {α : Type u_1} [has_one α] [has_add α] :
has_coe_t pos_num α
Equations
source
@[protected, instance]
def num_nat_coe {α : Type u_1} [has_one α] [has_add α] [z : has_zero α] :
has_coe_t num α
Equations
source
@[protected, instance]
def pos_num.has_repr  :
has_repr pos_num
Equations
source
@[protected, instance]
def num.has_repr  :
has_repr num
Equations
source
def num.succ'  :
num → pos_num

The successor of a num as a pos_num.

Equations
source
def num.succ (n : num) :
num

The successor of a num as a num.

Equations
source
@[protected]
def num.add  :
num → num → num

Addition of two nums.

Equations
source
@[protected, instance]
def num.has_add  :
has_add num
Equations
source
@[protected]
def num.bit0  :
num → num

bit0 n appends a 0 to the end of n, where bit0 n = n0.

Equations
source
@[protected]
def num.bit1  :
num → num

bit1 n appends a 1 to the end of n, where bit1 n = n1.

Equations
source
def num.bit (b : bool) :
num → num

bit b n appends the bit b to the end of n, where bit tt x = x1 and bit ff x = x0.

Equations
source
def num.size  :
num → num

The number of bits required to represent a num, as a num. size 0 is defined to be 0.

Equations
source
def num.nat_size  :
num → ℕ

The number of bits required to represent a num, as a nat. size 0 is defined to be 0.

Equations
source
@[protected]
def num.mul  :
num → num → num

Multiplication of two nums.

Equations
source
@[protected, instance]
def num.has_mul  :
has_mul num
Equations
source
def num.cmp  :
num → num → ordering

Ordering of nums.

Equations
source
@[protected, instance]
def num.has_lt  :
has_lt num
Equations
source
@[protected, instance]
def num.has_le  :
has_le num
Equations
source
@[protected, instance]
def num.decidable_lt  :
decidable_rel has_lt.lt
Equations
source
@[protected, instance]
def num.decidable_le  :
decidable_rel has_le.le
Equations
source
def num.to_znum  :
num → znum

Converts a num to a znum.

Equations
source
def num.to_znum_neg  :
num → znum

Converts x : num to -x : znum.

Equations
source
def num.of_nat'  :
ℕ → num

Converts a nat to a num.

Equations
source
def znum.zneg  :
znum → znum

The negation of a znum.

Equations
source
@[protected, instance]
def znum.has_neg  :
has_neg znum
Equations
source
def znum.abs  :
znum → num

The absolute value of a znum as a num.

Equations
source
def znum.succ  :
znum → znum

The successor of a znum.

Equations
source
def znum.pred  :
znum → znum

The predecessor of a znum.

Equations
source
@[protected]
def znum.bit0  :
znum → znum

bit0 n appends a 0 to the end of n, where bit0 n = n0.

Equations
source
@[protected]
def znum.bit1  :
znum → znum

bit1 x appends a 1 to the end of x, mapping x to 2 * x + 1.

Equations
source
@[protected]
def znum.bitm1  :
znum → znum

bitm1 x appends a 1 to the end of x, mapping x to 2 * x - 1.

Equations
source
def znum.of_int'  :
ℤ → znum

Converts an int to a znum.

Equations
source
def pos_num.sub'  :
pos_num → pos_num → znum

Subtraction of two pos_nums, producing a znum.

Equations
source
def pos_num.of_znum'  :
znum → option pos_num

Converts a znum to option pos_num, where it is some if the znum was positive and none otherwise.

Equations
source
def pos_num.of_znum  :
znum → pos_num

Converts a znum to a pos_num, mapping all out of range values to 1.

Equations
source
@[protected]
def pos_num.sub (a b : pos_num) :
pos_num

Subtraction of pos_nums, where if a < b, then a - b = 1.

Equations
source
@[protected, instance]
def pos_num.has_sub  :
has_sub pos_num
Equations
source
def num.ppred  :
num → option num

The predecessor of a num as an option num, where ppred 0 = none

Equations
source
def num.pred  :
num → num

The predecessor of a num as a num, where pred 0 = 0.

Equations
source
def num.div2  :
num → num

Divides a num by 2

Equations
source
def num.of_znum'  :
znum → option num

Converts a znum to an option num, where of_znum' p = none if p < 0.

Equations
source
def num.of_znum  :
znum → num

Converts a znum to an option num, where of_znum p = 0 if p < 0.

Equations
source
def num.sub'  :
num → num → znum

Subtraction of two nums, producing a znum.

Equations
source
def num.psub (a b : num) :
option num

Subtraction of two nums, producing an option num.

Equations
source
@[protected]
def num.sub (a b : num) :
num

Subtraction of two nums, where if a < b, a - b = 0.

Equations
source
@[protected, instance]
def num.has_sub  :
has_sub num
Equations
source
@[protected]
def znum.add  :
znum → znum → znum

Addition of znums.

Equations
source
@[protected, instance]
def znum.has_add  :
has_add znum
Equations
source
@[protected]
def znum.mul  :
znum → znum → znum

Multiplication of znums.

Equations
source
@[protected, instance]
def znum.has_mul  :
has_mul znum
Equations
source
def znum.cmp  :
znum → znum → ordering

Ordering on znums.

Equations
source
@[protected, instance]
def znum.has_lt  :
has_lt znum
Equations
source
@[protected, instance]
def znum.has_le  :
has_le znum
Equations
source
@[protected, instance]
def znum.decidable_lt  :
decidable_rel has_lt.lt
Equations
source
@[protected, instance]
def znum.decidable_le  :
decidable_rel has_le.le
Equations
source
def pos_num.divmod_aux (d : pos_num) (q r : num) :
num × num

Auxiliary definition for pos_num.divmod.

Equations
source
def pos_num.divmod (d : pos_num) :
pos_num → num × num

divmod x y = (y / x, y % x).

Equations
source
def pos_num.div' (n d : pos_num) :
num

Division of pos_num,

Equations
source
def pos_num.mod' (n d : pos_num) :
num

Modulus of pos_nums.

Equations
source
def num.div  :
num → num → num

Division of nums, where x / 0 = 0.

Equations
source
def num.mod  :
num → num → num

Modulus of nums.

Equations
source
@[protected, instance]
def num.has_div  :
has_div num
Equations
source
@[protected, instance]
def num.has_mod  :
has_mod num
Equations
source
def num.gcd_aux  :
ℕ → num → num → num

Auxiliary definition for num.gcd.

Equations
source
def num.gcd (a b : num) :
num

Greatest Common Divisor (GCD) of two nums.

Equations
source
def znum.div  :
znum → znum → znum

Division of znum, where x / 0 = 0.

Equations
source
def znum.mod  :
znum → znum → znum

Modulus of znums.

Equations
source
@[protected, instance]
def znum.has_div  :
has_div znum
Equations
source
@[protected, instance]
def znum.has_mod  :
has_mod znum
Equations
source
def znum.gcd (a b : znum) :
num

Greatest Common Divisor (GCD) of two znums.

Equations
source
def cast_znum {α : Type u_1} [has_zero α] [has_one α] [has_add α] [has_neg α] :
znum → α

cast_znum casts a znum into any type which has 0, 1, + and neg

Equations
source
@[protected, instance]
def znum_coe {α : Type u_1} [has_zero α] [has_one α] [has_add α] [has_neg α] :
has_coe_t znum α
Equations
source
@[protected, instance]
def znum.has_repr  :
has_repr znum
Equations