Basic Theorems About Bitvectors

This file contains theorems about bitvectors.

theorem BitVec.toFin_injective {n : ℕ} : Function.Injective BitVec.toFin

theorem BitVec.toFin_inj {w : ℕ} {x : BitVec w} {y : BitVec w} : x.toFin = y.toFin ↔ x = y

theorem BitVec.toNat_injective {n : ℕ} : Function.Injective BitVec.toNat

theorem BitVec.toNat_inj {w : ℕ} {x : BitVec w} {y : BitVec w} : BitVec.toNat x = BitVec.toNat y ↔ x = y

theorem BitVec.toNat_lt_toNat {w : ℕ} {x : BitVec w} {y : BitVec w} : BitVec.toNat x < BitVec.toNat y ↔ x < y

x < y as natural numbers if and only if x < y as BitVec w.

theorem BitVec.toNat_ofNat_of_lt {w : ℕ} {m : ℕ} (h : m < 2 ^ w) : BitVec.toNat m#w = m

@[simp]

theorem BitVec.extractLsb_eq {w : ℕ} (hi : ℕ) (lo : ℕ) (a : BitVec w) : BitVec.extractLsb hi lo a = BitVec.extractLsb' lo (hi - lo + 1) a

theorem BitVec.toNat_extractLsb' {w : ℕ} {i : ℕ} {j : ℕ} {x : BitVec w} : BitVec.toNat (BitVec.extractLsb' i j x) = BitVec.toNat x / 2 ^ i % 2 ^ j

theorem BitVec.ofFin_val {n : ℕ} (i : Fin (2 ^ n)) : BitVec.toNat { toFin := 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.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' {w : ℕ} (x : BitVec w) : (BitVec.toNat x)#w = x

theorem BitVec.ofNat_toNat_of_eq {w : ℕ} {v : ℕ} (x : BitVec w) (h : w = v) : (BitVec.toNat x)#v = BitVec.cast h x

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

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

theorem BitVec.ofFin_le_ofFin_of_le {n : ℕ} {i : Fin (2 ^ n)} {j : Fin (2 ^ n)} (h : i ≤ j) : { toFin := i } ≤ { toFin := j }

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

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

Distributivity of BitVec.ofFin

@[simp]

theorem BitVec.ofFin_neg {w : ℕ} (x : Fin (2 ^ w)) : { toFin := -x } = -{ toFin := x }

@[simp]

theorem BitVec.ofFin_and {w : ℕ} (x : Fin (2 ^ w)) (y : Fin (2 ^ w)) : { toFin := x &&& y } = { toFin := x } &&& { toFin := y }

@[simp]

theorem BitVec.ofFin_or {w : ℕ} (x : Fin (2 ^ w)) (y : Fin (2 ^ w)) : { toFin := x ||| y } = { toFin := x } ||| { toFin := y }

@[simp]

theorem BitVec.ofFin_xor {w : ℕ} (x : Fin (2 ^ w)) (y : Fin (2 ^ w)) : { toFin := x ^^^ y } = { toFin := x } ^^^ { toFin := y }

@[simp]

theorem BitVec.ofFin_mul {w : ℕ} (x : Fin (2 ^ w)) (y : Fin (2 ^ w)) : { toFin := x * y } = { toFin := x } * { toFin := y }

theorem BitVec.ofFin_zero {w : ℕ} : { toFin := 0 } = 0

theorem BitVec.ofFin_one {w : ℕ} : { toFin := 1 } = 1

theorem BitVec.ofFin_nsmul {w : ℕ} (n : ℕ) (x : Fin (2 ^ w)) : { toFin := n • x } = n • { toFin := x }

theorem BitVec.ofFin_zsmul {w : ℕ} (z : ℤ) (x : Fin (2 ^ w)) : { toFin := z • x } = z • { toFin := x }

@[simp]

theorem BitVec.ofFin_pow {w : ℕ} (x : Fin (2 ^ w)) (n : ℕ) : { toFin := x ^ n } = { toFin := x } ^ n

@[simp]

theorem BitVec.ofFin_natCast {w : ℕ} (n : ℕ) : { toFin := ↑n } = ↑n

@[simp]

theorem BitVec.ofFin_ofNat {w : ℕ} (n : ℕ) : { toFin := OfNat.ofNat n } = OfNat.ofNat n

Distributivity of Std.BitVec.toFin

@[simp]

theorem BitVec.toFin_neg {w : ℕ} (x : BitVec w) : (-x).toFin = -x.toFin

theorem BitVec.toFin_zero {w : ℕ} : 0.toFin = 0

theorem BitVec.toFin_one {w : ℕ} : 1.toFin = 1

theorem BitVec.toFin_nsmul {w : ℕ} (n : ℕ) (x : BitVec w) : (n • x).toFin = n • x.toFin

theorem BitVec.toFin_zsmul {w : ℕ} (z : ℤ) (x : BitVec w) : (z • x).toFin = z • x.toFin

@[simp]

theorem BitVec.toFin_pow {w : ℕ} (x : BitVec w) (n : ℕ) : (x ^ n).toFin = x.toFin ^ n

theorem BitVec.toFin_natCast {w : ℕ} (n : ℕ) : (↑n).toFin = ↑n

IntCast

Ring

instance BitVec.instCommSemiringBitVec {w : ℕ} : CommSemiring (BitVec w)

Equations

• BitVec.instCommSemiringBitVec = Function.Injective.commSemiring BitVec.toFin ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯