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

---
 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 fbfc6cedbf62..dcd7f416e53c 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,11 @@ 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 +517,11 @@ 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

From 84a4f4fc8e207573c8eb7a4440128cc3ff40a5f8 Mon Sep 17 00:00:00 2001
From: Tobias Grosser <tobias@grosser.es>
Date: Tue, 28 May 2024 17:54:40 +0100
Subject: [PATCH 2/2] rename a b c -> x y z

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

diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index dcd7f416e53c..bee324d8ec25 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -461,8 +461,8 @@ 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
+theorem or_assoc (x y z : BitVec w) :
+    x ||| y ||| z = x ||| (y ||| z) := by
   ext i
   simp [Bool.or_assoc]
 
@@ -492,8 +492,8 @@ theorem or_assoc (a b c : BitVec w) :
   ext
   simp
 
-theorem and_assoc (a b c : BitVec w) :
-    a &&& b &&& c = a &&& (b &&& c) := by
+theorem and_assoc (x y z : BitVec w) :
+    x &&& y &&& z = x &&& (y &&& z) := by
   ext i
   simp [Bool.and_assoc]
 
@@ -517,8 +517,8 @@ theorem and_assoc (a b c : BitVec w) :
   ext
   simp
 
-theorem xor_assoc (a b c : BitVec w) :
-    a ^^^ b ^^^ c = a ^^^ (b ^^^ c) := by
+theorem xor_assoc (x y z : BitVec w) :
+    x ^^^ y ^^^ z = x ^^^ (y ^^^ z) := by
   ext i
   simp [Bool.xor_assoc]