From 16a16898d5cab567152234edc877f66ad43ac39a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Sat, 28 Sep 2024 11:21:48 +0200
Subject: [PATCH] feat: improve bv_normalize rules for Prop and == (#5506)

---
 .../Meta/Tactic/Simp/BuiltinSimprocs/BitVec.lean |  8 ++++++++
 src/Std/Tactic/BVDecide/Normalize/Prop.lean      | 16 ++++++++++++++--
 tests/lean/run/bv_decide_rewriter.lean           |  4 ++++
 3 files changed, 26 insertions(+), 2 deletions(-)

diff --git a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/BitVec.lean b/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/BitVec.lean
index a0ae2d71fb79..fa467069b4a4 100644
--- a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/BitVec.lean
+++ b/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/BitVec.lean
@@ -228,8 +228,16 @@ builtin_dsimproc [simp, seval] reduceOfNat (BitVec.ofNat _ _) := fun e => do
   if bv.toNat == v then return .continue -- already normalized
   return .done <| toExpr (BitVec.ofNat n v)
 
+/-- Simplification procedure for `=` on `BitVec`s. -/
 builtin_simproc [simp, seval] reduceEq  (( _ : BitVec _) = _)  := reduceBinPred ``Eq 3 (. = .)
+/-- Simplification procedure for `≠` on `BitVec`s. -/
 builtin_simproc [simp, seval] reduceNe  (( _ : BitVec _) ≠ _)  := reduceBinPred ``Ne 3 (. ≠ .)
+/-- Simplification procedure for `==` on `BitVec`s. -/
+builtin_dsimproc [simp, seval] reduceBEq  (( _ : BitVec _) == _)  :=
+  reduceBoolPred ``BEq.beq 4 (· == ·)
+/-- Simplification procedure for `!=` on `BitVec`s. -/
+builtin_dsimproc [simp, seval] reduceBNe  (( _ : BitVec _) != _)  :=
+  reduceBoolPred ``bne 4 (· != ·)
 
 /-- Simplification procedure for `<` on `BitVec`s. -/
 builtin_simproc [simp, seval] reduceLT (( _ : BitVec _) < _)  := reduceBinPred ``LT.lt 4 (· < ·)
diff --git a/src/Std/Tactic/BVDecide/Normalize/Prop.lean b/src/Std/Tactic/BVDecide/Normalize/Prop.lean
index ec2e92cd8baf..6cf7473a309b 100644
--- a/src/Std/Tactic/BVDecide/Normalize/Prop.lean
+++ b/src/Std/Tactic/BVDecide/Normalize/Prop.lean
@@ -13,16 +13,28 @@ This module contains the `Prop` simplifying part of the `bv_normalize` simp set.
 namespace Std.Tactic.BVDecide
 namespace Frontend.Normalize
 
-attribute [bv_normalize] not_true
+attribute [bv_normalize] ite_true
+attribute [bv_normalize] ite_false
+attribute [bv_normalize] dite_true
+attribute [bv_normalize] dite_false
 attribute [bv_normalize] and_true
 attribute [bv_normalize] true_and
+attribute [bv_normalize] and_false
+attribute [bv_normalize] false_and
 attribute [bv_normalize] or_true
 attribute [bv_normalize] true_or
-attribute [bv_normalize] eq_iff_iff
+attribute [bv_normalize] or_false
+attribute [bv_normalize] false_or
 attribute [bv_normalize] iff_true
 attribute [bv_normalize] true_iff
 attribute [bv_normalize] iff_false
 attribute [bv_normalize] false_iff
+attribute [bv_normalize] false_implies
+attribute [bv_normalize] implies_true
+attribute [bv_normalize] true_implies
+attribute [bv_normalize] not_true
+attribute [bv_normalize] not_false_iff
+attribute [bv_normalize] eq_iff_iff
 
 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 ed1afbc01eec..b1cc02f0ecdc 100644
--- a/tests/lean/run/bv_decide_rewriter.lean
+++ b/tests/lean/run/bv_decide_rewriter.lean
@@ -9,3 +9,7 @@ example (z : BitVec 64) : True := by
   have : z + (2 * x) = y := by
     bv_decide
   exact True.intro
+
+example :
+  ¬ (0 ≤ 0 + 16#64 ∧ 0 ≤ 0 + 16#64 ∧ (0 + 16#64 ≤ 0 ∨ 0 ≥ 0 + 16#64 ∨ 16#64 = 0 ∨ 16#64 = 0)) := by
+  bv_normalize