Documentation

Mathlib.Data.BitVec.Lemmas

Basic Theorems About Bitvectors #

This file contains theorems about bitvectors.

source
theorem BitVec.toFin_injective {n : ℕ} :
Function.Injective BitVec.toFin
source
theorem BitVec.toFin_inj {w : ℕ} {x : BitVec w} {y : BitVec w} :
x.toFin = y.toFin ↔ x = y
source
theorem BitVec.toNat_injective {n : ℕ} :
Function.Injective BitVec.toNat
source
theorem BitVec.toNat_inj {w : ℕ} {x : BitVec w} {y : BitVec w} :
BitVec.toNat x = BitVec.toNat y ↔ x = y
source
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.

source
theorem BitVec.toNat_ofNat_of_lt {w : ℕ} {m : ℕ} (h : m < 2 ^ w) :
BitVec.toNat m#w = m
source
@[simp]
theorem BitVec.extractLsb_eq {w : ℕ} (hi : ℕ) (lo : ℕ) (a : BitVec w) :
BitVec.extractLsb hi lo a = BitVec.extractLsb' lo (hi - lo + 1) a
source
theorem BitVec.toNat_extractLsb' {w : ℕ} {i : ℕ} {j : ℕ} {x : BitVec w} :
BitVec.toNat (BitVec.extractLsb' i j x) = BitVec.toNat x / 2 ^ i % 2 ^ j
source
theorem BitVec.ofFin_val {n : ℕ} (i : Fin (2 ^ n)) :
BitVec.toNat { toFin := i } = ↑i
source
theorem BitVec.addLsb_eq_twice_add_one {x : ℕ} {b : Bool} :
BitVec.addLsb x b = 2 * x + bif b then 1 else 0
source
theorem BitVec.addLsb_div_two {x : ℕ} {b : Bool} :
BitVec.addLsb x b / 2 = x
source
theorem BitVec.decide_addLsb_mod_two {x : ℕ} {b : Bool} :
decide (BitVec.addLsb x b % 2 = 1) = b
source
theorem BitVec.ofNat_toNat' {w : ℕ} (x : BitVec w) :
(BitVec.toNat x)#w = x
source
theorem BitVec.ofNat_toNat_of_eq {w : ℕ} {v : ℕ} (x : BitVec w) (h : w = v) :
(BitVec.toNat x)#v = BitVec.cast h x
source
theorem BitVec.toFin_val {n : ℕ} (v : BitVec n) :
↑v.toFin = BitVec.toNat v
source
theorem BitVec.toFin_le_toFin_of_le {n : ℕ} {v₀ : BitVec n} {v₁ : BitVec n} (h : v₀ ≤ v₁) :
v₀.toFin ≤ v₁.toFin
source
theorem BitVec.ofFin_le_ofFin_of_le {n : ℕ} {i : Fin (2 ^ n)} {j : Fin (2 ^ n)} (h : i ≤ j) :
{ toFin := i } ≤ { toFin := j }
source
theorem BitVec.toFin_ofFin {n : ℕ} (i : Fin (2 ^ n)) :
{ toFin := i }.toFin = i
source
theorem BitVec.ofFin_toFin {n : ℕ} (v : BitVec n) :
{ toFin := v.toFin } = v

Distributivity of BitVec.ofFin #

source
@[simp]
theorem BitVec.ofFin_neg {w : ℕ} (x : Fin (2 ^ w)) :
{ toFin := -x } = -{ toFin := x }
source
@[simp]
theorem BitVec.ofFin_and {w : ℕ} (x : Fin (2 ^ w)) (y : Fin (2 ^ w)) :
{ toFin := x &&& y } = { toFin := x } &&& { toFin := y }
source
@[simp]
theorem BitVec.ofFin_or {w : ℕ} (x : Fin (2 ^ w)) (y : Fin (2 ^ w)) :
{ toFin := x ||| y } = { toFin := x } ||| { toFin := y }
source
@[simp]
theorem BitVec.ofFin_xor {w : ℕ} (x : Fin (2 ^ w)) (y : Fin (2 ^ w)) :
{ toFin := x ^^^ y } = { toFin := x } ^^^ { toFin := y }
source
@[simp]
theorem BitVec.ofFin_mul {w : ℕ} (x : Fin (2 ^ w)) (y : Fin (2 ^ w)) :
{ toFin := x * y } = { toFin := x } * { toFin := y }
source
theorem BitVec.ofFin_zero {w : ℕ} :
{ toFin := 0 } = 0
source
theorem BitVec.ofFin_one {w : ℕ} :
{ toFin := 1 } = 1
source
theorem BitVec.ofFin_nsmul {w : ℕ} (n : ℕ) (x : Fin (2 ^ w)) :
{ toFin := n • x } = n • { toFin := x }
source
theorem BitVec.ofFin_zsmul {w : ℕ} (z : ℤ) (x : Fin (2 ^ w)) :
{ toFin := z • x } = z • { toFin := x }
source
@[simp]
theorem BitVec.ofFin_pow {w : ℕ} (x : Fin (2 ^ w)) (n : ℕ) :
{ toFin := x ^ n } = { toFin := x } ^ n
source
@[simp]
theorem BitVec.ofFin_natCast {w : ℕ} (n : ℕ) :
{ toFin := ↑n } = ↑n
source
@[simp]
theorem BitVec.ofFin_ofNat {w : ℕ} (n : ℕ) :
{ toFin := OfNat.ofNat n } = OfNat.ofNat n

Distributivity of Std.BitVec.toFin #

source
@[simp]
theorem BitVec.toFin_neg {w : ℕ} (x : BitVec w) :
(-x).toFin = -x.toFin
source
theorem BitVec.toFin_zero {w : ℕ} :
0.toFin = 0
source
theorem BitVec.toFin_one {w : ℕ} :
1.toFin = 1
source
theorem BitVec.toFin_nsmul {w : ℕ} (n : ℕ) (x : BitVec w) :
(n • x).toFin = n • x.toFin
source
theorem BitVec.toFin_zsmul {w : ℕ} (z : ℤ) (x : BitVec w) :
(z • x).toFin = z • x.toFin
source
@[simp]
theorem BitVec.toFin_pow {w : ℕ} (x : BitVec w) (n : ℕ) :
(x ^ n).toFin = x.toFin ^ n
source
theorem BitVec.toFin_natCast {w : ℕ} (n : ℕ) :
(↑n).toFin = ↑n

IntCast #

Ring #

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