From 3e2bca73096f7490bb4a64280aed93c88d129f2a Mon Sep 17 00:00:00 2001
From: Luisa Cicolini <48860705+luisacicolini@users.noreply.github.com>
Date: Tue, 1 Oct 2024 12:57:14 +0100
Subject: [PATCH] feat: add `Bitvec.[add, sub, mul]_eq_xor` and
 `width_one_cases` (#5554)

Co-authored-by: Tobias Grosser <github@grosser.es>
---
 src/Init/Data/BitVec/Lemmas.lean | 25 +++++++++++++++++++++++++
 1 file changed, 25 insertions(+)

diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index a4e581802954..44db8a636191 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -463,6 +463,16 @@ theorem toInt_pos_iff {w : Nat} {x : BitVec w} :
     0 ≤ BitVec.toInt x ↔ 2 * x.toNat < 2 ^ w := by
   simp [toInt_eq_toNat_cond]; omega
 
+theorem eq_zero_or_eq_one (a : BitVec 1) : a = 0#1 ∨ a = 1#1 := by
+  obtain ⟨a, ha⟩ := a
+  simp only [Nat.reducePow]
+  have acases : a = 0 ∨ a = 1 := by omega
+  rcases acases with ⟨rfl | rfl⟩
+  · simp
+  · case inr h =>
+    subst h
+    simp
+
 /-! ### setWidth, zeroExtend and truncate -/
 
 @[simp]
@@ -1910,6 +1920,11 @@ theorem shiftLeft_add_distrib {x y : BitVec w} {n : Nat} :
   case succ n ih =>
     simp [ih, toNat_eq, Nat.shiftLeft_eq, ← Nat.add_mul]
 
+theorem add_eq_xor {a b : BitVec 1} : a + b = a ^^^ b := by
+  have ha : a = 0 ∨ a = 1 := eq_zero_or_eq_one _
+  have hb : b = 0 ∨ b = 1 := eq_zero_or_eq_one _
+  rcases ha with h | h <;> (rcases hb with h' | h' <;> (simp [h, h']))
+
 /-! ### sub/neg -/
 
 theorem sub_def {n} (x y : BitVec n) : x - y = .ofNat n ((2^n - y.toNat) + x.toNat) := by rfl
@@ -2019,6 +2034,11 @@ theorem neg_ne_iff_ne_neg {x y : BitVec w} : -x ≠ y ↔ x ≠ -y := by
     subst h'
     simp at h
 
+theorem sub_eq_xor {a b : BitVec 1} : a - b = a ^^^ b := by
+  have ha : a = 0 ∨ a = 1 := eq_zero_or_eq_one _
+  have hb : b = 0 ∨ b = 1 := eq_zero_or_eq_one _
+  rcases ha with h | h <;> (rcases hb with h' | h' <;> (simp [h, h']))
+
 /-! ### abs -/
 
 @[simp, bv_toNat]
@@ -2086,6 +2106,11 @@ theorem ofInt_mul {n} (x y : Int) : BitVec.ofInt n (x * y) =
   apply eq_of_toInt_eq
   simp
 
+theorem mul_eq_and {a b : BitVec 1} : a * b = a &&& b := by
+  have ha : a = 0 ∨ a = 1 := eq_zero_or_eq_one _
+  have hb : b = 0 ∨ b = 1 := eq_zero_or_eq_one _
+  rcases ha with h | h <;> (rcases hb with h' | h' <;> (simp [h, h']))
+
 /-! ### le and lt -/
 
 @[bv_toNat] theorem le_def {x y : BitVec n} :