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

feat: add more constant related rewrites to bv_decide (#7438)

Browse source 
This PR adds the EQUAL_CONST_BV_ADD and BV_AND_CONST rules to
bv_decide's preprocessor.
This commit is contained in:
Henrik Böving 2025-03-11 14:37:12 +01:00 • committed by GitHub
parent bfe7b1fb34
commit 1731f2f850
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 60 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -375,5 +375,49 @@ theorem BitVec.mul_ones (a : BitVec w) : a * -1#w = -a := by
rw [_root_.BitVec.mul_neg]
simp
-- All push a to the lhs as the rhs is guaranteed to be a constant so this form improves sharing.
@[bv_normalize]
theorem BitVec.add_const_beq_const {a : BitVec w} :
((a + BitVec.ofNat w b) == BitVec.ofNat w c) = (a == BitVec.ofNat w c - BitVec.ofNat w b) := by
rw [Bool.eq_iff_iff]
simp [BitVec.eq_sub_iff_add_eq]
@[bv_normalize]
theorem BitVec.const_add_beq_const :
((BitVec.ofNat w b + a) == BitVec.ofNat w c) = (a == BitVec.ofNat w c - BitVec.ofNat w b) := by
rw [Bool.eq_iff_iff, BitVec.add_comm _ a]
simp [BitVec.eq_sub_iff_add_eq]
@[bv_normalize]
theorem BitVec.const_beq_add_const_beq :
(BitVec.ofNat w c == (a + BitVec.ofNat w b)) = (a == BitVec.ofNat w c - BitVec.ofNat w b) := by
rw [Bool.eq_iff_iff, Bool.beq_comm]
simp [BitVec.eq_sub_iff_add_eq]
@[bv_normalize]
theorem BitVec.const_beq_const_add_beq :
(BitVec.ofNat w c == (BitVec.ofNat w b + a)) = (a == BitVec.ofNat w c - BitVec.ofNat w b) := by
rw [Bool.eq_iff_iff, BitVec.add_comm _ a, Bool.beq_comm]
simp [BitVec.eq_sub_iff_add_eq]
@[bv_normalize]
theorem BitVec.and_const_left :
BitVec.ofNat w a &&& (BitVec.ofNat w b &&& c) = (BitVec.ofNat w a &&& BitVec.ofNat w b) &&& c := by
ac_rfl
@[bv_normalize]
theorem BitVec.and_const_right :
BitVec.ofNat w a &&& (b &&& BitVec.ofNat w c) = (BitVec.ofNat w a &&& BitVec.ofNat w c) &&& b := by
ac_rfl
@[bv_normalize]
theorem BitVec.and_const_left' :
(BitVec.ofNat w a &&& b) &&& BitVec.ofNat w c = (BitVec.ofNat w a &&& BitVec.ofNat w c) &&& b := by
ac_rfl
@[bv_normalize]
theorem BitVec.and_const_right' {a : BitVec w} :
(a &&& BitVec.ofNat w b) &&& BitVec.ofNat w c = (BitVec.ofNat w b &&& BitVec.ofNat w c) &&& a := by
ac_rfl
end Normalize
end Std.Tactic.BVDecide

20
tests/lean/run/bv_decide_rewriter.lean
View file

@ -291,16 +291,16 @@ example (a : BitVec 16) : a + a = a <<< 1 := by
bv_normalize
-- NOT_EQUAL_BV1_BOOL
example : ∀ (a : Bool), (!(a == true)) = (a == false) := by
example : ∀ (a : Bool), (!(a == true)) = (!a) := by
bv_normalize
example : ∀ (a : Bool), (!(a == false)) = (a == true) := by
example : ∀ (a : Bool), (!(a == false)) = a := by
bv_normalize
example : ∀ (a : Bool), (!(true == a)) = (a == false) := by
example : ∀ (a : Bool), (!(true == a)) = !a := by
bv_normalize
example : ∀ (a : Bool), (!(false == a)) = (a == true) := by
example : ∀ (a : Bool), (!(false == a)) = a := by
bv_normalize
example : ∀ (a : BitVec 1), (!(a == 1#1)) = (a == 0#1) := by
@ -561,6 +561,18 @@ example {a : BitVec 8} : a <<< 3 = BitVec.extractLsb' 0 5 a ++ 0#3 := by bv_norm
example {a : BitVec 8} : a <<< 8 = 0 := by bv_normalize
example {a : BitVec 8} : a <<< 12 = 0 := by bv_normalize
-- EQUAL_CONST_BV_ADD
example {a : BitVec 8} (h : a + 5 = 7) : a = 2 := by bv_normalize
example {a : BitVec 8} (h : 5 + a = 7) : a = 2 := by bv_normalize
example {a : BitVec 8} (h : 7 = a + 5) : a = 2 := by bv_normalize
example {a : BitVec 8} (h : 7 = 5 + a) : a = 2 := by bv_normalize
-- BV_AND_CONST
example {x : BitVec 8} : (10 &&& x) &&& 2 = 2 &&& x := by bv_normalize
example {x : BitVec 8} : (x &&& 10) &&& 2 = 2 &&& x := by bv_normalize
example {x : BitVec 8} : 2 &&& (x &&& 10) = 2 &&& x := by bv_normalize
example {x : BitVec 8} : 2 &&& (10 &&& x) = 2 &&& x := by bv_normalize
section
example (x y : BitVec 256) : x * y = y * x := by