mathlib3 documentation

def pos_num.one_bits :

pos_num → ℕ → list ℕ

n.one_bits 0 is the list of indices of active bits in the binary representation of n.

Equations

p.bit0.one_bits d = p.one_bits (d + 1)
p.bit1.one_bits d = d :: p.one_bits (d + 1)
1.one_bits d = [d]

def pos_num.shiftl (p : pos_num) :

ℕ → pos_num

Left-shift the binary representation of a pos_num.

Equations

p.shiftl (n + 1) = (p.shiftl n).bit0
p.shiftl 0 = p

def pos_num.shiftr :

pos_num → ℕ → num

Right-shift the binary representation of a pos_num.

Equations

p.bit0.shiftr (n + 1) = p.shiftr n
ᾰ.bit0.shiftr 0 = num.pos ᾰ.bit0
p.bit1.shiftr (n + 1) = p.shiftr n
ᾰ.bit1.shiftr 0 = num.pos ᾰ.bit1
1.shiftr (n + 1) = 0
pos_num.one.shiftr 0 = num.pos pos_num.one

def num.lor :

Bitwise "or" for num.

Equations

(num.pos p).lor (num.pos q) = num.pos (p.lor q)
(num.pos ᾰ).lor 0 = num.pos ᾰ
0.lor (num.pos ᾰ) = num.pos ᾰ
0.lor num.zero = num.zero

def num.land :

Bitwise "and" for num.

Equations

(num.pos p).land (num.pos q) = p.land q
(num.pos ᾰ).land 0 = 0
0.land (num.pos ᾰ) = 0
0.land num.zero = 0

def num.ldiff :

Bitwise λ a b, a && !b for num. For example, ldiff 5 9 = 4:

1001 #

Equations

(num.pos p).ldiff (num.pos q) = p.ldiff q
(num.pos ᾰ).ldiff 0 = num.pos ᾰ
0.ldiff (num.pos ᾰ) = 0
0.ldiff num.zero = 0

def num.lxor :

Bitwise "xor" for num.

Equations

(num.pos p).lxor (num.pos q) = p.lxor q
(num.pos ᾰ).lxor 0 = num.pos ᾰ
0.lxor (num.pos ᾰ) = num.pos ᾰ
0.lxor num.zero = num.zero

def num.shiftl :

num → ℕ → num

Left-shift the binary representation of a num.

Equations

(num.pos p).shiftl n = num.pos (p.shiftl n)
0.shiftl n = 0

def num.shiftr :

num → ℕ → num

Right-shift the binary representation of a pos_num.

Equations

(num.pos p).shiftr n = p.shiftr n
0.shiftr n = 0

def num.test_bit :

num → ℕ → bool

a.test_bit n is tt iff the n-th bit (starting from the LSB) in the binary representation of a is active. If the size of a is less than n, this evaluates to ff.

Equations

(num.pos p).test_bit n = p.test_bit n
0.test_bit n = bool.ff

def num.one_bits :

num → list ℕ

n.one_bits is the list of indices of active bits in the binary representation of n.

Equations

(num.pos p).one_bits = p.one_bits 0
0.one_bits = list.nil

@[protected, instance]

meta def nzsnum.has_reflect :

has_reflect nzsnum

@[protected, instance]

def nzsnum.decidable_eq :

decidable_eq nzsnum

inductive nzsnum :

Type

msb : bool → nzsnum
bit : bool → nzsnum → nzsnum

This is a nonzero (and "non minus one") version of snum. See the documentation of snum for more details.

Instances for nzsnum

@[protected, instance]

def snum.decidable_eq :

decidable_eq snum

@[protected, instance]

meta def snum.has_reflect :

has_reflect snum

inductive snum :

Type

zero : bool → snum
nz : nzsnum → snum

Alternative representation of integers using a sign bit at the end. The convention on sign here is to have the argument to msb denote the sign of the MSB itself, with all higher bits set to the negation of this sign. The result is interpreted in two's complement.

13  = ..0001101(base 2) = nz (bit1 (bit0 (bit1 (msb tt))))
-13 = ..1110011(base 2) = nz (bit1 (bit1 (bit0 (msb ff))))

As with num, a special case must be added for zero, which has no msb, but by two's complement symmetry there is a second special case for -1. Here the bool field indicates the sign of the number.

0  = ..0000000(base 2) = zero ff
-1 = ..1111111(base 2) = zero tt

Instances for snum

@[protected, instance]

def snum.has_coe :

has_coe nzsnum snum

Equations

snum.has_coe = {coe := snum.nz}

@[protected, instance]

def snum.has_zero :

has_zero snum

Equations

snum.has_zero = {zero := snum.zero bool.ff}

@[protected, instance]

def nzsnum.has_one :

has_one nzsnum

Equations

nzsnum.has_one = {one := nzsnum.msb bool.tt}

@[protected, instance]

def snum.has_one :

has_one snum

Equations

snum.has_one = {one := snum.nz 1}

@[protected, instance]

def nzsnum.inhabited :

inhabited nzsnum

Equations

nzsnum.inhabited = {default := 1}

@[protected, instance]

def snum.inhabited :

inhabited snum

Equations

snum.inhabited = {default := 0}

def nzsnum.sign :

nzsnum → bool

Sign of a nzsnum.

Equations

(b::p).sign = p.sign
(nzsnum.msb b).sign = !b

def nzsnum.not :

nzsnum → nzsnum

Bitwise not for nzsnum.

Equations

~(b::p) = !b::~p
~nzsnum.msb b = nzsnum.msb (!b)

def nzsnum.bit0 :

nzsnum → nzsnum

Add an inactive bit at the end of a nzsnum. This mimics pos_num.bit0.

Equations

nzsnum.bit0 = nzsnum.bit bool.ff

def nzsnum.bit1 :

nzsnum → nzsnum

Add an active bit at the end of a nzsnum. This mimics pos_num.bit1.

Equations

nzsnum.bit1 = nzsnum.bit bool.tt

def nzsnum.head :

nzsnum → bool

The head of a nzsnum is the boolean value of its LSB.

Equations

(b::p).head = b
(nzsnum.msb b).head = b

def nzsnum.tail :

nzsnum → snum

The tail of a nzsnum is the snum obtained by removing the LSB. Edge cases: tail 1 = 0 and tail (-2) = -1.

Equations

(b::p).tail = ↑p
(nzsnum.msb b).tail = snum.zero (!b)

def snum.sign :

snum → bool

Sign of a snum.

Equations

(snum.nz p).sign = p.sign
(snum.zero z).sign = z

def snum.not :

Bitwise not for snum.

Equations

~snum.nz p = ↑~p
~snum.zero z = snum.zero (!z)

def snum.bit :

bool → snum → snum

Add a bit at the end of a snum. This mimics nzsnum.bit.

Equations

b::snum.nz p = ↑(b::p)
b::snum.zero z = ite (b = z) (snum.zero b) ↑(nzsnum.msb b)

def snum.bit0 :

Add an inactive bit at the end of a snum. This mimics znum.bit0.

Equations

snum.bit0 = snum.bit bool.ff

def snum.bit1 :

Add an active bit at the end of a snum. This mimics znum.bit1.

Equations

snum.bit1 = snum.bit bool.tt

theorem snum.bit_zero (b : bool) :

b::snum.zero b = snum.zero b

theorem snum.bit_one (b : bool) :

b::snum.zero (!b) = ↑(nzsnum.msb b)

def nzsnum.drec' {C : snum → Sort u_1} (z : Π (b : bool), C (snum.zero b)) (s : Π (b : bool) (p : snum), C p → C (b::p)) (p : nzsnum) :

C ↑p

A dependent induction principle for nzsnum, with base cases 0 : snum and (-1) : snum.

Equations

nzsnum.drec' z s (b::p) = s b ↑p (nzsnum.drec' z s p)
nzsnum.drec' z s (nzsnum.msb b) = _.mpr (s b (snum.zero (!b)) (z (!b)))

def snum.head :

snum → bool

The head of a snum is the boolean value of its LSB.

Equations

(snum.nz p).head = p.head
(snum.zero z).head = z

def snum.tail :

The tail of a snum is obtained by removing the LSB. Edge cases: tail 1 = 0, tail (-2) = -1, tail 0 = 0 and tail (-1) = -1.

Equations

(snum.nz p).tail = p.tail
(snum.zero z).tail = snum.zero z

def snum.drec' {C : snum → Sort u_1} (z : Π (b : bool), C (snum.zero b)) (s : Π (b : bool) (p : snum), C p → C (b::p)) (p : snum) :

C p

A dependent induction principle for snum which avoids relying on nzsnum.

Equations

snum.drec' z s (snum.nz p) = nzsnum.drec' z s p
snum.drec' z s (snum.zero b) = z b

def snum.rec' {α : Sort u_1} (z : bool → α) (s : bool → snum → α → α) :

snum → α

An induction principle for snum which avoids relying on nzsnum.

Equations

snum.rec' z s = snum.drec' z s

def snum.test_bit :

ℕ → snum → bool

snum.test_bit n a is tt iff the n-th bit (starting from the LSB) of a is active. If the size of a is less than n, this evaluates to ff.

Equations

snum.test_bit (n + 1) p = snum.test_bit n p.tail
snum.test_bit 0 p = p.head

def snum.succ :

The successor of a snum (i.e. the operation adding one).

Equations

snum.succ = snum.rec' (λ (b : bool), cond b 0 1) (λ (b : bool) (p succp : snum), cond b (bool.ff ::succp) (bool.tt ::p))

def snum.pred :

The predecessor of a snum (i.e. the operation of removing one).

Equations

snum.pred = snum.rec' (λ (b : bool), cond b (~1) (~0)) (λ (b : bool) (p predp : snum), cond b (bool.ff ::p) (bool.tt ::predp))

@[protected]

def snum.neg (n : snum) :

snum

The opposite of a snum.

Equations

n.neg = (~n).succ

@[protected, instance]

def snum.has_neg :

has_neg snum

Equations

snum.has_neg = {neg := snum.neg}

def snum.czadd :

bool → bool → snum → snum

snum.czadd a b n is n + a - b (where a and b should be read as either 0 or 1). This is useful to implement the carry system in cadd.

Equations

def snum.bits :

snum → Π (n : ℕ), vector bool n

a.bits n is the vector of the n first bits of a (starting from the LSB).

Equations

p.bits (n + 1) = p.head ::ᵥ p.tail.bits n
p.bits 0 = vector.nil

def snum.cadd :

snum → snum → bool → snum

Equations

snum.cadd = snum.rec' (λ (a : bool) (p : snum) (c : bool), snum.czadd c a p) (λ (a : bool) (p : snum) (IH : snum → bool → snum), snum.rec' (λ (b c : bool), snum.czadd c b (a::p)) (λ (b : bool) (q : snum) (_x : bool → snum) (c : bool), bitvec.xor3 a b c::IH q (bitvec.carry a b c)))

@[protected]

def snum.add (a b : snum) :

snum

Add two snums.

Equations

a.add b = a.cadd b bool.ff

@[protected, instance]

def snum.has_add :

has_add snum

Equations

snum.has_add = {add := snum.add}

@[protected]

def snum.sub (a b : snum) :

snum

subtract two snums.

Equations

a.sub b = a + -b

@[protected, instance]

def snum.has_sub :

has_sub snum

Equations

snum.has_sub = {sub := snum.sub}

@[protected]

def snum.mul (a : snum) :

Multiply two snums.

Equations

a.mul = snum.rec' (λ (b : bool), cond b (-a) 0) (λ (b : bool) (q IH : snum), cond b (IH.bit0 + a) IH.bit0)