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

feat: BitVec.extractLsb'_eq_self (#7426)

Browse source 
This PR adds the Bitwuzla rewrite rule
[`BV_EXTRACT_FULL`](6a1a768987/src/rewrite/rewrites_bv.cpp (L1236-L1253)),
which is useful for the bitblaster to simplify `extractLsb'` based
expressions.

```lean
theorem extractLsb'_eq_self (x : BitVec w) : x.extractLsb' 0 w = x
```
This commit is contained in:
Siddharth 2025-03-10 19:16:25 +00:00 • committed by GitHub
parent 51794c384a
commit af8ec41014
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 5 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -1046,6 +1046,11 @@ theorem extractLsb'_eq_extractLsb {w : Nat} (x : BitVec w) (start len : Nat) (h
apply eq_of_toNat_eq
simp [extractLsb, show len - 1 + 1 = len by omega]
/-- Extracting all the bits of a bitvector is an identity operation. -/
@[simp] theorem extractLsb'_eq_self {x : BitVec w} : x.extractLsb' 0 w = x := by
apply eq_of_toNat_eq
simp [extractLsb']
/-! ### allOnes -/
@[simp] theorem toNat_allOnes : (allOnes v).toNat = 2^v - 1 := by