From e4e9cf7c76ca7639e60dcba1c11683efdeda51ce Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Mon, 14 Oct 2024 07:48:03 +0100 Subject: [PATCH] chore: performance bug in bv_decide --- tests/lean/run/bv_arith_plus_bitwise.lean | 34 +++++++++++++++++++++++ 1 file changed, 34 insertions(+) create mode 100644 tests/lean/run/bv_arith_plus_bitwise.lean diff --git a/tests/lean/run/bv_arith_plus_bitwise.lean b/tests/lean/run/bv_arith_plus_bitwise.lean new file mode 100644 index 000000000000..30794fb14c1d --- /dev/null +++ b/tests/lean/run/bv_arith_plus_bitwise.lean @@ -0,0 +1,34 @@ +import Std.Tactic.BVDecide + +open BitVec + +set_option trace.Meta.Tactic.bv true + +theorem add_eq_sub_not_sub_one (x y : BitVec 32): + x + y = x - ~~~ y - 1 := by + bv_decide -- this one hangs with ac_nf enabled + +set_option bv.ac_nf false in +theorem add_eq_sub_not_sub_one' (x y : BitVec 32): + x + y = x - ~~~ y - 1 := by + bv_normalize + rename_i a + ac_nf at a + simp only [BitVec.reduceAdd] at a + simp only [BitVec.add_zero] at a + simp only [beq_self_eq_true] at a + simp only [Bool.not_true] at a + /- + case h + x y : BitVec 32 + a : false = true + ⊢ False + -/ + simp only [Bool.false_eq_true] at a -- here the proof hangs + +/-- +This one is fast. +-/ +theorem test (x y : BitVec 32) (a : false = true ) : + False := by + simp only [Bool.false_eq_true] at a