mathlib3 documentation

data.bitvec.basic

@[protected, instance]

def bitvec.preorder (n : ℕ) :

preorder (bitvec n)

Equations

bitvec.preorder n = preorder.lift bitvec.to_nat

def bitvec.of_fin {n : ℕ} (i : fin (2 ^ n)) :

convert fin to bitvec

Equations

bitvec.of_fin i = bitvec.of_nat n i.val

theorem bitvec.of_fin_val {n : ℕ} (i : fin (2 ^ n)) :

(bitvec.of_fin i).to_nat = i.val

def bitvec.to_fin {n : ℕ} (i : bitvec n) :

fin (2 ^ n)

convert bitvec to fin

Equations

i.to_fin = ↑(i.to_nat)

theorem bitvec.add_lsb_eq_twice_add_one {x : ℕ} {b : bool} :

bitvec.add_lsb x b = 2 * x + cond b 1 0

theorem bitvec.to_nat_eq_foldr_reverse {n : ℕ} (v : bitvec n) :

v.to_nat = list.foldr (flip bitvec.add_lsb) 0 (vector.to_list v).reverse

theorem bitvec.to_nat_lt {n : ℕ} (v : bitvec n) :

v.to_nat < 2 ^ n

theorem bitvec.add_lsb_div_two {x : ℕ} {b : bool} :

bitvec.add_lsb x b / 2 = x

theorem bitvec.to_bool_add_lsb_mod_two {x : ℕ} {b : bool} :

decidable.to_bool (bitvec.add_lsb x b % 2 = 1) = b

theorem bitvec.of_nat_to_nat {n : ℕ} (v : bitvec n) :

bitvec.of_nat n v.to_nat = v

theorem bitvec.to_fin_val {n : ℕ} (v : bitvec n) :

↑(v.to_fin) = v.to_nat

theorem bitvec.to_fin_le_to_fin_of_le {n : ℕ} {v₀ v₁ : bitvec n} (h : v₀ ≤ v₁) :

v₀.to_fin ≤ v₁.to_fin

theorem bitvec.of_fin_le_of_fin_of_le {n : ℕ} {i j : fin (2 ^ n)} (h : i ≤ j) :

bitvec.of_fin i ≤ bitvec.of_fin j

theorem bitvec.to_fin_of_fin {n : ℕ} (i : fin (2 ^ n)) :

(bitvec.of_fin i).to_fin = i

theorem bitvec.of_fin_to_fin {n : ℕ} (v : bitvec n) :

bitvec.of_fin v.to_fin = v