From c6cb2f52f028882ff821394f447d569898546803 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Mon, 3 Feb 2025 19:19:34 +0100
Subject: [PATCH] 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
---
 .../BVDecide/Frontend/Normalize/Simproc.lean  | 28 +++++++++++++++++++
 src/Std/Tactic/BVDecide/Normalize/Equal.lean  | 10 +++++++
 tests/lean/run/bv_decide_rewriter.lean        |  7 +++++
 3 files changed, 45 insertions(+)

diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Simproc.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Simproc.lean
index 6fd90dec39be..7c4b390828e7 100644
--- a/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Simproc.lean
+++ b/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
diff --git a/src/Std/Tactic/BVDecide/Normalize/Equal.lean b/src/Std/Tactic/BVDecide/Normalize/Equal.lean
index a408b4c80f20..2b32d41db7a6 100644
--- a/src/Std/Tactic/BVDecide/Normalize/Equal.lean
+++ b/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
diff --git a/tests/lean/run/bv_decide_rewriter.lean b/tests/lean/run/bv_decide_rewriter.lean
index 7cbc18e7cf57..9f1a025a71db 100644
--- a/tests/lean/run/bv_decide_rewriter.lean
+++ b/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