From 09e8079ea3a7dd9a57cae5b417c7f2d84c8fcb81 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Tue, 5 Aug 2025 13:43:43 +0200 Subject: [PATCH] fix: U/SIntX BEq handling in bv_decide (#9728) This PR fixes #9724 --- src/Std/Tactic/BVDecide/Normalize/BitVec.lean | 31 +++++++++++++++++++ tests/lean/run/bv_uint.lean | 12 +++++++ 2 files changed, 43 insertions(+) diff --git a/src/Std/Tactic/BVDecide/Normalize/BitVec.lean b/src/Std/Tactic/BVDecide/Normalize/BitVec.lean index 1846b2fb5f..d1938b204d 100644 --- a/src/Std/Tactic/BVDecide/Normalize/BitVec.lean +++ b/src/Std/Tactic/BVDecide/Normalize/BitVec.lean @@ -592,5 +592,36 @@ theorem ISize.toBitVec_ite [Decidable c] : ISize.toBitVec (if c then t else e) = if c then t.toBitVec else e.toBitVec := by rw [apply_ite ISize.toBitVec] +@[int_toBitVec] +theorem UInt8.beq_eq_decide_eq {a b : UInt8} : (a == b) = decide (a = b) := Bool.beq_eq_decide_eq .. + +@[int_toBitVec] +theorem UInt16.beq_eq_decide_eq {a b : UInt16} : (a == b) = decide (a = b) := Bool.beq_eq_decide_eq .. + +@[int_toBitVec] +theorem UInt32.beq_eq_decide_eq {a b : UInt32} : (a == b) = decide (a = b) := Bool.beq_eq_decide_eq .. + +@[int_toBitVec] +theorem UInt64.beq_eq_decide_eq {a b : UInt64} : (a == b) = decide (a = b) := Bool.beq_eq_decide_eq .. + +@[int_toBitVec] +theorem USize.beq_eq_decide_eq {a b : USize} : (a == b) = decide (a = b) := Bool.beq_eq_decide_eq .. + +@[int_toBitVec] +theorem Int8.beq_eq_decide_eq {a b : Int8} : (a == b) = decide (a = b) := Bool.beq_eq_decide_eq .. + +@[int_toBitVec] +theorem Int16.beq_eq_decide_eq {a b : Int16} : (a == b) = decide (a = b) := Bool.beq_eq_decide_eq .. + +@[int_toBitVec] +theorem Int32.beq_eq_decide_eq {a b : Int32} : (a == b) = decide (a = b) := Bool.beq_eq_decide_eq .. + +@[int_toBitVec] +theorem Int64.beq_eq_decide_eq {a b : Int64} : (a == b) = decide (a = b) := Bool.beq_eq_decide_eq .. + +@[int_toBitVec] +theorem ISize.beq_eq_decide_eq {a b : ISize} : (a == b) = decide (a = b) := Bool.beq_eq_decide_eq .. + + end Normalize end Std.Tactic.BVDecide diff --git a/tests/lean/run/bv_uint.lean b/tests/lean/run/bv_uint.lean index 6789f1eeed..d37bca0784 100644 --- a/tests/lean/run/bv_uint.lean +++ b/tests/lean/run/bv_uint.lean @@ -86,3 +86,15 @@ example (n : Int8) : n.toUInt8.toInt8 = n := by bv_decide example (n : Int16) : n.toUInt16.toInt16 = n := by bv_decide example (n : Int32) : n.toUInt32.toInt32 = n := by bv_decide example (n : Int64) : n.toUInt64.toInt64 = n := by bv_decide + +example {b : UInt8} (h : b &&& 0x80 == 0) : b < 0x80 := by bv_decide + +example (x y z: UInt8) (h1 : x == y) (h2 : y == z) : x == z := by bv_decide +example (x y z: UInt16) (h1 : x == y) (h2 : y == z) : x == z := by bv_decide +example (x y z: UInt32) (h1 : x == y) (h2 : y == z) : x == z := by bv_decide +example (x y z: UInt64) (h1 : x == y) (h2 : y == z) : x == z := by bv_decide + +example (x y z: Int8) (h1 : x == y) (h2 : y == z) : x == z := by bv_decide +example (x y z: Int16) (h1 : x == y) (h2 : y == z) : x == z := by bv_decide +example (x y z: Int32) (h1 : x == y) (h2 : y == z) : x == z := by bv_decide +example (x y z: Int64) (h1 : x == y) (h2 : y == z) : x == z := by bv_decide