From 46bf4b69b651f94cbb64068079a0a23e71fbbdd7 Mon Sep 17 00:00:00 2001 From: Alex Keizer Date: Tue, 5 Mar 2024 02:48:10 +0000 Subject: [PATCH] feat: add lemmas about `BitVec.concat` and bitwise ops (#3487) Show how the various bitwise ops (`and`, `or`, `not`, and `xor`) distribute over `concat`. --- src/Init/Data/BitVec/Lemmas.lean | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index eb2e202331..6ae3955677 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -638,6 +638,21 @@ theorem getLsb_concat (x : BitVec w) (b : Bool) (i : Nat) : @[simp] theorem getLsb_concat_succ : (concat x b).getLsb (i + 1) = x.getLsb i := by simp [getLsb_concat] +@[simp] theorem not_concat (x : BitVec w) (b : Bool) : ~~~(concat x b) = concat (~~~x) !b := by + ext i; cases i using Fin.succRecOn <;> simp [*, Nat.succ_lt_succ] + +@[simp] theorem concat_or_concat (x y : BitVec w) (a b : Bool) : + (concat x a) ||| (concat y b) = concat (x ||| y) (a || b) := by + ext i; cases i using Fin.succRecOn <;> simp + +@[simp] theorem concat_and_concat (x y : BitVec w) (a b : Bool) : + (concat x a) &&& (concat y b) = concat (x &&& y) (a && b) := by + ext i; cases i using Fin.succRecOn <;> simp + +@[simp] theorem concat_xor_concat (x y : BitVec w) (a b : Bool) : + (concat x a) ^^^ (concat y b) = concat (x ^^^ y) (xor a b) := by + ext i; cases i using Fin.succRecOn <;> simp + /-! ### add -/ theorem add_def {n} (x y : BitVec n) : x + y = .ofNat n (x.toNat + y.toNat) := rfl