chore: changed the name of simp_alive_bitvec and refactored hacker …

…delight's tests accordingly (#592)

SSA/Projects/InstCombine/HackersDelight/AdditionAndLogicalOps.lean

@@ -12,91 +12,91 @@ variable {x y z : BitVec w}
 
 theorem neg_eq_not_add_one :
     -x = ~~~ x + 1 := by
-  alive_auto
+  bv_auto
 
 theorem neg_eq_neg_not_one :
     -x = ~~~ (x - 1) := by
-  alive_auto
+  bv_auto
 
 theorem not_eq_neg_sub_one :
     ~~~ x = - x - 1:= by
-  alive_auto
+  bv_auto
 
 theorem neg_not_eq_add_one :
     - ~~~ x = x + 1 := by
-  alive_auto
+  bv_auto
 
 theorem not_neg_eq_sub_one :
     ~~~ (-x) = x - 1 := by
-  alive_auto
+  bv_auto
 
 theorem add_eq_sub_not_sub_one :
     x + y = x - ~~~ y - 1 := by
-  alive_auto
+  bv_auto
 
 theorem add_eq_xor_add_mul_and :
     x + y = (x ^^^ y) + 2 * (x &&& y) := by
-  alive_auto
+  bv_auto
 
 theorem add_eq_or_add_and :
     x + y = (x ||| y) + (x &&& y) := by
-  alive_auto
+  bv_auto
 
 theorem add_eq_mul_or_neg_xor :
     x + y = 2 * (x ||| y) - (x ^^^ y) := by
-  alive_auto
+  bv_auto
 
 theorem sub_eq_add_not_add_one :
     x - y = x + ~~~ y + 1 := by
-  alive_auto
+  bv_auto
 
 theorem sub_eq_xor_sub_mul_not_and :
     x - y = (x ^^^ y) - 2 * (~~~ x &&& y) := by
-  alive_auto
+  bv_auto
 
 theorem sub_eq_and_not_sub_not_and :
     x - y = (x &&& ~~~ y) - (~~~ x &&& y) := by
-  alive_auto
+  bv_auto
 
 theorem sub_eq_mul_and_not_sub_xor :
     x - y = 2 * (x &&& ~~~ y) - (x ^^^ y) := by
-  alive_auto
+  bv_auto
 
 theorem xor_eq_or_sub_and :
     x ^^^ y = (x ||| y) - (x &&& y) := by
-  alive_auto
+  bv_auto
 
 theorem and_not_eq_or_sub:
     x &&& ~~~ y = (x ||| y) - y := by
-  alive_auto
+  bv_auto
 
 theorem and_not_eq_sub_add :
     x &&& ~~~ y = x - (x &&& y) := by
-  alive_auto
+  bv_auto
 
 theorem not_sub_eq_sub_sub_one :
     ~~~ (x - y) = y - x - 1 := by
-  alive_auto
+  bv_auto
 
 theorem not_sub_eq_not_add :
     ~~~ (x - y) = ~~~x + y := by
-  alive_auto
+  bv_auto
 
 theorem not_xor_eq_and_sub_or_sub_one :
     ~~~ (x ^^^ y) = (x &&& y) - (x ||| y) - 1 := by
-  alive_auto
+  bv_auto
 
 theorem not_xor_eq_and_add_not_or :
     ~~~ (x ^^^ y) = (x &&& y) + ~~~ (x ||| y) := by
-  alive_auto
+  bv_auto
 
 theorem or_eq_and_not_add :
     x ||| y = (x &&& ~~~ y) + y := by
-  alive_auto
+  bv_auto
 
 theorem and_eq_not_or_sub_not :
     x &&& y = (~~~ x ||| y) - ~~~ x := by
-  alive_auto
+  bv_auto
 
 end AdditionCombinedWithLogicalOperations
 

SSA/Projects/InstCombine/HackersDelight/DeMorgan.lean

@@ -12,39 +12,39 @@ variable {x y z : BitVec w}
 
 theorem not_and_eq_not_or_not :
     ~~~ (x &&& y) = ~~~ x ||| ~~~ y := by
-  alive_auto
+  bv_auto
 
 theorem not_or_eq_not_and_not :
     ~~~ (x ||| y) = ~~~ x &&& ~~~ y := by
-  alive_auto
+  bv_auto
 
 theorem not_add_one_eq_not_sub_one :
     ~~~ (x + 1) = ~~~ x - 1 := by
-  alive_auto
+  bv_auto
 
 theorem not_sub_one_eq_not_add_one :
     ~~~ (x - 1) = ~~~ x + 1 := by
-  alive_auto
+  bv_auto
 
 theorem not_neg_eq_sub_one :
     ~~~ (- x) = x - 1 := by
-  alive_auto
+  bv_auto
 
 theorem not_xor_eq_not_xor :
     ~~~ (x ^^^ y) = ~~~ x ^^^ y := by
-  alive_auto
+  bv_auto
 
 theorem q_not_xor :
     ~~~ (x ^^^ y) = ~~~ x ^^^ y := by
-  alive_auto
+  bv_auto
 
 theorem not_add_eq_not_sub :
     ~~~ (x + y) = ~~~ x - y := by
-  alive_auto
+  bv_auto
 
 theorem not_sub_eq_not_add :
     ~~~ (x - y) = ~~~ x + y := by
-  alive_auto
+  bv_auto
 
 end DeMorgansLawsExtended
 

SSA/Projects/InstCombine/TacticAuto.lean

@@ -106,7 +106,7 @@ macro "of_bool_tactic" : tactic =>
     )
     ))
 
-macro "simp_alive_bitvec": tactic =>
+macro "bv_auto": tactic =>
   `(tactic|
       (
         intros
@@ -155,6 +155,6 @@ macro "alive_auto": tactic =>
           simp_alive_case_bash
           ensure_only_goal
         )
-        simp_alive_bitvec
+        bv_auto
       )
    )