data.num.basic - mathlib docs

source

@[protected, instance]

meta def pos_num.has_reflect :

has_reflect pos_num

source

inductive pos_num :

Type

one : pos_num
bit1 : pos_num → pos_num
bit0 : pos_num → pos_num

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

pos_num.has_one = {one := pos_num.one}

source

@[protected, instance]

def pos_num.inhabited :

inhabited pos_num

Equations

pos_num.inhabited = {default := 1}

source

inductive num :

Type

zero : num
pos : pos_num → num

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

num.has_zero = {zero := num.zero}

source

@[protected, instance]

def num.has_one :

has_one num

Equations

num.has_one = {one := num.pos 1}

source

@[protected, instance]

def num.inhabited :

inhabited num

Equations

num.inhabited = {default := 0}

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

zero : znum
pos : pos_num → znum
neg : pos_num → 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)))

source

@[protected, instance]

def znum.has_zero :

has_zero znum

Equations

znum.has_zero = {zero := znum.zero}

source

@[protected, instance]

def znum.has_one :

has_one znum

Equations

znum.has_one = {one := znum.pos 1}

source

@[protected, instance]

def znum.inhabited :

inhabited znum

Equations

znum.inhabited = {default := 0}

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

pos_num.bit b = cond b pos_num.bit1 pos_num.bit0

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

a.bit0.add b.bit0 = (a.add b).bit0
a.bit0.add b.bit1 = (a.add b).bit1
ᾰ.bit0.add 1 = ᾰ.bit0.succ
a.bit1.add b.bit0 = (a.add b).bit1
a.bit1.add b.bit1 = (a.add b).succ.bit0
ᾰ.bit1.add 1 = ᾰ.bit1.succ
1.add ᾰ.bit0 = ᾰ.bit0.succ
1.add ᾰ.bit1 = ᾰ.bit1.succ
1.add pos_num.one = pos_num.one.succ

source

@[protected, instance]

def pos_num.has_add :

has_add pos_num

Equations

pos_num.has_add = {add := pos_num.add}

source

def pos_num.pred' :

pos_num → num

The predecessor of a pos_num as a num.

Equations

n.bit0.pred' = num.pos (n.pred'.cases_on 1 pos_num.bit1)
n.bit1.pred' = num.pos n.bit0
1.pred' = 0

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

a.pred = a.pred'.cases_on 1 id

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

a.mul b.bit0 = (a.mul b).bit0
a.mul b.bit1 = (a.mul b).bit0 + a
a.mul 1 = a

source

@[protected, instance]

def pos_num.has_mul :

has_mul pos_num

Equations

pos_num.has_mul = {mul := pos_num.mul}

source

def pos_num.of_nat_succ :

ℕ → pos_num

of_nat_succ n is the pos_num corresponding to n + 1.

Equations

pos_num.of_nat_succ n.succ = (pos_num.of_nat_succ n).succ
pos_num.of_nat_succ 0 = 1

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

pos_num.of_nat n = pos_num.of_nat_succ n.pred

source

def pos_num.cmp :

pos_num → pos_num → ordering

Ordering of pos_nums.

Equations

a.bit0.cmp b.bit0 = a.cmp b
a.bit0.cmp b.bit1 = (a.cmp b).cases_on ordering.lt ordering.lt ordering.gt
ᾰ.bit0.cmp 1 = ordering.gt
a.bit1.cmp b.bit0 = (a.cmp b).cases_on ordering.lt ordering.gt ordering.gt
a.bit1.cmp b.bit1 = a.cmp b
ᾰ.bit1.cmp 1 = ordering.gt
1.cmp ᾰ.bit0 = ordering.lt
1.cmp ᾰ.bit1 = ordering.lt
1.cmp 1 = ordering.eq

source

@[protected, instance]

def pos_num.has_lt :

has_lt pos_num

Equations

pos_num.has_lt = {lt := λ (a b : pos_num), a.cmp b = ordering.lt}

source

@[protected, instance]

def pos_num.has_le :

has_le pos_num

Equations

pos_num.has_le = {le := λ (a b : pos_num), ¬b < a}

source

@[protected, instance]

def pos_num.decidable_lt :

decidable_rel has_lt.lt

Equations

pos_num.decidable_lt a b = id (ordering.decidable_eq (a.cmp b) ordering.lt)

source

@[protected, instance]

def pos_num.decidable_le :

decidable_rel has_le.le

Equations

pos_num.decidable_le a b = id (ne.decidable (b.cmp a) ordering.lt)

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

cast_pos_num a.bit0 = bit0 (cast_pos_num a)
cast_pos_num a.bit1 = bit1 (cast_pos_num a)
cast_pos_num 1 = 1

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

cast_num (num.pos p) = cast_pos_num p
cast_num 0 = 0

source

@[protected, instance]

def pos_num_coe {α : Type u_1} [has_one α] [has_add α] :

has_coe_t pos_num α

Equations

pos_num_coe = {coe := cast_pos_num _inst_2}

source

@[protected, instance]

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

has_coe_t num α

Equations

num_nat_coe = {coe := cast_num z}

source

@[protected, instance]

def pos_num.has_repr :

has_repr pos_num

Equations

pos_num.has_repr = {repr := λ (n : pos_num), repr ↑n}

source

@[protected, instance]

def num.has_repr :

has_repr num

Equations

num.has_repr = {repr := λ (n : num), repr ↑n}

source

def num.succ' :

num → pos_num

The successor of a num as a pos_num.

Equations

(num.pos p).succ' = p.succ
0.succ' = 1

source

def num.succ (n : num) :

num

The successor of a num as a num.

Equations

n.succ = num.pos n.succ'

source

@[protected]

def num.add :

num → num → num

Addition of two nums.

Equations

(num.pos a).add (num.pos b) = num.pos (a + b)
(num.pos ᾰ).add 0 = num.pos ᾰ
0.add (num.pos ᾰ) = num.pos ᾰ
0.add num.zero = num.zero

source

@[protected, instance]

def num.has_add :

has_add num

Equations

num.has_add = {add := num.add}

source

@[protected]

def num.bit0 :

num → num

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

Equations

(num.pos n).bit0 = num.pos n.bit0
0.bit0 = 0

source

@[protected]

def num.bit1 :

num → num

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

Equations

(num.pos n).bit1 = num.pos n.bit1
0.bit1 = 1

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

num.bit b = cond b num.bit1 num.bit0

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

(num.pos n).size = num.pos n.size
0.size = 0

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

(num.pos n).nat_size = n.nat_size
0.nat_size = 0

source

@[protected]

def num.mul :

num → num → num

Multiplication of two nums.

Equations

(num.pos a).mul (num.pos b) = num.pos (a * b)
(num.pos ᾰ).mul 0 = 0
0.mul (num.pos ᾰ) = 0
0.mul num.zero = 0

source

@[protected, instance]

def num.has_mul :

has_mul num

Equations

num.has_mul = {mul := num.mul}

source

def num.cmp :

num → num → ordering

Ordering of nums.

Equations

source

@[protected, instance]

def num.has_lt :

has_lt num

Equations

num.has_lt = {lt := λ (a b : num), a.cmp b = ordering.lt}

source

@[protected, instance]

def num.has_le :

has_le num

Equations

num.has_le = {le := λ (a b : num), ¬b < a}

source

@[protected, instance]

def num.decidable_lt :

decidable_rel has_lt.lt

Equations

num.decidable_lt a b = id (ordering.decidable_eq (a.cmp b) ordering.lt)

source

@[protected, instance]

def num.decidable_le :

decidable_rel has_le.le

Equations

num.decidable_le a b = id (ne.decidable (b.cmp a) ordering.lt)

source

def num.to_znum :

num → znum

Converts a num to a znum.

Equations

(num.pos a).to_znum = znum.pos a
0.to_znum = 0

source

def num.to_znum_neg :

num → znum

Converts x : num to -x : znum.

Equations

(num.pos a).to_znum_neg = znum.neg a
0.to_znum_neg = 0

source

def num.of_nat' :

ℕ → num

Converts a nat to a num.

Equations

num.of_nat' = nat.binary_rec 0 (λ (b : bool) (n : ℕ), cond b num.bit1 num.bit0)

source

def znum.zneg :

znum → znum

The negation of a znum.

Equations

source

@[protected, instance]

def znum.has_neg :

has_neg znum

Equations

znum.has_neg = {neg := znum.zneg}

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

(znum.neg n).bit1 = znum.neg (n.pred'.cases_on 1 pos_num.bit1)
(znum.pos n).bit1 = znum.pos n.bit1
0.bit1 = 1

source

@[protected]

def znum.bitm1 :

znum → znum

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

Equations

(znum.neg n).bitm1 = znum.neg n.bit1
(znum.pos n).bitm1 = znum.pos (n.pred'.cases_on 1 pos_num.bit1)
0.bitm1 = znum.neg 1

source

def znum.of_int' :

ℤ → znum

Converts an int to a znum.

Equations

znum.of_int' -[1+ n] = (num.of_nat' (n + 1)).to_znum_neg
znum.of_int' ↑n = (num.of_nat' n).to_znum

source

def pos_num.sub' :

pos_num → pos_num → znum

Subtraction of two pos_nums, producing a znum.

Equations

a.bit0.sub' b.bit0 = (a.sub' b).bit0
a.bit0.sub' b.bit1 = (a.sub' b).bitm1
ᾰ.bit0.sub' 1 = ᾰ.bit0.pred'.to_znum
a.bit1.sub' b.bit0 = (a.sub' b).bit1
a.bit1.sub' b.bit1 = (a.sub' b).bit0
ᾰ.bit1.sub' 1 = ᾰ.bit1.pred'.to_znum
1.sub' ᾰ.bit0 = ᾰ.bit0.pred'.to_znum_neg
1.sub' ᾰ.bit1 = ᾰ.bit1.pred'.to_znum_neg
pos_num.one.sub' 1 = pos_num.one.pred'.to_znum

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

a.sub b = pos_num.sub._match_1 (a.sub' b)
pos_num.sub._match_1 (znum.neg ᾰ) = 1
pos_num.sub._match_1 (znum.pos p) = p
pos_num.sub._match_1 znum.zero = 1

source

@[protected, instance]

def pos_num.has_sub :

has_sub pos_num

Equations

pos_num.has_sub = {sub := pos_num.sub}

source

def num.ppred :

num → option num

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

Equations

(num.pos p).ppred = some p.pred'
0.ppred = none

source

def num.pred :

num → num

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

Equations

(num.pos p).pred = p.pred'
0.pred = 0

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

num.of_znum' (znum.neg p) = none
num.of_znum' (znum.pos p) = some (num.pos p)
num.of_znum' 0 = some 0

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

(num.pos a).sub' (num.pos b) = a.sub' b
(num.pos a).sub' 0 = znum.pos a
0.sub' (num.pos b) = znum.neg b
0.sub' 0 = 0

source

def num.psub (a b : num) :

option num

Subtraction of two nums, producing an option num.

Equations

a.psub b = num.of_znum' (a.sub' b)

source

@[protected]

def num.sub (a b : num) :

num

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

Equations

a.sub b = num.of_znum (a.sub' b)

source

@[protected, instance]

def num.has_sub :

has_sub num

Equations

num.has_sub = {sub := num.sub}

source

@[protected]

def znum.add :

znum → znum → znum

Addition of znums.

Equations

(znum.neg a).add (znum.neg b) = znum.neg (a + b)
(znum.neg a).add (znum.pos b) = b.sub' a
(znum.neg ᾰ).add 0 = znum.neg ᾰ
(znum.pos a).add (znum.neg b) = a.sub' b
(znum.pos a).add (znum.pos b) = znum.pos (a + b)
(znum.pos ᾰ).add 0 = znum.pos ᾰ
0.add (znum.neg ᾰ) = znum.neg ᾰ
0.add (znum.pos ᾰ) = znum.pos ᾰ
0.add znum.zero = znum.zero

source

@[protected, instance]

def znum.has_add :

has_add znum

Equations

znum.has_add = {add := znum.add}

source

@[protected]

def znum.mul :

znum → znum → znum

Multiplication of znums.

Equations

(znum.neg a).mul (znum.neg b) = znum.pos (a * b)
(znum.neg a).mul (znum.pos b) = znum.neg (a * b)
(znum.neg ᾰ).mul 0 = 0
(znum.pos a).mul (znum.neg b) = znum.neg (a * b)
(znum.pos a).mul (znum.pos b) = znum.pos (a * b)
(znum.pos ᾰ).mul 0 = 0
0.mul (znum.neg ᾰ) = 0
0.mul (znum.pos ᾰ) = 0
0.mul znum.zero = 0

source

@[protected, instance]

def znum.has_mul :

has_mul znum

Equations

znum.has_mul = {mul := znum.mul}

source

def znum.cmp :

znum → znum → ordering

Ordering on znums.

Equations

(znum.neg a).cmp (znum.neg b) = b.cmp a
(znum.neg _x).cmp (znum.pos ᾰ) = ordering.lt
(znum.neg _x).cmp znum.zero = ordering.lt
(znum.pos _x).cmp (znum.neg ᾰ) = ordering.gt
(znum.pos a).cmp (znum.pos b) = a.cmp b
(znum.pos _x).cmp znum.zero = ordering.gt
znum.zero.cmp (znum.neg _x) = ordering.gt
znum.zero.cmp (znum.pos _x) = ordering.lt
0.cmp 0 = ordering.eq

source

@[protected, instance]

def znum.has_lt :

has_lt znum

Equations

znum.has_lt = {lt := λ (a b : znum), a.cmp b = ordering.lt}

source

@[protected, instance]

def znum.has_le :

has_le znum

Equations

znum.has_le = {le := λ (a b : znum), ¬b < a}

source

@[protected, instance]

def znum.decidable_lt :

decidable_rel has_lt.lt

Equations

znum.decidable_lt a b = id (ordering.decidable_eq (a.cmp b) ordering.lt)

source

@[protected, instance]

def znum.decidable_le :

decidable_rel has_le.le

Equations

znum.decidable_le a b = id (ne.decidable (b.cmp a) ordering.lt)

source

def pos_num.divmod_aux (d : pos_num) (q r : num) :

num × num

Auxiliary definition for pos_num.divmod.

Equations

d.divmod_aux q r = pos_num.divmod_aux._match_1 q r (num.of_znum' (r.sub' (num.pos d)))
pos_num.divmod_aux._match_1 q r (some r') = (q.bit1, r')
pos_num.divmod_aux._match_1 q r none = (q.bit0, r)

source

def pos_num.divmod (d : pos_num) :

pos_num → num × num

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

Equations

d.divmod n.bit0 = pos_num.divmod._match_1 d (d.divmod n)
d.divmod n.bit1 = pos_num.divmod._match_2 d (d.divmod n)
d.divmod 1 = d.divmod_aux 0 1
pos_num.divmod._match_1 d (q, r₁) = d.divmod_aux q r₁.bit0
pos_num.divmod._match_2 d (q, r₁) = d.divmod_aux q r₁.bit1

source

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

num

Division of pos_num,

Equations

n.div' d = (d.divmod n).fst

source

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

num

Modulus of pos_nums.

Equations

n.mod' d = (d.divmod n).snd

source

def num.div :

num → num → num

Division of nums, where x / 0 = 0.

Equations

(num.pos n).div (num.pos d) = n.div' d
(num.pos ᾰ).div 0 = 0
0.div (num.pos ᾰ) = 0
0.div num.zero = 0

source

def num.mod :

num → num → num

Modulus of nums.

Equations

(num.pos n).mod (num.pos d) = n.mod' d
(num.pos ᾰ).mod 0 = num.pos ᾰ
0.mod (num.pos ᾰ) = 0
0.mod num.zero = 0

source

@[protected, instance]

def num.has_div :

has_div num

Equations

num.has_div = {div := num.div}

source

@[protected, instance]

def num.has_mod :

has_mod num

Equations

num.has_mod = {mod := num.mod}

source

def num.gcd_aux :

ℕ → num → num → num

Auxiliary definition for num.gcd.

Equations

num.gcd_aux n.succ (num.pos ᾰ) b = num.gcd_aux n (b % num.pos ᾰ) (num.pos ᾰ)
num.gcd_aux n.succ 0 b = b
num.gcd_aux 0 a b = b

source

def num.gcd (a b : num) :

num

Greatest Common Divisor (GCD) of two nums.

Equations

a.gcd b = ite (a ≤ b) (num.gcd_aux (a.nat_size + b.nat_size) a b) (num.gcd_aux (b.nat_size + a.nat_size) b a)

source

def znum.div :

znum → znum → znum

Division of znum, where x / 0 = 0.

Equations

(znum.neg n).div (znum.neg d) = znum.pos (n.pred' / num.pos d).succ'
(znum.neg n).div (znum.pos d) = znum.neg (n.pred' / num.pos d).succ'
(znum.neg ᾰ).div 0 = 0
(znum.pos n).div (znum.neg d) = (n.div' d).to_znum_neg
(znum.pos n).div (znum.pos d) = (n.div' d).to_znum
(znum.pos ᾰ).div 0 = 0
0.div (znum.neg ᾰ) = 0
0.div (znum.pos ᾰ) = 0
0.div znum.zero = 0

source

def znum.mod :

znum → znum → znum

Modulus of znums.

Equations

(znum.neg n).mod d = d.abs.sub' (n.pred' % d.abs).succ
(znum.pos n).mod d = (num.pos n % d.abs).to_znum
0.mod d = 0

source

@[protected, instance]

def znum.has_div :

has_div znum

Equations

znum.has_div = {div := znum.div}

source

@[protected, instance]

def znum.has_mod :

has_mod znum

Equations

znum.has_mod = {mod := znum.mod}

source

def znum.gcd (a b : znum) :

num

Greatest Common Divisor (GCD) of two znums.

Equations

a.gcd b = a.abs.gcd b.abs

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

znum_coe = {coe := cast_znum _inst_4}

source

@[protected, instance]

def znum.has_repr :

has_repr znum

Equations

znum.has_repr = {repr := λ (n : znum), repr ↑n}

mathlib documentation

Binary representation of integers using inductive types #