feat: add BitVec.[zero_ushiftRight|zero_sshiftRight|zero_mul] and clean up BVDecide

- Fix names

  shiftLeft_zero_eq -> shiftLeft_zero
  ushiftRight_zero_eq -> ushiftRight_zero

- Remove duplicate prefixes

  BitVec.mul_zero -> mul_zero
  BitVec.mul_add  -> mul_add

- Adapt BVDecide/Normalize/BitVec by reusing the following functions

  zero_add | add_zero
  and_self
  mul_zero | zero_mul
  shiftLeft_zero | zero_shiftLeft
  sshiftRight_zero | zero_sshiftRight
  ushiftRight_zero | zero_ushiftRight

Author: tobiasgrosser

src/Init/Data/BitVec/Lemmas.lean

@@ -1062,7 +1062,7 @@ theorem not_eq_comm {x y : BitVec w} : ~~~ x = y ↔ x = ~~~ y := by
     BitVec.toFin (x <<< n) = Fin.ofNat' (2^w) (x.toNat <<< n) := rfl
 
 @[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 +1232,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 +1391,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 +2161,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]
 
-theorem BitVec.mul_add {x y z : BitVec w} :
+@[simp]
+theorem zero_mul {x : BitVec w} : 0#w * x = 0#w := by
+  apply eq_of_toNat_eq
+  simp [toNat_mul]
+
+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
@@ -3179,4 +3192,10 @@ abbrev and_one_eq_zeroExtend_ofBool_getLsbD := @and_one_eq_setWidth_ofBool_getLs
 @[deprecated msb_sshiftRight (since := "2024-10-03")]
 abbrev sshiftRight_msb_eq_msb := @msb_sshiftRight
 
+@[deprecated shiftLeft_zero (since := "2024-10-27")]
+abbrev shiftLeft_zero_eq := @shiftLeft_zero
+
+@[deprecated ushiftRight_zero (since := "2024-10-27")]
+abbrev ushiftRight_zero_eq := @ushiftRight_zero
+
 end BitVec

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,56 +192,30 @@ 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.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
+attribute [bv_normalize] BitVec.zero_sshiftRight
+attribute [bv_normalize] BitVec.sshiftRight_zero
 
-@[bv_normalize]
-theorem BitVec.zero_shiftRight (n : Nat) : 0#w >>> n = 0#w := by
-  ext
-  simp
+attribute [bv_normalize] BitVec.zero_ushiftRight
+attribute [bv_normalize] BitVec.ushiftRight_zero
 
 @[bv_normalize]
-theorem BitVec.shiftRight_zero (n : BitVec w) : n >>> 0#w' = n := by
+theorem BitVec.ushiftRight_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 <;>
     simp_all only [BitVec.lt_def, BitVec.toNat_ofNat, Nat.zero_mod, ne_eq, BitVec.toNat_eq] <;>