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

feat: add _self, _zero, and _allOnes for BitVec.[and|or|xor] (#5413)

Browse source 
The `xor_allOnes` theorems end up in the `not` section, as the relevant
simplification lemmas are otherwise not defined.
This commit is contained in:
Tobias Grosser 2024-09-22 11:10:54 +01:00 • committed by GitHub
parent a6830f90ab
commit fc52015841
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 60 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -710,6 +710,26 @@ theorem or_comm (x y : BitVec w) :
simp [Bool.or_comm]
instance : Std.Commutative (fun (x y : BitVec w) => x ||| y) := ⟨BitVec.or_comm⟩
@[simp] theorem or_self {x : BitVec w} : x ||| x = x := by
ext i
simp
@[simp] theorem or_zero {x : BitVec w} : x ||| 0#w = x := by
ext i
simp
@[simp] theorem zero_or {x : BitVec w} : 0#w ||| x = x := by
ext i
simp
@[simp] theorem or_allOnes {x : BitVec w} : x ||| allOnes w = allOnes w := by
ext i
simp
@[simp] theorem allOnes_or {x : BitVec w} : allOnes w ||| x = allOnes w := by
ext i
simp
/-! ### and -/
@[simp] theorem toNat_and (x y : BitVec v) :
@ -751,6 +771,26 @@ theorem and_comm (x y : BitVec w) :
simp [Bool.and_comm]
instance : Std.Commutative (fun (x y : BitVec w) => x &&& y) := ⟨BitVec.and_comm⟩
@[simp] theorem and_self {x : BitVec w} : x &&& x = x := by
ext i
simp
@[simp] theorem and_zero {x : BitVec w} : x &&& 0#w = 0#w := by
ext i
simp
@[simp] theorem zero_and {x : BitVec w} : 0#w &&& x = 0#w := by
ext i
simp
@[simp] theorem and_allOnes {x : BitVec w} : x &&& allOnes w = x := by
ext i
simp
@[simp] theorem allOnes_and {x : BitVec w} : allOnes w &&& x = x := by
ext i
simp
/-! ### xor -/
@[simp] theorem toNat_xor (x y : BitVec v) :
@ -795,6 +835,18 @@ theorem xor_comm (x y : BitVec w) :
simp [Bool.xor_comm]
instance : Std.Commutative (fun (x y : BitVec w) => x ^^^ y) := ⟨BitVec.xor_comm⟩
@[simp] theorem xor_self {x : BitVec w} : x ^^^ x = 0#w := by
ext i
simp
@[simp] theorem xor_zero {x : BitVec w} : x ^^^ 0#w = x := by
ext i
simp
@[simp] theorem zero_xor {x : BitVec w} : 0#w ^^^ x = x := by
ext i
simp
/-! ### not -/
theorem not_def {x : BitVec v} : ~~~x = allOnes v ^^^ x := rfl
@ -843,6 +895,14 @@ theorem not_def {x : BitVec v} : ~~~x = allOnes v ^^^ x := rfl
ext
simp
@[simp] theorem xor_allOnes {x : BitVec w} : x ^^^ allOnes w = ~~~ x := by
ext i
simp
@[simp] theorem allOnes_xor {x : BitVec w} : allOnes w ^^^ x = ~~~ x := by
ext i
simp
/-! ### cast -/
@[simp] theorem not_cast {x : BitVec w} (h : w = w') : ~~~(cast h x) = cast h (~~~x) := by