feat: eliminate sequences of BitVec.ofBool (#303)

This solves one additional theorems and simplifies a number of theorems
we are seeing. We are now at 50/93 solved statements.

SSA/Projects/InstCombine/ForLean.lean

@@ -834,6 +834,22 @@ theorem and_add_xor_eq_or {a b : BitVec w} : (a &&& b) + (a ^^^ b) = a ||| b :=
   simp only [Bool.bne_assoc]
   cases a.getLsb ↑i <;> simp [carry_and_xor_false]
 
+@[bv_ofBool]
+theorem ofBool_or {a b : Bool} : BitVec.ofBool a ||| BitVec.ofBool b = ofBool (a || b) := by
+  simp [bv_toNat]; rcases a <;> rcases b <;> rfl
+
+@[bv_ofBool]
+theorem ofBool_and {a b : Bool} : BitVec.ofBool a &&& BitVec.ofBool b = ofBool (a && b) := by
+  simp [bv_toNat]; rcases a <;> rcases b <;> rfl
+
+@[bv_ofBool]
+theorem ofBool_xor {a b : Bool} : BitVec.ofBool a ^^^ BitVec.ofBool b = ofBool (a.xor b) := by
+  simp [bv_toNat]; rcases a <;> rcases b <;> rfl
+
+@[simp]
+theorem ofBool_eq' : ofBool a = ofBool b ↔ a = b:= by
+  rcases a <;> rcases b <;> simp [bv_toNat]
+
 end BitVec
 
 -- Given (a, b) that are less than a modulus m, to show (a + b) % m < k, it suffices to consider two cases.

SSA/Projects/InstCombine/LLVM/SimpSet.lean

@@ -11,3 +11,5 @@ register_simp_attr simp_llvm_wrap
 
 /-- The simp-set used in `simp_alive_case_bash` to attempt to discharge trivial `none` cases -/
 register_simp_attr simp_llvm_case_bash
+
+register_simp_attr bv_ofBool

SSA/Projects/InstCombine/TacticAuto.lean

@@ -78,5 +78,6 @@ macro "alive_auto": tactic =>
                      try cases BitVec.getLsb _ _ <;> try simp;
                      try cases BitVec.getLsb _ _ <;> try simp;
                      try cases BitVec.getLsb _ _ <;> try simp;)
+        try solve | (simp [bv_ofBool])
       )
    )