From 2cb89823f3c207a9abc412e4410249ece767fb39 Mon Sep 17 00:00:00 2001 From: Siddharth Date: Fri, 14 Mar 2025 13:21:17 +0000 Subject: [PATCH] feat: BitVec.BV_ADD_NEG_MUL (#7481) 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 --- src/Init/Data/BitVec/Lemmas.lean | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index 09bb88b77e..9defbee5f9 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -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} :