From f4afbc2f8bd474bafedf9b8bdf9b7406cb6cb48e Mon Sep 17 00:00:00 2001
From: Siddharth <siddu.druid@gmail.com>
Date: Sun, 22 Sep 2024 23:37:04 -0500
Subject: [PATCH] feat: BitVec analogues of Nat.{mul_two, two_mul, mul_succ,
 succ_mul} (#5410)

As requested by @hargoniX .
---
 src/Init/Data/BitVec/Lemmas.lean | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index e3b07535c6..39b0a74020 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -1724,6 +1724,15 @@ theorem BitVec.mul_add {x y z : BitVec w} :
   rw [Nat.mul_mod, Nat.mod_mod (y.toNat + z.toNat),
     ← Nat.mul_mod, Nat.mul_add]
 
+theorem mul_succ {x y : BitVec w} : x * (y + 1#w) = x * y + x := by simp [BitVec.mul_add]
+theorem succ_mul {x y : BitVec w} : (x + 1#w) * y = x * y + y := by simp [BitVec.mul_comm, BitVec.mul_add]
+
+theorem mul_two {x : BitVec w} : x * 2#w = x + x := by
+  have : 2#w = 1#w + 1#w := by apply BitVec.eq_of_toNat_eq; simp
+  simp [this, mul_succ]
+
+theorem two_mul {x : BitVec w} : 2#w * x = x + x := by rw [BitVec.mul_comm, mul_two]
+
 @[simp, bv_toNat] theorem toInt_mul (x y : BitVec w) :
   (x * y).toInt = (x.toInt * y.toInt).bmod (2^w) := by
   simp [toInt_eq_toNat_bmod]