From 21f7cc5f4e0390fc08db39b5a6cc7dc376014b3d Mon Sep 17 00:00:00 2001
From: Tobias Grosser <tobias@grosser.es>
Date: Mon, 27 May 2024 19:38:53 +0100
Subject: [PATCH] feat: add BitVec _assoc lemmas

---
 src/Init/Data/BitVec/Lemmas.lean | 13 +++++++++++++
 1 file changed, 13 insertions(+)

diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index fbfc6cedbf62..994273ba719c 100644
--- 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