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

feat: add BitVec.toFin_abs (#7206)

Browse source 
This PR adds theorem `BitVec.toFin_abs`, completing the API for
`BitVec.*_abs`.

---------

Co-authored-by: Tobias Grosser <github@grosser.es>
This commit is contained in:
Luisa Cicolini 2025-02-24 17:02:51 +00:00 • committed by GitHub
parent af741abbf5
commit 32a9392a11
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

@ -4217,6 +4217,10 @@ theorem toInt_abs_eq_natAbs_of_ne_intMin {x : BitVec w} (hx : x ≠ intMin w) :
x.abs.toInt = x.toInt.natAbs := by
simp [toInt_abs_eq_natAbs, hx]
theorem toFin_abs {x : BitVec w} :
x.abs.toFin = if x.msb then Fin.ofNat' (2 ^ w) (2 ^ w - x.toNat) else x.toFin := by
by_cases h : x.msb <;> simp [BitVec.abs, h]
/-! ### Reverse -/
theorem getLsbD_reverse {i : Nat} {x : BitVec w} :