mathlib docs: data.num.basic

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

@[instance]

meta def pos_num.has_reflect :

has_reflect pos_num

source

@[instance]

def pos_num.decidable_eq :

decidable_eq pos_num

source

@[instance]

def pos_num.has_one :

has_one pos_num

Equations

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

source

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

@[instance]

def num.decidable_eq :

decidable_eq num

source

@[instance]

meta def num.has_reflect :

has_reflect num

source

@[instance]

def num.has_zero :

has_zero num

Equations

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

source

@[instance]

def num.has_one :

has_one num

Equations

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

source

@[instance]

def num.inhabited :

inhabited num

Equations

num.inhabited = {default := 0}

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

@[instance]

meta def znum.has_reflect :

has_reflect znum

source

@[instance]

def znum.decidable_eq :

decidable_eq znum

source

@[instance]

def znum.has_zero :

has_zero znum

Equations

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

source

@[instance]

def znum.has_one :

has_one znum

Equations

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

source

@[instance]

def znum.inhabited :

inhabited znum

Equations

znum.inhabited = {default := 0}

source

def pos_num.bit :

bool → pos_num → pos_num

Equations

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

source

def pos_num.succ :

pos_num → pos_num

Equations

source

def pos_num.is_one :

pos_num → bool

Equations

source

def pos_num.add :

pos_num → pos_num → pos_num

Equations

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

source

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

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 :

pos_num → pos_num

Equations

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

source

def pos_num.size :

pos_num → pos_num

Equations

source

def pos_num.nat_size :

pos_num → ℕ

Equations

source

def pos_num.mul :

pos_num → pos_num → pos_num

Equations

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

source

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

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 :

ℕ → pos_num

Equations

pos_num.of_nat n = pos_num.of_nat_succ n.pred

source

def pos_num.cmp :

pos_num → pos_num → ordering

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
a.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
a.bit1.cmp 1 = ordering.gt
1.cmp a.bit0 = ordering.lt
1.cmp a.bit1 = ordering.lt
1.cmp 1 = ordering.eq

source

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

@[instance]

def pos_num.has_le :

has_le pos_num

Equations

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

source

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

@[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_zero α] [has_one α] [has_add α] :

pos_num → α

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_zero α] [has_one α] [has_add α] :

num → α

Equations

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

source

@[instance]

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

has_coe_t pos_num α

Equations

pos_num_coe = {coe := cast_pos_num _inst_3}

source

@[instance]

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

has_coe_t num α

Equations

num_nat_coe = {coe := cast_num _inst_3}

source

@[instance]

def pos_num.has_repr :

has_repr pos_num

Equations

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

source

@[instance]

def num.has_repr :

has_repr num

Equations

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

source

def num.succ' :

num → pos_num

Equations

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

source

def num.succ :

num → num

Equations

n.succ = num.pos n.succ'

source

def num.add :

num → num → num

Equations

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

source

@[instance]

def num.has_add :

has_add num

Equations

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

source

def num.bit0 :

num → num

Equations

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

source

def num.bit1 :

num → num

Equations

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

source

def num.bit :

bool → num → num

Equations

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

source

def num.size :

num → num

Equations

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

source

def num.nat_size :

num → ℕ

Equations

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

source

def num.mul :

num → num → num

Equations

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

source

@[instance]

def num.has_mul :

has_mul num

Equations

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

source

def num.cmp :

num → num → ordering

Equations

source

@[instance]

def num.has_lt :

has_lt num

Equations

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

source

@[instance]

def num.has_le :

has_le num

Equations

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

source

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

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

Equations

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

source

def num.to_znum_neg :

num → znum

Equations

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

source

def num.of_nat' :

ℕ → num

Equations

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

source

def znum.zneg :

znum → znum

Equations

source

@[instance]

def znum.has_neg :

has_neg znum

Equations

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

source

def znum.abs :

znum → num

Equations

source

def znum.succ :

znum → znum

Equations

source

def znum.pred :

znum → znum

Equations

source

def znum.bit0 :

znum → znum

Equations

source

def znum.bit1 :

znum → znum

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

def znum.bitm1 :

znum → znum

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

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

Equations

a.bit0.sub' b.bit0 = (a.sub' b).bit0
a.bit0.sub' b.bit1 = (a.sub' b).bitm1
a.bit0.sub' 1 = a.bit0.pred'.to_znum
a.bit1.sub' b.bit0 = (a.sub' b).bit1
a.bit1.sub' b.bit1 = (a.sub' b).bit0
a.bit1.sub' 1 = a.bit1.pred'.to_znum
1.sub' a.bit0 = a.bit0.pred'.to_znum_neg
1.sub' a.bit1 = a.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

Equations

pos_num.of_znum' (znum.neg a) = option.none
pos_num.of_znum' (znum.pos p) = option.some p
pos_num.of_znum' znum.zero = option.none

source

def pos_num.of_znum :

znum → pos_num

Equations

source

def pos_num.sub :

pos_num → pos_num → pos_num

Equations

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

source

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

Equations

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

source

def num.pred :

num → num

Equations

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

source

def num.div2 :

num → num

Equations

source

def num.of_znum' :

znum → option num

Equations

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

source

def num.of_znum :

znum → num

Equations

source

def num.sub' :

num → num → 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 :

num → num → option num

Equations

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

source

def num.sub :

num → num → num

Equations

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

source

@[instance]

def num.has_sub :

has_sub num

Equations

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

source

def znum.add :

znum → znum → znum

Equations

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

source

@[instance]

def znum.has_add :

has_add znum

Equations

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

source

def znum.mul :

znum → znum → znum

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 a).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 a).mul 0 = 0
0.mul (znum.neg a) = 0
0.mul (znum.pos a) = 0
0.mul znum.zero = 0

source

@[instance]

def znum.has_mul :

has_mul znum

Equations

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

source

def znum.cmp :

znum → znum → ordering

Equations

(znum.neg a).cmp (znum.neg b) = b.cmp a
(znum.neg _x).cmp (znum.pos a) = ordering.lt
(znum.neg _x).cmp znum.zero = ordering.lt
(znum.pos _x).cmp (znum.neg a) = 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

@[instance]

def znum.has_lt :

has_lt znum

Equations

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

source

@[instance]

def znum.has_le :

has_le znum

Equations

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

source

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

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

pos_num → num → num → num × num

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 (option.some r') = (q.bit1, r')
pos_num.divmod_aux._match_1 q r option.none = (q.bit0, r)

source

def pos_num.divmod :

pos_num → pos_num → num × num

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' :

pos_num → pos_num → num

Equations

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

source

def pos_num.mod' :

pos_num → pos_num → num

Equations

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

source

def pos_num.sqrt_aux1 :

pos_num → num → num → num × num

Equations

b.sqrt_aux1 r n = pos_num.sqrt_aux1._match_1 b r n (num.of_znum' (n.sub' (r + num.pos b)))
pos_num.sqrt_aux1._match_1 b r n (option.some n') = (r.div2 + num.pos b, n')
pos_num.sqrt_aux1._match_1 b r n option.none = (r.div2, n)

source

def pos_num.sqrt_aux :

pos_num → num → num → num

Equations

b'.bit0.sqrt_aux r n = pos_num.sqrt_aux._match_1 (λ (r' n' : num), b'.sqrt_aux r' n') (b'.bit0.sqrt_aux1 r n)
b'.bit1.sqrt_aux r n = pos_num.sqrt_aux._match_2 (λ (r' n' : num), b'.sqrt_aux r' n') (b'.bit1.sqrt_aux1 r n)
1.sqrt_aux r n = (1.sqrt_aux1 r n).fst
pos_num.sqrt_aux._match_1 _f_1 (r', n') = _f_1 r' n'
pos_num.sqrt_aux._match_2 _f_1 (r', n') = _f_1 r' n'