From 3565555aec03397e4fac8f0a01149bfd201d9f44 Mon Sep 17 00:00:00 2001 From: Siddharth Bhat Date: Fri, 20 Sep 2024 10:05:48 -0500 Subject: [PATCH] feat: BitVec analogues of Nat.{mul_two, two_mul, mul_succ, succ_mul} --- 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 54355070f1f3..c4d53205ec4a 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -1664,6 +1664,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]