feat: add BitVec zero/one simplifications

src/Init/Data/BitVec/Lemmas.lean

@@ -1061,8 +1061,9 @@ theorem not_eq_comm {x y : BitVec w} : ~~~ x = y ↔ x = ~~~ y := by
 @[simp] theorem toFin_shiftLeft {n : Nat} (x : BitVec w) :
     BitVec.toFin (x <<< n) = Fin.ofNat' (2^w) (x.toNat <<< n) := rfl
 
+-- deprecate?
 @[simp]
-theorem shiftLeft_zero_eq (x : BitVec w) : x <<< 0 = x := by
+theorem shiftLeft_zero (x : BitVec w) : x <<< 0 = x := by
   apply eq_of_toNat_eq
   simp
 
@@ -1232,7 +1233,11 @@ theorem ushiftRight_or_distrib (x y : BitVec w)  (n : Nat) :
   simp
 
 @[simp]
-theorem ushiftRight_zero_eq (x : BitVec w) : x >>> 0 = x := by
+theorem ushiftRight_zero (x : BitVec w) : x >>> 0 = x := by
+  simp [bv_toNat]
+
+@[simp]
+theorem zero_ushiftRight {n : Nat} : 0#w >>> n = 0#w := by
   simp [bv_toNat]
 
 /--
@@ -1387,6 +1392,10 @@ theorem msb_sshiftRight {n : Nat} {x : BitVec w} :
   ext i
   simp [getLsbD_sshiftRight]
 
+@[simp] theorem zero_sshiftRight {n : Nat} : (0#w).sshiftRight n = 0#w := by
+  ext i
+  simp [getLsbD_sshiftRight]
+
 theorem sshiftRight_add {x : BitVec w} {m n : Nat} :
     x.sshiftRight (m + n) = (x.sshiftRight m).sshiftRight n := by
   ext i
@@ -2153,18 +2162,23 @@ instance : Std.LawfulCommIdentity (fun (x y : BitVec w) => x * y) (1#w) where
   right_id := BitVec.mul_one
 
 @[simp]
-theorem BitVec.mul_zero {x : BitVec w} : x * 0#w = 0#w := by
+theorem mul_zero {x : BitVec w} : x * 0#w = 0#w := by
+  apply eq_of_toNat_eq
+  simp [toNat_mul]
+
+@[simp]
+theorem zero_mul {x : BitVec w} : 0#w * x = 0#w := by
   apply eq_of_toNat_eq
   simp [toNat_mul]
 
-theorem BitVec.mul_add {x y z : BitVec w} :
+theorem mul_add {x y z : BitVec w} :
     x * (y + z) = x * y + x * z := by
   apply eq_of_toNat_eq
   simp only [toNat_mul, toNat_add, Nat.add_mod_mod, Nat.mod_add_mod]
   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 mul_succ {x y : BitVec w} : x * (y + 1#w) = x * y + x := by simp [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

src/Std/Tactic/BVDecide/Normalize/BitVec.lean

@@ -104,15 +104,8 @@ attribute [bv_normalize] BitVec.not_not
 
 end Constant
 
-@[bv_normalize]
-theorem BitVec.zero_and (a : BitVec w) : 0#w &&& a = 0#w := by
-  ext
-  simp
-
-@[bv_normalize]
-theorem BitVec.and_zero (a : BitVec w) : a &&& 0#w = 0#w := by
-  ext
-  simp
+attribute [bv_normalize] BitVec.zero_and
+attribute [bv_normalize] BitVec.and_zero
 
 -- Used in simproc because of - normalization
 theorem BitVec.ones_and (a : BitVec w) : (-1#w) &&& a = a := by
@@ -124,10 +117,7 @@ theorem BitVec.and_ones (a : BitVec w) : a &&& (-1#w) = a := by
   ext
   simp [BitVec.negOne_eq_allOnes]
 
-@[bv_normalize]
-theorem BitVec.and_self (a : BitVec w) : a &&& a = a := by
-  ext
-  simp
+attribute [bv_normalize] BitVec.and_self
 
 @[bv_normalize]
 theorem BitVec.and_contra (a : BitVec w) : a &&& ~~~a = 0#w := by
@@ -202,55 +192,29 @@ theorem BitVec.add_const_right (a b c : BitVec w) : a + (b + c) = (a + c) + b :=
 theorem BitVec.add_const_left' (a b c : BitVec w) : (a + b) + c = (a + c) + b := by ac_rfl
 theorem BitVec.add_const_right' (a b c : BitVec w) : (a + b) + c = (b + c) + a := by ac_rfl
 
-@[bv_normalize]
-theorem BitVec.zero_sshiftRight : BitVec.sshiftRight 0#w a = 0#w := by
-  ext
-  simp [BitVec.getLsbD_sshiftRight]
-
-@[bv_normalize]
-theorem BitVec.sshiftRight_zero : BitVec.sshiftRight a 0 = a := by
-  ext
-  simp [BitVec.getLsbD_sshiftRight]
-
-@[bv_normalize]
-theorem BitVec.mul_zero (a : BitVec w) : a * 0#w = 0#w := by
-  simp [bv_toNat]
+attribute [bv_normalize] BitVec.zero_sshiftRight
+attribute [bv_normalize] BitVec.sshiftRight_zero
+attribute [bv_normalize] BitVec.mul_zero
+attribute [bv_normalize] BitVec.zero_mul
 
-@[bv_normalize]
-theorem BitVec.zero_mul (a : BitVec w) : 0#w * a = 0#w := by
-  simp [bv_toNat]
+attribute [bv_normalize] BitVec.shiftLeft_zero
+attribute [bv_normalize] BitVec.zero_shiftLeft
 
 @[bv_normalize]
-theorem BitVec.shiftLeft_zero (n : BitVec w) : n <<< 0#w' = n := by
+theorem BitVec.shiftLeft_zero' (n : BitVec w) : n <<< 0#w' = n := by
   ext i
   simp only [(· <<< ·)]
   simp
 
-@[bv_normalize]
-theorem BitVec.shiftLeft_zero' (n : BitVec w) : n <<< 0 = n := by
-  ext i
-  simp
-
-@[bv_normalize]
-theorem BitVec.zero_shiftLeft (n : Nat) : 0#w <<< n = 0#w := by
-  ext
-  simp
-
-@[bv_normalize]
-theorem BitVec.zero_shiftRight (n : Nat) : 0#w >>> n = 0#w := by
-  ext
-  simp
+attribute [bv_normalize] BitVec.zero_sshiftRight
+attribute [bv_normalize] BitVec.sshiftRight_zero
 
 @[bv_normalize]
-theorem BitVec.shiftRight_zero (n : BitVec w) : n >>> 0#w' = n := by
+theorem BitVec.shiftRight_zero' (n : BitVec w) : n >>> 0#w' = n := by
   ext i
   simp only [(· >>> ·)]
   simp
 
-@[bv_normalize]
-theorem BitVec.shiftRight_zero' (n : BitVec w) : n >>> 0 = n := by
-  ext i
-  simp
 
 theorem BitVec.zero_lt_iff_zero_neq (a : BitVec w) : (0#w < a) ↔ (a ≠ 0#w) := by
   constructor <;>