refactor: change iff lowering rule in bv_decide (#7287)

This PR uses a better lowering rule for iff in bv_decide's
preprocessing.

Author: hargoniX

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

@@ -52,9 +52,6 @@ theorem if_eq_cond {b : Bool} {x y : α} : (if b = true then x else y) = (bif b
 @[bv_normalize]
 theorem Bool.not_xor : ∀ (a b : Bool), !(a ^^ b) = (a == b) := by decide
 
-@[bv_normalize]
-theorem Bool.or_elim : ∀ (a b : Bool), (a || b) = !(!a && !b) := by decide
-
 @[bv_normalize]
 theorem Bool.not_beq_one : ∀ (a : BitVec 1), (!(a == 1#1)) = (a == 0#1) := by
   decide

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

@@ -54,9 +54,8 @@ theorem Bool.and_to_and (a b : Bool) : ((a = true) ∧ (b = true)) = ((a && b) =
   simp
 
 @[bv_normalize]
-theorem Bool.iff_to_or (a b : Bool)
-    : ((a = true) ↔ (b = true)) = (((!a || b) && (!b || a)) = true) := by
-  revert a b
+theorem Bool.iff_to_beq :
+    ∀ (a b : Bool), ((a = true) ↔ (b = true)) = ((a == b) = true) := by
   decide
 
 @[bv_normalize]
@@ -67,10 +66,6 @@ theorem Bool.eq_false (a : Bool) : ((a = true) = False) = ((!a) = true) := by
 theorem Bool.decide_eq_true (a : Bool) : (decide (a = true)) = a := by
   simp
 
-@[bv_normalize]
-theorem Bool.eq_true_eq_true_eq (x y : Bool) : ((x = true) = (y = true)) ↔ ((x == y) = true) := by
-  simp
-
 attribute [bv_normalize] BitVec.getLsbD_cast
 attribute [bv_normalize] BitVec.testBit_toNat
 
@@ -80,10 +75,13 @@ theorem BitVec.lt_ult (x y : BitVec w) : (x < y) = (BitVec.ult x y = true) := by
   simp only [(· < ·)]
   simp
 
+@[bv_normalize]
+theorem Bool.or_elim : ∀ (a b : Bool), (a || b) = !(!a && !b) := by decide
+
 @[bv_normalize]
 theorem BitVec.or_elim (x y : BitVec w) : x ||| y = ~~~(~~~x &&& ~~~y) := by
   ext
-  simp_all
+  simp
 
 attribute [bv_normalize] BitVec.natCast_eq_ofNat
 attribute [bv_normalize] BitVec.append_eq

tests/lean/run/bv_decide_rewriter.lean

@@ -26,6 +26,7 @@ theorem mem_subset_refl : mem_subset a1 a2 a1 a2 := by
   unfold mem_subset
   bv_normalize
 
+example (a b : Bool) : ((a = true) ↔ (b = true)) ↔ (a == b) := by bv_normalize
 example {x : BitVec 16} : 0#16 + x = x := by bv_normalize
 example {x : BitVec 16} : x + 0#16 = x := by bv_normalize
 example {x : BitVec 16} : x.setWidth 16 = x := by bv_normalize