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

feat: BitVec.[toInt|toFin|getMsbD]_ofBool (#6317)

Browse source 
This PR completes the basic API for BitVec.ofBool.

---------

Co-authored-by: Kim Morrison <scott@tqft.net>
This commit is contained in:
Tobias Grosser 2024-12-10 08:46:24 +00:00 • committed by GitHub
parent a805946466
commit 17865394d4
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 11 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -241,8 +241,11 @@ theorem toFin_one : toFin (1 : BitVec w) = 1 := by
@[simp] theorem toNat_ofBool (b : Bool) : (ofBool b).toNat = b.toNat := by
cases b <;> rfl
@[simp] theorem msb_ofBool (b : Bool) : (ofBool b).msb = b := by
cases b <;> simp [BitVec.msb, getMsbD, getLsbD]
@[simp] theorem toInt_ofBool (b : Bool) : (ofBool b).toInt = -b.toInt := by
cases b <;> rfl
@[simp] theorem toFin_ofBool (b : Bool) : (ofBool b).toFin = Fin.ofNat' 2 (b.toNat) := by
cases b <;> rfl
theorem ofNat_one (n : Nat) : BitVec.ofNat 1 n = BitVec.ofBool (n % 2 = 1) := by
rcases (Nat.mod_two_eq_zero_or_one n) with h | h <;> simp [h, BitVec.ofNat, Fin.ofNat']
@ -366,6 +369,12 @@ theorem getElem_ofBool {b : Bool} {i : Nat} : (ofBool b)[0] = b := by
· simp only [ofBool]
by_cases hi : i = 0 <;> simp [hi] <;> omega
@[simp] theorem getMsbD_ofBool (b : Bool) : (ofBool b).getMsbD i = (decide (i = 0) && b) := by
cases b <;> simp [getMsbD]
@[simp] theorem msb_ofBool (b : Bool) : (ofBool b).msb = b := by
cases b <;> simp [BitVec.msb]
/-! ### msb -/
@[simp] theorem msb_zero : (0#w).msb = false := by simp [BitVec.msb, getMsbD]