theorem Std.BitVec.eq_of_toNat_eq {n : Nat} {i : Std.BitVec n} {j : Std.BitVec n} : Std.BitVec.toNat i = Std.BitVec.toNat j → i = j

Prove equality of bitvectors in terms of nat operations.

@[deprecated Std.BitVec.eq_nil]

theorem Std.BitVec.zero_is_unique (x : Std.BitVec 0) : x = Std.BitVec.nil

Replaced 2024-02-07.

@[simp]

theorem Std.BitVec.val_toFin {w : Nat} (x : Std.BitVec w) : ↑x.toFin = Std.BitVec.toNat x

theorem Std.BitVec.toNat_eq {n : Nat} (x : Std.BitVec n) (y : Std.BitVec n) : x = y ↔ Std.BitVec.toNat x = Std.BitVec.toNat y

theorem Std.BitVec.toNat_lt {n : Nat} (x : Std.BitVec n) : Std.BitVec.toNat x < 2 ^ n

theorem Std.BitVec.testBit_toNat {w : Nat} {i : Nat} (x : Std.BitVec w) : Nat.testBit (Std.BitVec.toNat x) i = Std.BitVec.getLsb x i

@[simp]

theorem Std.BitVec.getLsb_ofFin {n : Nat} (x : Fin (2 ^ n)) (i : Nat) : Std.BitVec.getLsb { toFin := x } i = Nat.testBit (↑x) i

@[simp]

theorem Std.BitVec.getLsb_ge {w : Nat} (x : Std.BitVec w) (i : Nat) (ge : i ≥ w) : Std.BitVec.getLsb x i = false

theorem Std.BitVec.eq_of_getLsb_eq {w : Nat} {x : Std.BitVec w} {y : Std.BitVec w} (pred : ∀ (i : Fin w), Std.BitVec.getLsb x ↑i = Std.BitVec.getLsb y ↑i) : x = y

theorem Std.BitVec.eq_of_getMsb_eq {w : Nat} {x : Std.BitVec w} {y : Std.BitVec w} (pred : ∀ (i : Fin w), Std.BitVec.getMsb x ↑i = Std.BitVec.getMsb y ↑i) : x = y

@[simp]

theorem Std.BitVec.toNat_ofBool (b : Bool) : Std.BitVec.toNat (Std.BitVec.ofBool b) = Bool.toNat b

@[simp]

theorem Std.BitVec.toNat_ofFin {n : Nat} (x : Fin (2 ^ n)) : Std.BitVec.toNat { toFin := x } = ↑x

@[simp]

theorem Std.BitVec.toNat_ofNat (x : Nat) (w : Nat) : Std.BitVec.toNat x#w = x % 2 ^ w

@[simp]

theorem Std.BitVec.getLsb_ofNat (n : Nat) (x : Nat) (i : Nat) : Std.BitVec.getLsb (x#n) i = (decide (i < n) && Nat.testBit x i)

@[deprecated Std.BitVec.toNat_ofNat]

theorem Std.BitVec.toNat_zero (n : Nat) : Std.BitVec.toNat 0#n = 0

@[simp]

theorem Std.BitVec.toNat_mod_cancel {n : Nat} (x : Std.BitVec n) : Std.BitVec.toNat x % 2 ^ n = Std.BitVec.toNat x

@[simp]

theorem Std.BitVec.ofNat_toNat {n : Nat} (m : Nat) (x : Std.BitVec n) : (Std.BitVec.toNat x)#m = Std.BitVec.truncate m x

cast

@[simp]

theorem Std.BitVec.toNat_cast {m : Nat} {n : Nat} (e : m = n) (x : Std.BitVec m) : Std.BitVec.toNat (Std.BitVec.cast e x) = Std.BitVec.toNat x

@[simp]

theorem Std.BitVec.getLsb_cast : ∀ {a a_1 : Nat} {h : a = a_1} {v : Std.BitVec a} {i : Nat}, Std.BitVec.getLsb (Std.BitVec.cast h v) i = Std.BitVec.getLsb v i

zeroExtend and truncate

@[simp]

theorem Std.BitVec.toNat_zeroExtend' {m : Nat} {n : Nat} (p : m ≤ n) (x : Std.BitVec m) : Std.BitVec.toNat (Std.BitVec.zeroExtend' p x) = Std.BitVec.toNat x

theorem Std.BitVec.toNat_zeroExtend {n : Nat} (i : Nat) (x : Std.BitVec n) : Std.BitVec.toNat (Std.BitVec.zeroExtend i x) = Std.BitVec.toNat x % 2 ^ i

@[simp]

theorem Std.BitVec.zeroExtend_eq {n : Nat} (x : Std.BitVec n) : Std.BitVec.zeroExtend n x = x

@[simp]

theorem Std.BitVec.zeroExtend_zero (m : Nat) (n : Nat) : Std.BitVec.zeroExtend m 0#n = 0#m

@[simp]

theorem Std.BitVec.truncate_eq {n : Nat} (x : Std.BitVec n) : Std.BitVec.truncate n x = x

@[simp]

theorem Std.BitVec.toNat_truncate {n : Nat} {i : Nat} (x : Std.BitVec n) : Std.BitVec.toNat (Std.BitVec.truncate i x) = Std.BitVec.toNat x % 2 ^ i

@[simp]

theorem Std.BitVec.getLsb_zeroExtend' {m : Nat} {n : Nat} (ge : m ≥ n) (x : Std.BitVec n) (i : Nat) : Std.BitVec.getLsb (Std.BitVec.zeroExtend' ge x) i = Std.BitVec.getLsb x i

@[simp]

theorem Std.BitVec.getLsb_zeroExtend {n : Nat} (m : Nat) (x : Std.BitVec n) (i : Nat) : Std.BitVec.getLsb (Std.BitVec.zeroExtend m x) i = (decide (i < m) && Std.BitVec.getLsb x i)

@[simp]

theorem Std.BitVec.getLsb_truncate {n : Nat} (m : Nat) (x : Std.BitVec n) (i : Nat) : Std.BitVec.getLsb (Std.BitVec.truncate m x) i = (decide (i < m) && Std.BitVec.getLsb x i)

extractLsb

@[simp]

theorem Std.BitVec.extractLsb_ofFin {n : Nat} (x : Fin (2 ^ n)) (hi : Nat) (lo : Nat) : Std.BitVec.extractLsb hi lo { toFin := x } = (↑x >>> lo)#(hi - lo + 1)

@[simp]

theorem Std.BitVec.extractLsb_ofNat (x : Nat) (n : Nat) (hi : Nat) (lo : Nat) : Std.BitVec.extractLsb hi lo x#n = ((x % 2 ^ n) >>> lo)#(hi - lo + 1)

@[simp]

theorem Std.BitVec.extractLsb'_toNat {n : Nat} (s : Nat) (m : Nat) (x : Std.BitVec n) : Std.BitVec.toNat (Std.BitVec.extractLsb' s m x) = Std.BitVec.toNat x >>> s % 2 ^ m

@[simp]

theorem Std.BitVec.extractLsb_toNat {n : Nat} (hi : Nat) (lo : Nat) (x : Std.BitVec n) : Std.BitVec.toNat (Std.BitVec.extractLsb hi lo x) = Std.BitVec.toNat x >>> lo % 2 ^ (hi - lo + 1)

@[simp]

theorem Std.BitVec.getLsb_extract {n : Nat} (hi : Nat) (lo : Nat) (x : Std.BitVec n) (i : Nat) : Std.BitVec.getLsb (Std.BitVec.extractLsb hi lo x) i = (decide (i ≤ hi - lo) && Std.BitVec.getLsb x (lo + i))

or

@[simp]

theorem Std.BitVec.toNat_or {v : Nat} {x : Std.BitVec v} {y : Std.BitVec v} : Std.BitVec.toNat (x ||| y) = Std.BitVec.toNat x ||| Std.BitVec.toNat y

@[simp]

theorem Std.BitVec.getLsb_or {v : Nat} {i : Nat} {x : Std.BitVec v} {y : Std.BitVec v} : Std.BitVec.getLsb (x ||| y) i = (Std.BitVec.getLsb x i || Std.BitVec.getLsb y i)

or

@[simp]

theorem Std.BitVec.toNat_and {v : Nat} {x : Std.BitVec v} {y : Std.BitVec v} : Std.BitVec.toNat (x &&& y) = Std.BitVec.toNat x &&& Std.BitVec.toNat y

@[simp]

theorem Std.BitVec.getLsb_and {v : Nat} {i : Nat} {x : Std.BitVec v} {y : Std.BitVec v} : Std.BitVec.getLsb (x &&& y) i = (Std.BitVec.getLsb x i && Std.BitVec.getLsb y i)

xor

@[simp]

theorem Std.BitVec.toNat_xor {v : Nat} {x : Std.BitVec v} {y : Std.BitVec v} : Std.BitVec.toNat (x ^^^ y) = Std.BitVec.toNat x ^^^ Std.BitVec.toNat y

@[simp]

theorem Std.BitVec.getLsb_xor {v : Nat} {i : Nat} {x : Std.BitVec v} {y : Std.BitVec v} : Std.BitVec.getLsb (x ^^^ y) i = xor (Std.BitVec.getLsb x i) (Std.BitVec.getLsb y i)

not

shiftLeft

@[simp]

theorem Std.BitVec.toNat_shiftLeft {v : Nat} {n : Nat} {x : Std.BitVec v} : Std.BitVec.toNat (x <<< n) = Std.BitVec.toNat x <<< n % 2 ^ v

@[simp]

theorem Std.BitVec.getLsb_shiftLeft {m : Nat} {i : Nat} (x : Std.BitVec m) (n : Nat) : Std.BitVec.getLsb (x <<< n) i = (decide (i < m) && !decide (i < n) && Std.BitVec.getLsb x (i - n))

theorem Std.BitVec.shiftLeftZeroExtend_eq {w : Nat} {n : Nat} {x : Std.BitVec w} : Std.BitVec.shiftLeftZeroExtend x n = Std.BitVec.zeroExtend (w + n) x <<< n

@[simp]

theorem Std.BitVec.getLsb_shiftLeftZeroExtend {m : Nat} {i : Nat} (x : Std.BitVec m) (n : Nat) : Std.BitVec.getLsb (Std.BitVec.shiftLeftZeroExtend x n) i = (!decide (i < n) && Std.BitVec.getLsb x (i - n))

ushiftRight

@[simp]

theorem Std.BitVec.toNat_ushiftRight {n : Nat} (x : Std.BitVec n) (i : Nat) : Std.BitVec.toNat (x >>> i) = Std.BitVec.toNat x >>> i

@[simp]

theorem Std.BitVec.getLsb_ushiftRight {n : Nat} (x : Std.BitVec n) (i : Nat) (j : Nat) : Std.BitVec.getLsb (x >>> i) j = Std.BitVec.getLsb x (i + j)

append

theorem Std.BitVec.append_def {v : Nat} {w : Nat} (x : Std.BitVec v) (y : Std.BitVec w) : x ++ y = Std.BitVec.shiftLeftZeroExtend x w ||| Std.BitVec.zeroExtend' (_ : w ≤ v + w) y

@[simp]

theorem Std.BitVec.toNat_append {m : Nat} {n : Nat} (x : Std.BitVec m) (y : Std.BitVec n) : Std.BitVec.toNat (x ++ y) = Std.BitVec.toNat x <<< n ||| Std.BitVec.toNat y

@[simp]

theorem Std.BitVec.getLsb_append {n : Nat} {m : Nat} {i : Nat} {v : Std.BitVec n} {w : Std.BitVec m} : Std.BitVec.getLsb (v ++ w) i = bif decide (i < m) then Std.BitVec.getLsb w i else Std.BitVec.getLsb v (i - m)

rev

theorem Std.BitVec.getLsb_rev {w : Nat} (x : Std.BitVec w) (i : Fin w) : Std.BitVec.getLsb x ↑(Fin.rev i) = Std.BitVec.getMsb x ↑i

theorem Std.BitVec.getMsb_rev {w : Nat} (x : Std.BitVec w) (i : Fin w) : Std.BitVec.getMsb x ↑(Fin.rev i) = Std.BitVec.getLsb x ↑i

cons

@[simp]

theorem Std.BitVec.toNat_cons {w : Nat} (b : Bool) (x : Std.BitVec w) : Std.BitVec.toNat (Std.BitVec.cons b x) = Bool.toNat b <<< w ||| Std.BitVec.toNat x

@[simp]

theorem Std.BitVec.getLsb_cons (b : Bool) {n : Nat} (x : Std.BitVec n) (i : Nat) : Std.BitVec.getLsb (Std.BitVec.cons b x) i = if i = n then b else Std.BitVec.getLsb x i

theorem Std.BitVec.truncate_succ {w : Nat} {i : Nat} (x : Std.BitVec w) : Std.BitVec.truncate (i + 1) x = Std.BitVec.cons (Std.BitVec.getLsb x i) (Std.BitVec.truncate i x)

add

theorem Std.BitVec.add_def {n : Nat} (x : Std.BitVec n) (y : Std.BitVec n) : x + y = (Std.BitVec.toNat x + Std.BitVec.toNat y)#n

@[simp]

theorem Std.BitVec.toNat_add {w : Nat} (x : Std.BitVec w) (y : Std.BitVec w) : Std.BitVec.toNat (x + y) = (Std.BitVec.toNat x + Std.BitVec.toNat y) % 2 ^ w

Definition of bitvector addition as a nat.

@[simp]

theorem Std.BitVec.ofFin_add {n : Nat} (x : Fin (2 ^ n)) (y : Std.BitVec n) : { toFin := x } + y = { toFin := x + y.toFin }

@[simp]

theorem Std.BitVec.add_ofFin {n : Nat} (x : Std.BitVec n) (y : Fin (2 ^ n)) : x + { toFin := y } = { toFin := x.toFin + y }

@[simp]

theorem Std.BitVec.ofNat_add_ofNat {n : Nat} (x : Nat) (y : Nat) : x#n + y#n = (x + y)#n

theorem Std.BitVec.add_assoc {n : Nat} (x : Std.BitVec n) (y : Std.BitVec n) (z : Std.BitVec n) : x + y + z = x + (y + z)

theorem Std.BitVec.add_comm {n : Nat} (x : Std.BitVec n) (y : Std.BitVec n) : x + y = y + x

@[simp]

theorem Std.BitVec.add_zero {n : Nat} (x : Std.BitVec n) : x + 0#n = x

@[simp]

theorem Std.BitVec.zero_add {n : Nat} (x : Std.BitVec n) : 0#n + x = x

sub/neg

theorem Std.BitVec.sub_def {n : Nat} (x : Std.BitVec n) (y : Std.BitVec n) : x - y = (Std.BitVec.toNat x + (2 ^ n - Std.BitVec.toNat y))#n

@[simp]

theorem Std.BitVec.toNat_sub {n : Nat} (x : Std.BitVec n) (y : Std.BitVec n) : Std.BitVec.toNat (x - y) = (Std.BitVec.toNat x + (2 ^ n - Std.BitVec.toNat y)) % 2 ^ n

@[deprecated Std.BitVec.toNat_sub]

theorem Std.BitVec.sub_toNat {n : Nat} (x : Std.BitVec n) (y : Std.BitVec n) : Std.BitVec.toNat (x - y) = (Std.BitVec.toNat x + (2 ^ n - Std.BitVec.toNat y)) % 2 ^ n

Replaced 2024-02-06.

@[simp]

theorem Std.BitVec.ofFin_sub {n : Nat} (x : Fin (2 ^ n)) (y : Std.BitVec n) : { toFin := x } - y = { toFin := x - y.toFin }

@[simp]

theorem Std.BitVec.sub_ofFin {n : Nat} (x : Std.BitVec n) (y : Fin (2 ^ n)) : x - { toFin := y } = { toFin := x.toFin - y }

@[simp]

theorem Std.BitVec.ofNat_sub_ofNat {n : Nat} (x : Nat) (y : Nat) : x#n - y#n = (x + (2 ^ n - y % 2 ^ n))#n

@[simp]

theorem Std.BitVec.sub_zero {n : Nat} (x : Std.BitVec n) : x - 0#n = x

@[simp]

theorem Std.BitVec.sub_self {n : Nat} (x : Std.BitVec n) : x - x = 0#n

@[simp]

theorem Std.BitVec.toNat_neg {n : Nat} (x : Std.BitVec n) : Std.BitVec.toNat (-x) = (2 ^ n - Std.BitVec.toNat x) % 2 ^ n

@[deprecated Std.BitVec.toNat_neg]

theorem Std.BitVec.neg_toNat {n : Nat} (x : Std.BitVec n) : Std.BitVec.toNat (-x) = (2 ^ n - Std.BitVec.toNat x) % 2 ^ n

Replaced 2024-02-06.

theorem Std.BitVec.sub_toAdd {n : Nat} (x : Std.BitVec n) (y : Std.BitVec n) : x - y = x + -y

@[simp]

theorem Std.BitVec.neg_zero (n : Nat) : -0#n = 0#n

mul

theorem Std.BitVec.mul_def {n : Nat} {x : Std.BitVec n} {y : Std.BitVec n} : x * y = { toFin := x.toFin * y.toFin }

theorem Std.BitVec.toNat_mul {w : Nat} {x : Std.BitVec w} {y : Std.BitVec w} : Std.BitVec.toNat (x * y) = Std.BitVec.toNat x * Std.BitVec.toNat y % 2 ^ w

le and lt

theorem Std.BitVec.le_def {n : Nat} (x : Std.BitVec n) (y : Std.BitVec n) : x ≤ y ↔ Std.BitVec.toNat x ≤ Std.BitVec.toNat y

@[simp]

theorem Std.BitVec.le_ofFin {n : Nat} (x : Std.BitVec n) (y : Fin (2 ^ n)) : x ≤ { toFin := y } ↔ x.toFin ≤ y

@[simp]

theorem Std.BitVec.ofFin_le {n : Nat} (x : Fin (2 ^ n)) (y : Std.BitVec n) : { toFin := x } ≤ y ↔ x ≤ y.toFin

@[simp]

theorem Std.BitVec.ofNat_le_ofNat {n : Nat} (x : Nat) (y : Nat) : x#n ≤ y#n ↔ x % 2 ^ n ≤ y % 2 ^ n

theorem Std.BitVec.lt_def {n : Nat} (x : Std.BitVec n) (y : Std.BitVec n) : x < y ↔ Std.BitVec.toNat x < Std.BitVec.toNat y

@[simp]

theorem Std.BitVec.lt_ofFin {n : Nat} (x : Std.BitVec n) (y : Fin (2 ^ n)) : x < { toFin := y } ↔ x.toFin < y

@[simp]

theorem Std.BitVec.ofFin_lt {n : Nat} (x : Fin (2 ^ n)) (y : Std.BitVec n) : { toFin := x } < y ↔ x < y.toFin

@[simp]

theorem Std.BitVec.ofNat_lt_ofNat {n : Nat} (x : Nat) (y : Nat) : x#n < y#n ↔ x % 2 ^ n < y % 2 ^ n

theorem Std.BitVec.lt_of_le_ne {n : Nat} (x : Std.BitVec n) (y : Std.BitVec n) (h1 : x ≤ y) (h2 : ¬x = y) : x < y