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

feat: add twoPow multiplication lemmas (#6742)

Browse source 
This PR adds the lemmas that show what happens when multiplying by
`twoPow` to an arbitrary term, as well to another `twoPow`.

This will be followed up by a PR that uses these to build a simproc to
canonicalize `twoPow w i * x` and `x * twoPow w i`.
This commit is contained in:
Siddharth 2025-01-22 19:05:17 +00:00 • committed by GitHub
parent 6595ca8f29
commit 6befda831d
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 11 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -3328,6 +3328,11 @@ theorem mul_twoPow_eq_shiftLeft (x : BitVec w) (i : Nat) :
apply Nat.pow_dvd_pow 2 (by omega)
simp [Nat.mul_mod, hpow]
theorem twoPow_mul_eq_shiftLeft (x : BitVec w) (i : Nat) :
(twoPow w i) * x = x <<< i := by
rw [BitVec.mul_comm, mul_twoPow_eq_shiftLeft]
theorem twoPow_zero {w : Nat} : twoPow w 0 = 1#w := by
apply eq_of_toNat_eq
simp
@ -3337,6 +3342,12 @@ theorem shiftLeft_eq_mul_twoPow (x : BitVec w) (n : Nat) :
ext i
simp [getLsbD_shiftLeft, Fin.is_lt, decide_true, Bool.true_and, mul_twoPow_eq_shiftLeft]
/-- 2^i * 2^j = 2^(i + j) with bitvectors as well -/
theorem twoPow_mul_twoPow_eq {w : Nat} (i j : Nat) : twoPow w i * twoPow w j = twoPow w (i + j) := by
apply BitVec.eq_of_toNat_eq
simp only [toNat_mul, toNat_twoPow]
rw [← Nat.mul_mod, Nat.pow_add]
/--
The unsigned division of `x` by `2^k` equals shifting `x` right by `k`,
when `k` is less than the bitwidth `w`.