feat: add BitVec _assoc lemmas

opencompl · May 27, 2024 · 57d84ea · 57d84ea
1 parent 6677767
commit 57d84ea
Showing 1 changed file with 13 additions and 0 deletions.
diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
@@ -461,6 +461,11 @@ protected theorem extractLsb_ofNat (x n : Nat) (hi lo : Nat) :
   ext
   simp
 
+theorem or_assoc (a b c : BitVec w) :
+    a ||| b ||| c = a ||| (b ||| c) := by
+  ext i
+  simp [Bool.or_assoc]
+
 /-! ### and -/
 
 @[simp] theorem toNat_and (x y : BitVec v) :
@@ -487,6 +492,10 @@ protected theorem extractLsb_ofNat (x n : Nat) (hi lo : Nat) :
   ext
   simp
 
+theorem and_assoc (a b c : BitVec w) :
+    a &&& b &&& c = a &&& (b &&& c) := by
+  ext i; simp [Bool.and_assoc]
+
 /-! ### xor -/
 
 @[simp] theorem toNat_xor (x y : BitVec v) :
@@ -507,6 +516,10 @@ protected theorem extractLsb_ofNat (x n : Nat) (hi lo : Nat) :
   ext
   simp
 
+theorem xor_assoc (a b c : BitVec w) :
+    a ^^^ b ^^^ c = a ^^^ (b ^^^ c) := by
+  ext i; simp [Bool.xor_assoc]
+
 /-! ### not -/
 
 theorem not_def {x : BitVec v} : ~~~x = allOnes v ^^^ x := rfl