feat: improve bv_normalize rules for Prop and == (#5506)

leanprover · Sep 28, 2024 · 16a1689 · 16a1689
1 parent 4ea76aa
commit 16a1689
Show file tree

Hide file tree

Showing 3 changed files with 26 additions and 2 deletions.
diff --git 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
@@ -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
@@ -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