Skip to content

Commit

Permalink
feat: add _self, _zero, and _allOnes for BitVec.[and|or|xor]
Browse files Browse the repository at this point in the history
The `xor_allOnes` theorems end up in the `not` section, as the
relevant simplification lemmas are otherwise not defined.
  • Loading branch information
tobiasgrosser committed Sep 21, 2024
1 parent a6830f9 commit 042cd6c
Showing 1 changed file with 60 additions and 0 deletions.
60 changes: 60 additions & 0 deletions src/Init/Data/BitVec/Lemmas.lean
Original file line number Diff line number Diff line change
@@ -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 [Bool.or_self]

@[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 [Bool.and_self]

@[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 [Bool.xor_self]

@[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

0 comments on commit 042cd6c

Please sign in to comment.