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

chore: One sided BitVec.toNat equality lemmas (#3533)

Browse source
This commit is contained in:
Joe Hendrix 2024-02-28 16:25:40 -08:00 • committed by GitHub
parent 973cbb186b
commit 69e33efa2f
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 18 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -198,6 +198,24 @@ theorem msb_eq_getLsb_last (x : BitVec w) :
apply eq_of_toNat_eq
simp
/-- Moves one-sided left toNat equality to BitVec equality. -/
theorem toNat_eq_nat (x : BitVec w) (y : Nat)
: (x.toNat = y) ↔ (y < 2^w ∧ (x = y#w)) := by
apply Iff.intro
· intro eq
simp at eq
have lt := x.isLt
simp [eq] at lt
simp [←eq, lt, x.isLt]
· intro eq
simp [Nat.mod_eq_of_lt, eq]
/-- Moves one-sided right toNat equality to BitVec equality. -/
theorem nat_eq_toNat (x : BitVec w) (y : Nat)
: (y = x.toNat) ↔ (y < 2^w ∧ (x = y#w)) := by
rw [@eq_comm _ _ x.toNat]
apply toNat_eq_nat
@[simp] theorem getLsb_zeroExtend' (ge : m ≥ n) (x : BitVec n) (i : Nat) :
getLsb (zeroExtend' ge x) i = getLsb x i := by
simp [getLsb, toNat_zeroExtend']