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.

@[protected, instance]
inductive pos_num  :
Type

The type of positive binary numbers.

13 = 1101(base 2) = bit1 (bit0 (bit1 one))

Instances for pos_num
@[protected, instance]
@[protected, instance]
Equations
@[protected, instance]
Equations
inductive num  :
Type
• zero : num
• pos :

The type of nonnegative binary numbers, using pos_num.

13 = 1101(base 2) = pos (bit1 (bit0 (bit1 one)))

Instances for num
@[protected, instance]
@[protected, instance]
meta def num.has_reflect  :
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
@[protected, instance]
meta def znum.has_reflect  :
inductive znum  :
Type
• zero : znum
• pos :
• neg :

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

Instances for znum
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
def pos_num.bit (b : bool) :

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

Equations
def pos_num.succ  :

The successor of a pos_num.

Equations
def pos_num.is_one  :

Returns a boolean for whether the pos_num is one.

Equations
@[protected]
def pos_num.add  :

Addition of two pos_nums.

Equations
@[protected, instance]
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
def pos_num.size  :

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
@[protected]
def pos_num.mul (a : pos_num) :

Multiplication of two pos_nums.

Equations
@[protected, instance]
Equations

of_nat_succ n is the pos_num corresponding to n + 1.

Equations
def pos_num.of_nat (n : ) :

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

Equations
def pos_num.cmp  :

Ordering of pos_nums.

Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, 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
@[protected, instance]
def pos_num_coe {α : Type u_1} [has_one α] [has_add α] :
Equations
@[protected, instance]
def num_nat_coe {α : Type u_1} [has_one α] [has_add α] [z : has_zero α] :
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
def num.succ'  :

The successor of a num as a pos_num.

Equations
def num.succ (n : num) :

The successor of a num as a num.

Equations
@[protected]
def num.add  :
num

Addition of two nums.

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

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

Equations
@[protected]
def num.bit1  :

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

Equations
def num.bit (b : bool) :

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  :

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
@[protected]
def num.mul  :
num

Multiplication of two nums.

Equations
@[protected, instance]
Equations
def num.cmp  :
num

Ordering of nums.

Equations
@[protected, instance]
def num.has_lt  :
Equations
@[protected, instance]
def num.has_le  :
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
def num.to_znum  :

Converts a num to a znum.

Equations
def num.to_znum_neg  :

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
@[protected, instance]
Equations
def znum.abs  :

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
@[protected]
def znum.bit0  :

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

Equations
@[protected]
def znum.bit1  :

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

Equations
@[protected]
def znum.bitm1  :

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

Equations
def znum.of_int'  :

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
def pos_num.of_znum  :

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

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

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

Equations
@[protected, instance]
Equations
def num.ppred  :

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

Equations
def num.pred  :

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

Equations
def num.div2  :

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  :

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

Equations
def num.sub'  :
num

Subtraction of two nums, producing a znum.

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

Subtraction of two nums, producing an option num.

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

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

Equations
@[protected, instance]
Equations
@[protected]
def znum.add  :
znum

Addition of znums.

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

Multiplication of znums.

Equations
@[protected, instance]
Equations
def znum.cmp  :
znum

Ordering on znums.

Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
def pos_num.divmod_aux (d : pos_num) (q r : num) :

Auxiliary definition for pos_num.divmod.

Equations
def pos_num.divmod (d : pos_num) :

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

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

Division of pos_num,

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

Modulus of pos_nums.

Equations
def num.div  :
num

Division of nums, where x / 0 = 0.

Equations
def num.mod  :
num

Modulus of nums.

Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
def num.gcd_aux  :
num

Auxiliary definition for num.gcd.

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

Greatest Common Divisor (GCD) of two nums.

Equations
def znum.div  :
znum

Division of znum, where x / 0 = 0.

Equations
def znum.mod  :
znum

Modulus of znums.

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

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