feat: bv_decide implement BV_EQUAL_CONST_NOT rules (#6926)

This PR adds the BV_EQUAL_CONST_NOT rules from Bitwuzla to the
preprocessor of bv_decide.

Stacked on top of #6924

src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Simproc.lean

@@ -160,5 +160,33 @@ builtin_simproc [bv_normalize] bv_udiv_of_two_pow (((_ : BitVec _) / (BitVec.ofN
       proof? := some proof
   }
 
+builtin_simproc [bv_normalize] bv_equal_const_not (~~~(_ : BitVec _) == (_ : BitVec _)) :=
+  fun e => do
+    let_expr BEq.beq α inst outerLhs rhs := e | return .continue
+    let some ⟨w, rhsVal⟩ ← getBitVecValue? rhs | return .continue
+    let_expr Complement.complement _ _ lhs := outerLhs | return .continue
+    let newRhs := ~~~rhsVal
+    let expr := mkApp4 (mkConst ``BEq.beq [0]) α inst lhs (toExpr newRhs)
+    let proof :=
+      mkApp3 (mkConst ``Std.Tactic.BVDecide.Frontend.Normalize.BitVec.not_eq_comm)
+        (toExpr w)
+        lhs
+        rhs
+    return .visit { expr := expr, proof? := some proof }
+
+builtin_simproc [bv_normalize] bv_equal_const_not' ((_ : BitVec _) == ~~~(_ : BitVec _)) :=
+  fun e => do
+    let_expr BEq.beq α inst lhs outerRhs := e | return .continue
+    let some ⟨w, lhsVal⟩ ← getBitVecValue? lhs | return .continue
+    let_expr Complement.complement _ _ rhs := outerRhs | return .continue
+    let newLhs := ~~~lhsVal
+    let expr := mkApp4 (mkConst ``BEq.beq [0]) α inst (toExpr newLhs) rhs
+    let proof :=
+      mkApp3 (mkConst ``Std.Tactic.BVDecide.Frontend.Normalize.BitVec.not_eq_comm')
+        (toExpr w)
+        lhs
+        rhs
+    return .visit { expr := expr, proof? := some proof }
+
 end Frontend.Normalize
 end Lean.Elab.Tactic.BVDecide

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

@@ -185,5 +185,15 @@ theorem BitVec.bif_eq_not_bif' (d : Bool) (a b c : BitVec w) :
     ((bif d then a else c) == ~~~(bif d then b else c)) = (bif d then a == ~~~b else c == ~~~c) := by
   cases d <;> simp
 
+-- used for bv_equal_const_not simproc
+theorem BitVec.not_eq_comm (a b : BitVec w) : (~~~a == b) = (a == ~~~b) := by
+  rw [Bool.eq_iff_iff]
+  simp [_root_.BitVec.not_eq_comm]
+
+-- used for bv_equal_const_not simproc
+theorem BitVec.not_eq_comm' (a b : BitVec w) : (a == ~~~b) = (~~~a == b) := by
+  rw [Bool.eq_iff_iff]
+  simp [_root_.BitVec.not_eq_comm]
+
 end Frontend.Normalize
 end Std.Tactic.BVDecide

tests/lean/run/bv_decide_rewriter.lean

@@ -229,6 +229,13 @@ example (d : Bool) (a b c : BitVec w) :
     ((bif d then a else c) == ~~~(bif d then b else c)) = (bif d then a == ~~~b else c == ~~~c) := by
   bv_normalize
 
+-- bv_equal_const_not
+example (a : BitVec 32) : (~~~a = 0#32) ↔ (a = -1) := by
+  bv_normalize
+
+example (a : BitVec 32) : (0#32 = ~~~a) ↔ (-1 = a) := by
+  bv_normalize
+
 section
 
 example (x y : BitVec 256) : x * y = y * x := by