feat: Confluent simp-set for left shift by BitVec.twoPow

This PR adds `@[simp]` theorems to confluently rewrite
shifting left by `twoPow w i` (when `i` is constant).

Author: bollu

src/Init/Data/BitVec/Lemmas.lean

@@ -3401,6 +3401,22 @@ theorem twoPow_and (x : BitVec w) (i : Nat) :
     (twoPow w i) &&& x = if x.getLsbD i then twoPow w i else 0#w := by
   rw [BitVec.and_comm, and_twoPow]
 
+/-!
+NOTE(confluence of multiplication by twoPow):
+The three rewrite rules:
+- mul_twoPow_eq_shiftLeft: x * twoPow w i = x << i
+- twoPow_mul_eq_shiftLeft: twoPow w i * x = x << i
+- twoPow_shiftLeft_eq_twoPow_add: `twoPow w i << j = twoPow w (i + j)`
+
+ensure confluence in the case of `twoPow w i * twoPow w j`, which can get rewritten into:
+- `twoPow w i * twoPow w j → twoPow w i << j → twoPow w (i + j)
+- `twoPow w i * twoPow w j → twoPow w j << i → twoPow w (j + i)
+- `twoPow w i * twoPow w j → twoPow w (i + j)
+
+which produce the same right hand side, upto a commutation of `i + j`,
+which is acceptable for constant folding.
+-/
+
 @[simp]
 theorem mul_twoPow_eq_shiftLeft (x : BitVec w) (i : Nat) :
     x * (twoPow w i) = x <<< i := by
@@ -3414,6 +3430,7 @@ theorem mul_twoPow_eq_shiftLeft (x : BitVec w) (i : Nat) :
       apply Nat.pow_dvd_pow 2 (by omega)
     simp [Nat.mul_mod, hpow]
 
+@[simp]
 theorem twoPow_mul_eq_shiftLeft (x : BitVec w) (i : Nat) :
     (twoPow w i) * x = x <<< i := by
   rw [BitVec.mul_comm, mul_twoPow_eq_shiftLeft]
@@ -3429,11 +3446,15 @@ theorem shiftLeft_eq_mul_twoPow (x : BitVec w) (n : Nat) :
   simp [getLsbD_shiftLeft, Fin.is_lt, decide_true, Bool.true_and, mul_twoPow_eq_shiftLeft]
 
 /-- 2^i * 2^j = 2^(i + j) with bitvectors as well -/
-theorem twoPow_mul_twoPow_eq {w : Nat} (i j : Nat) : twoPow w i * twoPow w j = twoPow w (i + j) := by 
+theorem twoPow_mul_twoPow_eq {w : Nat} (i j : Nat) : twoPow w i * twoPow w j = twoPow w (i + j) := by
   apply BitVec.eq_of_toNat_eq
   simp only [toNat_mul, toNat_twoPow]
   rw [← Nat.mul_mod, Nat.pow_add]
 
+@[simp]
+theorem twoPow_shiftLeft_eq_twoPow_add {w i j : Nat} : twoPow w i <<< j = twoPow w (i + j) := by
+  rw [shiftLeft_eq_mul_twoPow, twoPow_mul_twoPow_eq]
+
 /--
 The unsigned division of `x` by `2^k` equals shifting `x` right by `k`,
 when `k` is less than the bitwidth `w`.

tests/lean/run/bitvec_simproc.lean

@@ -141,3 +141,12 @@ example (h : False) : 1#2 = 2#2 := by
   simp; guard_target =ₛ False; exact h
 example : 1#2 ≠ 2#2 := by
   simp
+/-! Check that multiplication by twoPow and <<< rewrites to the <<< normal form. -/
+example : twoPow 32 3 * twoPow 32 4 = twoPow 32 7 := by
+  simp
+example (x : BitVec 32) : x * twoPow 32 4 = x <<< 4 := by
+  simp
+example (x : BitVec 32) : twoPow 32 4 * x = x <<< 4 := by
+  simp
+example (x : BitVec 32) : ((twoPow 32 4 * x) <<< 3) * twoPow 32 3 = x <<< 10 := by
+  simp