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

feat: add BitVec _assoc lemmas (#4299)

Browse source
This commit is contained in:
Tobias Grosser 2024-06-01 17:24:18 +01:00 • committed by GitHub
parent 0dff5701af
commit ff116dae5f
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 15 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -463,6 +463,11 @@ protected theorem extractLsb_ofNat (x n : Nat) (hi lo : Nat) :
ext
simp
theorem or_assoc (x y z : BitVec w) :
x ||| y ||| z = x ||| (y ||| z) := by
ext i
simp [Bool.or_assoc]
/-! ### and -/
@[simp] theorem toNat_and (x y : BitVec v) :
@ -489,6 +494,11 @@ protected theorem extractLsb_ofNat (x n : Nat) (hi lo : Nat) :
ext
simp
theorem and_assoc (x y z : BitVec w) :
x &&& y &&& z = x &&& (y &&& z) := by
ext i
simp [Bool.and_assoc]
/-! ### xor -/
@[simp] theorem toNat_xor (x y : BitVec v) :
@ -509,6 +519,11 @@ protected theorem extractLsb_ofNat (x n : Nat) (hi lo : Nat) :
ext
simp
theorem xor_assoc (x y z : BitVec w) :
x ^^^ y ^^^ z = x ^^^ (y ^^^ z) := by
ext i
simp [Bool.xor_assoc]
/-! ### not -/
theorem not_def {x : BitVec v} : ~~~x = allOnes v ^^^ x := rfl