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

feat: BitVec.shiftLeft_neg_eq_neg_shiftLeft (#7508)

Browse source 
This PR shows that negation commutes with left shift, which is the
Bitwuzla rewrite
[NORM_BV_SHL_NEG](e09c50818b/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 <github@grosser.es>
This commit is contained in:
Siddharth 2025-03-17 11:54:43 +00:00 • committed by GitHub
parent e77b528ef5
commit 6df6011641
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 4 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

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