From 042cd6c2fa306964e7c653bf21fc732116c70638 Mon Sep 17 00:00:00 2001
From: Tobias Grosser <tobias@grosser.es>
Date: Sat, 21 Sep 2024 19:48:16 +0100
Subject: [PATCH] feat: add `_self`, `_zero`, and `_allOnes` for
 BitVec.[and|or|xor]

The `xor_allOnes` theorems end up in the `not` section, as the
relevant simplification lemmas are otherwise not defined.
---
 src/Init/Data/BitVec/Lemmas.lean | 60 ++++++++++++++++++++++++++++++++
 1 file changed, 60 insertions(+)

diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index 54355070f1f3..d3ced2ff315b 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -710,6 +710,26 @@ theorem or_comm (x y : BitVec w) :
   simp [Bool.or_comm]
 instance : Std.Commutative (fun (x y : BitVec w) => x ||| y) := ⟨BitVec.or_comm⟩
 
+@[simp] theorem or_self {x : BitVec w} : x ||| x = x := by
+  ext i
+  simp [Bool.or_self]
+
+@[simp] theorem or_zero {x : BitVec w} : x ||| 0#w = x := by
+  ext i
+  simp
+
+@[simp] theorem zero_or {x : BitVec w} : 0#w ||| x = x := by
+  ext i
+  simp
+
+@[simp] theorem or_allOnes {x : BitVec w} : x ||| allOnes w = allOnes w := by
+  ext i
+  simp
+
+@[simp] theorem allOnes_or {x : BitVec w} : allOnes w ||| x = allOnes w := by
+  ext i
+  simp
+
 /-! ### and -/
 
 @[simp] theorem toNat_and (x y : BitVec v) :
@@ -751,6 +771,26 @@ theorem and_comm (x y : BitVec w) :
   simp [Bool.and_comm]
 instance : Std.Commutative (fun (x y : BitVec w) => x &&& y) := ⟨BitVec.and_comm⟩
 
+@[simp] theorem and_self {x : BitVec w} : x &&& x = x := by
+  ext i
+  simp [Bool.and_self]
+
+@[simp] theorem and_zero {x : BitVec w} : x &&& 0#w = 0#w := by
+  ext i
+  simp
+
+@[simp] theorem zero_and {x : BitVec w} : 0#w &&& x = 0#w := by
+  ext i
+  simp
+
+@[simp] theorem and_allOnes {x : BitVec w} : x &&& allOnes w = x := by
+  ext i
+  simp
+
+@[simp] theorem allOnes_and {x : BitVec w} : allOnes w &&& x = x := by
+  ext i
+  simp
+
 /-! ### xor -/
 
 @[simp] theorem toNat_xor (x y : BitVec v) :
@@ -795,6 +835,18 @@ theorem xor_comm (x y : BitVec w) :
   simp [Bool.xor_comm]
 instance : Std.Commutative (fun (x y : BitVec w) => x ^^^ y) := ⟨BitVec.xor_comm⟩
 
+@[simp] theorem xor_self {x : BitVec w} : x ^^^ x = 0#w := by
+  ext i
+  simp [Bool.xor_self]
+
+@[simp] theorem xor_zero {x : BitVec w} : x ^^^ 0#w = x := by
+  ext i
+  simp
+
+@[simp] theorem zero_xor {x : BitVec w} : 0#w ^^^ x = x := by
+  ext i
+  simp
+
 /-! ### not -/
 
 theorem not_def {x : BitVec v} : ~~~x = allOnes v ^^^ x := rfl
@@ -843,6 +895,14 @@ theorem not_def {x : BitVec v} : ~~~x = allOnes v ^^^ x := rfl
   ext
   simp
 
+@[simp] theorem xor_allOnes {x : BitVec w} : x ^^^ allOnes w = ~~~ x := by
+  ext i
+  simp
+
+@[simp] theorem allOnes_xor {x : BitVec w} : allOnes w ^^^ x = ~~~ x := by
+  ext i
+  simp
+
 /-! ### cast -/
 
 @[simp] theorem not_cast {x : BitVec w} (h : w = w') : ~~~(cast h x) = cast h (~~~x) := by