mathlib documentation

data.num.basic

Binary representation of integers using inductive types #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. https://github.com/leanprover-community/mathlib4/pull/607 Any changes to this file require a corresponding PR to mathlib4.

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

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

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
@[protected]

Addition of two pos_nums.

Equations
@[protected, instance]
Equations

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
@[protected]

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

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

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  :

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

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

Equations
@[protected]
def num.mul  :

Multiplication of two nums.

Equations
@[protected, instance]
Equations

Ordering of nums.

Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations

Converts a num to a znum.

Equations

Converts x : num to -x : znum.

Equations

Converts a nat to a num.

Equations

The negation of a znum.

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

The absolute value of a znum as a num.

Equations

The successor of a znum.

Equations

The predecessor of a znum.

Equations
@[protected]

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

Equations
@[protected]

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

Equations
@[protected]

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

Equations

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
@[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

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

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

Equations

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

Equations

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]

Addition of znums.

Equations
@[protected, instance]
Equations
@[protected]

Multiplication of 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

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  :

Division of nums, where x / 0 = 0.

Equations
def num.mod  :

Modulus of nums.

Equations
@[protected, instance]
Equations
@[protected, instance]
Equations

Auxiliary definition for num.gcd.

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

Greatest Common Divisor (GCD) of two nums.

Equations

Division of znum, where x / 0 = 0.

Equations

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 α] :

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