max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: U/SIntX BEq handling in bv_decide (#9728)

Browse source 
This PR fixes #9724
This commit is contained in:
Henrik Böving 2025-08-05 13:43:43 +02:00 • committed by GitHub
parent b42a7780e2
commit 09e8079ea3
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 43 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

31
src/Std/Tactic/BVDecide/Normalize/BitVec.lean
View file

@ -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

12
tests/lean/run/bv_uint.lean
View file

@ -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