From 6df60116410edea005d07e438c1ae579a41f17dd Mon Sep 17 00:00:00 2001 From: Siddharth Date: Mon, 17 Mar 2025 11:54:43 +0000 Subject: [PATCH] feat: BitVec.shiftLeft_neg_eq_neg_shiftLeft (#7508) This PR shows that negation commutes with left shift, which is the Bitwuzla rewrite [NORM_BV_SHL_NEG](https://github.com/bitwuzla/bitwuzla/blob/e09c50818b798f990bd84bf61174553fef46d561/src/rewrite/rewrites_bv_norm.cpp#L142-L148). ```lean theorem shiftLeft_neg_eq_neg_shiftLeft {x : BitVec w} {y : Nat} : (-x) <<< y = - (x <<< y) ``` --------- Co-authored-by: Tobias Grosser --- src/Init/Data/BitVec/Lemmas.lean | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index 06560a56d9..b5396b4aa7 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -4212,6 +4212,10 @@ theorem udiv_twoPow_eq_of_lt {w : Nat} {x : BitVec w} {k : Nat} (hk : k < w) : x have : 2^k < 2^w := Nat.pow_lt_pow_of_lt (by decide) hk simp [bitvec_to_nat, Nat.shiftRight_eq_div_pow, Nat.mod_eq_of_lt this] +theorem shiftLeft_neg {x : BitVec w} {y : Nat} : + (-x) <<< y = - (x <<< y) := by + rw [shiftLeft_eq_mul_twoPow, shiftLeft_eq_mul_twoPow, BitVec.neg_mul] + /- ### cons -/ @[simp] theorem true_cons_zero : cons true 0#w = twoPow (w + 1) w := by