inspiration: two more theorem classes (#446)

Co-authored-by: Atticus Kuhn <[email protected]>

SSA/Projects/InstCombine/TacticAuto.lean

@@ -112,6 +112,40 @@ macro "simp_alive_bitvec": tactic =>
       )
    )
 
+  /-
+  This tactic attempts to shift ofBool to the outer-most level,
+  and then convert everything to arithmetic
+  and then solve with the omega tactic.
+  -/
+macro "of_bool_tactic" : tactic =>
+  `(tactic|
+    (
+      repeat (
+        first
+      | simp [bv_ofBool]
+      | simp [ForLean.ofBool_eq']
+      | simp
+      | simp only [bne]
+      )
+      repeat (
+        first
+      | simp only [BitVec.ule]
+      | simp only [BitVec.ult]
+      | simp only [BitVec.sle]
+      | simp only [BitVec.slt]
+      | simp only [BitVec.toInt]
+      | simp only [BEq.beq]
+      | simp only [← Bool.decide_or]
+      | simp only [← Bool.decide_and]
+      | simp only [← decide_not]
+      | simp only [decide_eq_decide]
+      | simp [of_decide_eq_true]
+      | simp only [BitVec.toNat_eq]
+      )
+      try omega
+    )
+  )
+
 macro "alive_auto": tactic =>
   `(tactic|
       (
@@ -122,5 +156,6 @@ macro "alive_auto": tactic =>
           ensure_only_goal
         )
         simp_alive_bitvec
+        of_bool_tactic
       )
    )