From 6833b6dba83f36dfdcd05ae86375e820f6d1a65f Mon Sep 17 00:00:00 2001 From: Osman Yasar Date: Mon, 16 Feb 2026 22:50:10 +0000 Subject: [PATCH] feat: add BitVec.signExtend_extractLsb_setWidth theorem (#11943) This PR introduces the theorem `BitVec.sshiftRight_eq_setWidth_extractLsb_signExtend` theorem, proving `x.sshiftRight n` is equivalent to first sign-extending `x`, extracting the appropriate least significant bits, and then setting the width back to `w`. --------- Co-authored-by: Tobias Grosser --- src/Init/Data/BitVec/Lemmas.lean | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index 7200999731..56941ece09 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -2581,6 +2581,19 @@ theorem msb_signExtend {x : BitVec w} : · simp [h, BitVec.msb, getMsbD_signExtend, show v - w = 0 by omega] · simp [h, BitVec.msb, getMsbD_signExtend, show ¬ (v - w = 0) by omega] +/-- Sign-extending to `w + n` bits, extracting bits `[w - 1 + n..n]`, and setting width +back to `w` is equivalent to arithmetic right shift by `n`, since both sides discard the `n` +least significant bits and replicate the sign bit into the upper bits. -/ +@[simp] +theorem signExtend_extractLsb_setWidth {x : BitVec w} {n : Nat} : + ((x.signExtend (w + n)).extractLsb (w - 1 + n) n).setWidth w = x.sshiftRight n := by + ext i hi + simp only [getElem_sshiftRight, getElem_setWidth, getLsbD_extract, + Nat.add_sub_cancel, show i ≤ w - 1 by omega, decide_true, getLsbD_signExtend, + Bool.true_and] + by_cases hni : n + i < w + <;> (simp [hni]; omega) + /-- Sign extending to a width smaller than the starting width is a truncation. -/ theorem signExtend_eq_setWidth_of_le (x : BitVec w) {v : Nat} (hv : v ≤ w) : x.signExtend v = x.setWidth v := by