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

feat: add BitVec.(toFin_signExtend_of_le, toFin_signExtend) (#7658)

Browse source 
This PR introduces `BitVec.(toFin_signExtend_of_le, toFin_signExtend)`,
completing the API for `BitVec.signExtend`.

Co-authored by @bollu.

---------

Co-authored-by: Tobias Grosser <github@grosser.es>
This commit is contained in:
Luisa Cicolini 2025-03-25 09:21:11 +00:00 • committed by GitHub
parent bd0b138f7c
commit 69a03ba00b
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 17 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -2414,6 +2414,23 @@ theorem toInt_signExtend_eq_toInt_bmod_of_le (x : BitVec w) (h : v ≤ w) :
(x.signExtend v).toInt = x.toInt.bmod (2 ^ v) := by
rw [BitVec.toInt_signExtend, Nat.min_eq_left h]
theorem toFin_signExtend_of_le {x : BitVec w} (hv : v ≤ w):
(x.signExtend v).toFin = Fin.ofNat' (2 ^ v) x.toNat := by
simp [signExtend_eq_setWidth_of_le _ hv]
theorem toFin_signExtend (x : BitVec w) :
(x.signExtend v).toFin = Fin.ofNat' (2 ^ v) (x.toNat + if x.msb = true then 2 ^ v - 2 ^ w else 0):= by
by_cases hv : v ≤ w
· simp [toFin_signExtend_of_le hv, show 2 ^ v - 2 ^ w = 0 by rw [@Nat.sub_eq_zero_iff_le]; apply Nat.pow_le_pow_of_le (by decide) (by omega)]
· simp only [Nat.not_le] at hv
apply Fin.eq_of_val_eq
simp only [val_toFin, Fin.val_ofNat']
rw [toNat_signExtend_of_le _ (by omega)]
have : 2 ^ w < 2 ^ v := by apply Nat.pow_lt_pow_of_lt <;> omega
rw [Nat.mod_eq_of_lt]
rcases x.msb <;> simp <;> omega
@[simp] theorem signExtend_and {x y : BitVec w} :
(x &&& y).signExtend v = (x.signExtend v) &&& (y.signExtend v) := by
refine eq_of_getElem_eq (fun i hi => ?_)