From 5f22ba7789bd2985b493c8d79741d7d07fff5a88 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Sat, 28 Sep 2024 12:05:16 +0200 Subject: [PATCH] feat: bv_normalize handle -> False (#5507) --- src/Std/Tactic/BVDecide/Normalize/Prop.lean | 1 + tests/lean/run/bv_decide_rewriter.lean | 3 +++ 2 files changed, 4 insertions(+) diff --git a/src/Std/Tactic/BVDecide/Normalize/Prop.lean b/src/Std/Tactic/BVDecide/Normalize/Prop.lean index 6cf7473a30..4e723caa60 100644 --- a/src/Std/Tactic/BVDecide/Normalize/Prop.lean +++ b/src/Std/Tactic/BVDecide/Normalize/Prop.lean @@ -30,6 +30,7 @@ attribute [bv_normalize] true_iff attribute [bv_normalize] iff_false attribute [bv_normalize] false_iff attribute [bv_normalize] false_implies +attribute [bv_normalize] imp_false attribute [bv_normalize] implies_true attribute [bv_normalize] true_implies attribute [bv_normalize] not_true diff --git a/tests/lean/run/bv_decide_rewriter.lean b/tests/lean/run/bv_decide_rewriter.lean index b1cc02f0ec..3d696fc605 100644 --- a/tests/lean/run/bv_decide_rewriter.lean +++ b/tests/lean/run/bv_decide_rewriter.lean @@ -13,3 +13,6 @@ example (z : BitVec 64) : True := by 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 + +example (x y z : BitVec 8) (h1 : x = z → False) (h2 : x = y) (h3 : y = z) : False := by + bv_decide