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

feat: add BitVec.[(toFin, toInt)_setWidth', msb_setWidth'_of_lt, toNat_lt_twoPow_of_le, toInt_setWidth'_of_lt] (#7661)

Browse source 
This PR adds theorems `BitVec.[(toFin, toInt)_setWidth',
msb_setWidth'_of_lt, toNat_lt_twoPow_of_le, toInt_setWidth'_of_lt]`,
completing the API for `BitVec.setWidth'`.

Co-authored by @alexkeizer.

---------

Co-authored-by: Alex Keizer <alex@keizer.dev>
Co-authored-by: Siddharth <siddu.druid@gmail.com>
This commit is contained in:
Luisa Cicolini 2025-03-25 10:59:54 +00:00 • committed by GitHub
parent 0eb46541e3
commit 3b40e0e588
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 29 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -128,6 +128,12 @@ theorem toNat_ne_iff_ne {n} {x y : BitVec n} : x.toNat ≠ y.toNat ↔ x ≠ y :
@[bitvec_to_nat] theorem toNat_ne {x y : BitVec n} : x ≠ y ↔ x.toNat ≠ y.toNat := by
rw [Ne, toNat_eq]
protected theorem toNat_lt_twoPow_of_le (h : m ≤ n) {x : BitVec m} :
x.toNat < 2 ^ n := by
apply Nat.lt_of_lt_of_le x.isLt
apply Nat.pow_le_pow_of_le
<;> omega
theorem testBit_toNat (x : BitVec w) : x.toNat.testBit i = x.getLsbD i := rfl
theorem getMsb'_eq_getLsb' (x : BitVec w) (i : Fin w) :
@ -924,6 +930,29 @@ and the second `setWidth` is a non-trivial extension.
have := @lt_of_getLsbD u x i
by_cases h' : x.getLsbD i = true <;> simp [h'] at * <;> omega
@[simp] theorem msb_setWidth'_of_lt {m n : Nat} (p : m < n) {x : BitVec m} :
(setWidth' (by omega : m ≤ n) x).msb = false := by
have h : x.getLsbD (n - 1) = false := getLsbD_ge _ _ (by omega)
simp [msb_setWidth', -setWidth'_eq, h]
@[simp] theorem toInt_setWidth'_of_lt {m n : Nat} (p : m < n) {x : BitVec m} :
(setWidth' (by omega : m ≤ n) x).toInt = x.toNat := by
rw [toInt_eq_toNat_of_msb]
· rfl
· apply msb_setWidth'_of_lt p
theorem toInt_setWidth' {m n : Nat} (p : m ≤ n) {x : BitVec m} :
(setWidth' p x).toInt = if m = n then x.toInt else x.toNat := by
split
case isTrue h => simp [h, toInt_eq_toNat_bmod]
case isFalse h => rw [toInt_setWidth'_of_lt (by omega)]
@[simp] theorem toFin_setWidth' {m n : Nat} (p : m ≤ n) (x : BitVec m) :
(setWidth' p x).toFin = x.toFin.castLE (Nat.pow_le_pow_right (by omega) (by omega)) := by
ext
rw [setWidth'_eq, toFin_setWidth, Fin.val_ofNat', Fin.coe_castLE, val_toFin,
Nat.mod_eq_of_lt (by apply BitVec.toNat_lt_twoPow_of_le p)]
/-! ## extractLsb -/
@[simp]