From af8ec410146bc49872c63d726bc585e4a731143d Mon Sep 17 00:00:00 2001 From: Siddharth Date: Mon, 10 Mar 2025 19:16:25 +0000 Subject: [PATCH] feat: BitVec.extractLsb'_eq_self (#7426) This PR adds the Bitwuzla rewrite rule [`BV_EXTRACT_FULL`](https://github.com/bitwuzla/bitwuzla/blob/6a1a768987cca77f36ebfe06f3a786348a481bbd/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 ``` --- src/Init/Data/BitVec/Lemmas.lean | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index 24d5e5c6de..699fa8b22d 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -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