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

feat: BitVec.BV_ADD_NEG_MUL (#7481)

Browse source 
This PR implements the Bitwuzla rewrites [BV_ADD_NEG_MUL](), and
associated lemmas to make the proof streamlined. ```bvneg (bvadd a
(bvmul a b)) = (bvmul a (bvnot b))```, or spelled as lean:

```lean
theorem neg_add_mul_eq_mul_not {x y : BitVec w} :
    - (x + x * y) = (x * ~~~ y)
```

---------

Co-authored-by: Tobias Grosser <github@grosser.es>
This commit is contained in:
Siddharth 2025-03-14 13:21:17 +00:00 • committed by GitHub
parent 297be24c0d
commit 2cb89823f3
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 14 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
src/Init/Data/BitVec/Lemmas.lean
View file

@ -3094,6 +3094,14 @@ theorem not_neg (x : BitVec w) : ~~~(-x) = x + -1#w := by
show (_ - x.toNat) % _ = _ by rw [Nat.mod_eq_of_lt (by omega)]]
omega
theorem neg_add {x y : BitVec w} : - (x + y) = - x - y := by
apply eq_of_toInt_eq
simp [toInt_neg, toInt_add, Int.neg_add, Int.add_neg_eq_sub]
theorem add_neg_eq_sub {x y : BitVec w} : x + - y = (x - y) := by
apply eq_of_toInt_eq
simp [toInt_neg, Int.sub_eq_add_neg]
/- ### add/sub injectivity -/
@[simp]
@ -3262,6 +3270,12 @@ protected theorem neg_mul_neg (x y : BitVec w) : -x * -y = x * y := by simp
protected theorem neg_mul_comm (x y : BitVec w) : -x * y = x * -y := by simp
theorem neg_add_mul_eq_mul_not {x y : BitVec w} :
- (x + x * y) = x * ~~~ y := by
rw [neg_add, sub_toAdd, ← BitVec.mul_neg, neg_eq_not_add y, mul_add,
BitVec.mul_one, BitVec.add_comm, BitVec.add_assoc, BitVec.add_right_eq_self,
add_neg_eq_sub, BitVec.sub_self]
/-! ### le and lt -/
@[bitvec_to_nat] theorem le_def {x y : BitVec n} :