Basic Theorems About Bitvectors

This file contains theorems about bitvectors and their coercions to Nat and Fin.

theorem Bitvec.bitsToNat_toList {n : ℕ} (x : Bitvec n) : Bitvec.toNat x = Bitvec.bitsToNat (Vector.toList x)

theorem Bitvec.toNat_append {m : ℕ} (xs : Bitvec m) (b : Bool) : Bitvec.toNat (Vector.append xs (b ::ᵥ Vector.nil)) = Bitvec.toNat xs * 2 + Bitvec.toNat (b ::ᵥ Vector.nil)

theorem Bitvec.bits_toNat_decide (n : ℕ) : Bitvec.toNat (decide (n % 2 = 1) ::ᵥ Vector.nil) = n % 2

theorem Bitvec.ofNat_succ {k : ℕ} {n : ℕ} : Bitvec.ofNat (Nat.succ k) n = Vector.append (Bitvec.ofNat k (n / 2)) (decide (n % 2 = 1) ::ᵥ Vector.nil)

theorem Bitvec.toNat_ofNat {k : ℕ} {n : ℕ} : Bitvec.toNat (Bitvec.ofNat k n) = n % 2 ^ k

theorem Bitvec.ofFin_val {n : ℕ} (i : Fin (2 ^ n)) : Bitvec.toNat (Bitvec.ofFin i) = ↑i

theorem Bitvec.addLsb_eq_twice_add_one {x : ℕ} {b : Bool} : Bitvec.addLsb x b = 2 * x + bif b then 1 else 0

theorem Bitvec.toNat_eq_foldr_reverse {n : ℕ} (v : Bitvec n) : Bitvec.toNat v = List.foldr (flip Bitvec.addLsb) 0 (List.reverse (Vector.toList v))

theorem Bitvec.toNat_lt {n : ℕ} (v : Bitvec n) : Bitvec.toNat v < 2 ^ n

theorem Bitvec.addLsb_div_two {x : ℕ} {b : Bool} : Bitvec.addLsb x b / 2 = x

theorem Bitvec.decide_addLsb_mod_two {x : ℕ} {b : Bool} : decide (Bitvec.addLsb x b % 2 = 1) = b

theorem Bitvec.ofNat_toNat {n : ℕ} (v : Bitvec n) : Bitvec.ofNat n (Bitvec.toNat v) = v

theorem Bitvec.toFin_val {n : ℕ} (v : Bitvec n) : ↑(Bitvec.toFin v) = Bitvec.toNat v

theorem Bitvec.toFin_le_toFin_of_le {n : ℕ} {v₀ : Bitvec n} {v₁ : Bitvec n} (h : v₀ ≤ v₁) : Bitvec.toFin v₀ ≤ Bitvec.toFin v₁

theorem Bitvec.ofFin_le_ofFin_of_le {n : ℕ} {i : Fin (2 ^ n)} {j : Fin (2 ^ n)} (h : i ≤ j) : Bitvec.ofFin i ≤ Bitvec.ofFin j

theorem Bitvec.toFin_ofFin {n : ℕ} (i : Fin (2 ^ n)) : Bitvec.toFin (Bitvec.ofFin i) = i

theorem Bitvec.ofFin_toFin {n : ℕ} (v : Bitvec n) : Bitvec.ofFin (Bitvec.toFin v) = v