Documentation

Mathlib.Data.BitVec.Lemmas

Basic Theorems About Bitvectors #

This file contains theorems about bitvectors.

source
theorem Std.BitVec.toFin_injective {n : ℕ} :
Function.Injective Std.BitVec.toFin
source
theorem Std.BitVec.toFin_inj {w : ℕ} {x : Std.BitVec w} {y : Std.BitVec w} :
x.toFin = y.toFin ↔ x = y
source
theorem Std.BitVec.toNat_injective {n : ℕ} :
Function.Injective Std.BitVec.toNat
source
theorem Std.BitVec.toNat_inj {w : ℕ} {x : Std.BitVec w} {y : Std.BitVec w} :
Std.BitVec.toNat x = Std.BitVec.toNat y ↔ x = y
source
theorem Std.BitVec.toNat_lt_toNat {w : ℕ} {x : Std.BitVec w} {y : Std.BitVec w} :
Std.BitVec.toNat x < Std.BitVec.toNat y ↔ x < y

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

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

Distributivity of Std.BitVec.ofFin #

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

Distributivity of Std.BitVec.toFin #

source
@[simp]
theorem Std.BitVec.toFin_neg {w : ℕ} (x : Std.BitVec w) :
(-x).toFin = -x.toFin
source
@[simp]
theorem Std.BitVec.toFin_and {w : ℕ} (x : Std.BitVec w) (y : Std.BitVec w) :
(x &&& y).toFin = x.toFin &&& y.toFin
source
@[simp]
theorem Std.BitVec.toFin_or {w : ℕ} (x : Std.BitVec w) (y : Std.BitVec w) :
(x ||| y).toFin = x.toFin ||| y.toFin
source
@[simp]
theorem Std.BitVec.toFin_xor {w : ℕ} (x : Std.BitVec w) (y : Std.BitVec w) :
(x ^^^ y).toFin = x.toFin ^^^ y.toFin
source
@[simp]
theorem Std.BitVec.toFin_add {w : ℕ} (x : Std.BitVec w) (y : Std.BitVec w) :
(x + y).toFin = x.toFin + y.toFin
source
@[simp]
theorem Std.BitVec.toFin_sub {w : ℕ} (x : Std.BitVec w) (y : Std.BitVec w) :
(x - y).toFin = x.toFin - y.toFin
source
@[simp]
theorem Std.BitVec.toFin_mul {w : ℕ} (x : Std.BitVec w) (y : Std.BitVec w) :
(x * y).toFin = x.toFin * y.toFin
source
theorem Std.BitVec.toFin_zero {w : ℕ} :
0.toFin = 0
source
theorem Std.BitVec.toFin_one {w : ℕ} :
1.toFin = 1
source
theorem Std.BitVec.toFin_nsmul {w : ℕ} (n : ℕ) (x : Std.BitVec w) :
(n • x).toFin = n • x.toFin
source
theorem Std.BitVec.toFin_zsmul {w : ℕ} (z : ℤ) (x : Std.BitVec w) :
(z • x).toFin = z • x.toFin
source
@[simp]
theorem Std.BitVec.toFin_pow {w : ℕ} (x : Std.BitVec w) (n : ℕ) :
(x ^ n).toFin = x.toFin ^ n
source
@[simp]
theorem Std.BitVec.toFin_natCast {w : ℕ} (n : ℕ) :
(↑n).toFin = ↑n
source
theorem Std.BitVec.toFin_ofNat {w : ℕ} (n : ℕ) :
(OfNat.ofNat n).toFin = OfNat.ofNat n

IntCast #

Ring #

source
instance Std.BitVec.instCommSemiringBitVec {w : ℕ} :
CommSemiring (Std.BitVec w)
Equations
  • One or more equations did not get rendered due to their size.