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

feat: add BitVec.[(toInt, toFin)_(extractLsb, extractLsb')] (#7605)

Browse source 
This PR adds theorems `BitVec.[(toInt, toFin)_(extractLsb,
extractLsb')]`, completing the API for `BitVec.(extractLsb,
extractLsb')`.
This commit is contained in:
Luisa Cicolini 2025-03-24 08:54:22 +00:00 • committed by GitHub
parent 5fa0e50440
commit 1e040672c0
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 16 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -939,6 +939,22 @@ protected theorem extractLsb_ofNat (x n : Nat) (hi lo : Nat) :
@[simp] theorem extractLsb_toNat (hi lo : Nat) (x : BitVec n) :
(extractLsb hi lo x).toNat = (x.toNat >>> lo) % 2^(hi-lo+1) := rfl
@[simp] theorem toInt_extractLsb' {s m : Nat} {x : BitVec n} :
(extractLsb' s m x).toInt = ((x.toNat >>> s) : Int).bmod (2 ^ m) := by
simp [extractLsb', toInt_ofNat]
@[simp] theorem toInt_extractLsb {hi lo : Nat} {x : BitVec n} :
(extractLsb hi lo x).toInt = ((x.toNat >>> lo) : Int).bmod (2 ^ (hi - lo + 1)) := by
simp [extractLsb, toInt_ofNat]
@[simp] theorem toFin_extractLsb' {s m : Nat} {x : BitVec n} :
(extractLsb' s m x).toFin = Fin.ofNat' (2 ^ m) (x.toNat >>> s) := by
simp [extractLsb', toInt_ofNat]
@[simp] theorem toFin_extractLsb {hi lo : Nat} {x : BitVec n} :
(extractLsb hi lo x).toFin = Fin.ofNat' (2 ^ (hi - lo + 1)) (x.toNat >>> lo) := by
simp [extractLsb, toInt_ofNat]
@[simp] theorem getElem_extractLsb' {start len : Nat} {x : BitVec n} {i : Nat} (h : i < len) :
(extractLsb' start len x)[i] = x.getLsbD (start+i) := by
simp [getElem_eq_testBit_toNat, getLsbD, h]