From ff116dae5fe9e4e053074b6fdd49aaeecf069e76 Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Sat, 1 Jun 2024 17:24:18 +0100 Subject: [PATCH] feat: add BitVec _assoc lemmas (#4299) --- 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 b4b4277150..1702170d08 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -463,6 +463,11 @@ protected theorem extractLsb_ofNat (x n : Nat) (hi lo : Nat) : ext simp +theorem or_assoc (x y z : BitVec w) : + x ||| y ||| z = x ||| (y ||| z) := by + ext i + simp [Bool.or_assoc] + /-! ### and -/ @[simp] theorem toNat_and (x y : BitVec v) : @@ -489,6 +494,11 @@ protected theorem extractLsb_ofNat (x n : Nat) (hi lo : Nat) : ext simp +theorem and_assoc (x y z : BitVec w) : + x &&& y &&& z = x &&& (y &&& z) := by + ext i + simp [Bool.and_assoc] + /-! ### xor -/ @[simp] theorem toNat_xor (x y : BitVec v) : @@ -509,6 +519,11 @@ protected theorem extractLsb_ofNat (x n : Nat) (hi lo : Nat) : ext simp +theorem xor_assoc (x y z : BitVec w) : + x ^^^ y ^^^ z = x ^^^ (y ^^^ z) := by + ext i + simp [Bool.xor_assoc] + /-! ### not -/ theorem not_def {x : BitVec v} : ~~~x = allOnes v ^^^ x := rfl