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

feat: add BitVec.getElem_truncate (#5278)

Browse source 
Co-authored-by: luisacicolini <luisacicolini@gmail.com>
Co-authored-by: Kim Morrison <scott@tqft.net>
This commit is contained in:
Tobias Grosser 2024-09-16 09:59:33 +01:00 • committed by GitHub
parent c25d206647
commit 7952a7f74d
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 13 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -173,6 +173,10 @@ instance : GetElem (BitVec w) Nat Bool fun _ i => i < w where
theorem getElem_eq_testBit_toNat (x : BitVec w) (i : Nat) (h : i < w) :
x[i] = x.toNat.testBit i := rfl
theorem getLsbD_eq_getElem {x : BitVec w} {i : Nat} (h : i < w) :
x.getLsbD i = x[i] := by
simp [getLsbD, getElem_eq_testBit_toNat]
end getElem
section Int

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

@ -523,6 +523,15 @@ theorem getElem?_zeroExtend (m : Nat) (x : BitVec n) (i : Nat) :
all_goals (first | apply getLsbD_ge | apply Eq.symm; apply getLsbD_ge)
<;> omega
@[simp]
theorem getElem_truncate (m : Nat) (x : BitVec n) (i : Nat) (hi : i < m) :
(truncate m x)[i] = x.getLsbD i := by
simp only [getElem_zeroExtend]
theorem getElem?_truncate (m : Nat) (x : BitVec n) (i : Nat) :
(truncate m x)[i]? = if i < m then some (x.getLsbD i) else none :=
getElem?_zeroExtend m x i
theorem getLsbD_truncate (m : Nat) (x : BitVec n) (i : Nat) :
getLsbD (truncate m x) i = (decide (i < m) && getLsbD x i) :=
getLsbD_zeroExtend m x i