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

feat: add BitVec.ofBool_[and|or|xor]_ofBool theorems (#5385)

Browse source 
... and use them to simplify some proofs.
This commit is contained in:
Tobias Grosser 2024-09-18 22:59:09 +01:00 • committed by GitHub
parent fa6afa85df
commit daf24ff6aa
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 39 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -234,6 +234,15 @@ theorem ofBool_eq_iff_eq : ∀ {b b' : Bool}, BitVec.ofBool b = BitVec.ofBool b'
@[simp] theorem not_ofBool : ~~~ (ofBool b) = ofBool (!b) := by cases b <;> rfl
@[simp] theorem ofBool_and_ofBool : ofBool b &&& ofBool b' = ofBool (b && b') := by
cases b <;> cases b' <;> rfl
@[simp] theorem ofBool_or_ofBool : ofBool b ||| ofBool b' = ofBool (b || b') := by
cases b <;> cases b' <;> rfl
@[simp] theorem ofBool_xor_ofBool : ofBool b ^^^ ofBool b' = ofBool (b ^^ b') := by
cases b <;> cases b' <;> rfl
@[simp, bv_toNat] theorem toNat_ofFin (x : Fin (2^n)) : (BitVec.ofFin x).toNat = x.val := rfl
@[simp] theorem toNat_ofNatLt (x : Nat) (p : x < 2^w) : (x#'p).toNat = x := rfl
@ -1421,15 +1430,18 @@ theorem eq_msb_cons_setWidth (x : BitVec (w+1)) : x = (cons x.msb (x.setWidth w)
@[simp] theorem cons_or_cons (x y : BitVec w) (a b : Bool) :
(cons a x) ||| (cons b y) = cons (a || b) (x ||| y) := by
ext i; cases i using Fin.succRecOn <;> simp <;> split <;> rfl
ext i
simp [cons]
@[simp] theorem cons_and_cons (x y : BitVec w) (a b : Bool) :
(cons a x) &&& (cons b y) = cons (a && b) (x &&& y) := by
ext i; cases i using Fin.succRecOn <;> simp <;> split <;> rfl
ext i
simp [cons]
@[simp] theorem cons_xor_cons (x y : BitVec w) (a b : Bool) :
(cons a x) ^^^ (cons b y) = cons (a ^^ b) (x ^^^ y) := by
ext i; cases i using Fin.succRecOn <;> simp <;> split <;> rfl
ext i
simp [cons]
/-! ### concat -/

24
tests/lean/interactive/completionPrv.lean.expected.out
View file

@ -46,6 +46,30 @@
"position": {"line": 9, "character": 11}},
"id": {"const": {"declName": "BitVec.getMsbD_ofBoolListBE"}}}},
{"sortText": "4",
"label": "BitVec.ofBool_and_ofBool",
"kind": 3,
"data":
{"params":
{"textDocument": {"uri": "file:///completionPrv.lean"},
"position": {"line": 9, "character": 11}},
"id": {"const": {"declName": "BitVec.ofBool_and_ofBool"}}}},
{"sortText": "5",
"label": "BitVec.ofBool_or_ofBool",
"kind": 3,
"data":
{"params":
{"textDocument": {"uri": "file:///completionPrv.lean"},
"position": {"line": 9, "character": 11}},
"id": {"const": {"declName": "BitVec.ofBool_or_ofBool"}}}},
{"sortText": "6",
"label": "BitVec.ofBool_xor_ofBool",
"kind": 3,
"data":
{"params":
{"textDocument": {"uri": "file:///completionPrv.lean"},
"position": {"line": 9, "character": 11}},
"id": {"const": {"declName": "BitVec.ofBool_xor_ofBool"}}}},
{"sortText": "7",
"label": "BitVec.ofBoolListBE",
"kind": 3,
"documentation":