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.

@[instance]

inductive pos_num  :
Type

The type of positive binary numbers.

13 = 1101(base 2) = bit1 (bit0 (bit1 one))
@[instance]

Equations
inductive num  :
Type

The type of nonnegative binary numbers, using pos_num.

13 = 1101(base 2) = pos (bit1 (bit0 (bit1 one)))
@[instance]

@[instance]

@[instance]

Equations
@[instance]

Equations
@[instance]

Equations
@[instance]

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

Equations
@[instance]

Equations
@[instance]

Equations
def pos_num.bit  :

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

Equations

The successor of a pos_num.

Equations

Returns a boolean for whether the pos_num is one.

Equations

Addition of two pos_nums.

Equations
def pos_num.pred'  :

The predecessor of a pos_num as a num.

Equations

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

Equations

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

Equations

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

Equations

Multiplication of two pos_nums.

Equations

of_nat_succ n is the pos_num corresponding to n + 1.

Equations
def pos_num.of_nat  :

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

Equations
@[instance]

Equations
@[instance]

Equations
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
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
@[instance]
def pos_num_coe {α : Type u_1} [has_one α] [has_add α] :

Equations
@[instance]
def num_nat_coe {α : Type u_1} [has_one α] [has_add α] [z : has_zero α] :

Equations
@[instance]

Equations
@[instance]

Equations
def num.succ'  :

The successor of a num as a pos_num.

Equations
def num.succ  :
numnum

The successor of a num as a num.

Equations
def num.add  :
numnumnum

Addition of two nums.

Equations
@[instance]

Equations
def num.bit0  :
numnum

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

Equations
def num.bit1  :
numnum

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

Equations
def num.bit  :
boolnumnum

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

Equations
def num.size  :
numnum

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

Equations
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
def num.mul  :
numnumnum

Multiplication of two nums.

Equations
@[instance]

Equations
def num.cmp  :
numnumordering

Ordering of nums.

Equations
@[instance]

Equations
@[instance]

Equations
def num.to_znum  :
numznum

Converts a num to a znum.

Equations
def num.to_znum_neg  :
numznum

Converts x : num to -x : znum.

Equations
def num.of_nat'  :
num

Converts a nat to a num.

Equations
def znum.zneg  :

The negation of a znum.

Equations
@[instance]

Equations
def znum.abs  :
znumnum

The absolute value of a znum as a num.

Equations
def znum.succ  :

The successor of a znum.

Equations
def znum.pred  :

The predecessor of a znum.

Equations
def znum.bit0  :

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

Equations
def znum.bit1  :

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

Equations
def znum.bitm1  :

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

Equations
def znum.of_int'  :
znum

Converts an int to a znum.

Equations
def pos_num.sub'  :

Subtraction of two pos_nums, producing a znum.

Equations

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

Equations

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

Equations

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

Equations
def num.ppred  :

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

Equations
def num.pred  :
numnum

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

Equations
def num.div2  :
numnum

Divides a num by 2

Equations
def num.of_znum'  :

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

Equations
def num.of_znum  :
znumnum

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

Equations
def num.sub'  :
numnumznum

Subtraction of two nums, producing a znum.

Equations
def num.psub  :
numnumoption num

Subtraction of two nums, producing an option num.

Equations
def num.sub  :
numnumnum

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

Equations
@[instance]

Equations
def znum.add  :
znumznumznum

Addition of znums.

Equations
@[instance]

Equations
def znum.mul  :
znumznumznum

Multiplication of znums.

Equations
@[instance]

Equations
@[instance]

Equations
@[instance]

Equations
def pos_num.divmod_aux  :
pos_numnumnumnum × num

Auxiliary definition for pos_num.divmod.

Equations

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

Equations
def pos_num.div'  :

Division of pos_num,

Equations
def pos_num.mod'  :

Modulus of pos_nums.

Equations
def num.div  :
numnumnum

Division of nums, where x / 0 = 0.

Equations
def num.mod  :
numnumnum

Modulus of nums.

Equations
@[instance]

Equations
@[instance]

Equations
def num.gcd_aux  :
numnumnum

Auxiliary definition for num.gcd.

Equations
def num.gcd  :
numnumnum

Greatest Common Divisor (GCD) of two nums.

Equations
def znum.div  :
znumznumznum

Division of znum, where x / 0 = 0.

Equations
def znum.mod  :
znumznumznum

Modulus of znums.

Equations
@[instance]

Equations
@[instance]

Equations
def znum.gcd  :
znumznumnum

Greatest Common Divisor (GCD) of two znums.

Equations
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
@[instance]
def znum_coe {α : Type u_1} [has_zero α] [has_one α] [has_add α] [has_neg α] :

Equations
@[instance]

Equations