From 32a9392a11773fceeaf540dc5a682e08191cd191 Mon Sep 17 00:00:00 2001 From: Luisa Cicolini <48860705+luisacicolini@users.noreply.github.com> Date: Mon, 24 Feb 2025 17:02:51 +0000 Subject: [PATCH] feat: add `BitVec.toFin_abs` (#7206) This PR adds theorem `BitVec.toFin_abs`, completing the API for `BitVec.*_abs`. --------- Co-authored-by: Tobias Grosser --- src/Init/Data/BitVec/Lemmas.lean | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index d0384606a4..931797edd3 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -4217,6 +4217,10 @@ theorem toInt_abs_eq_natAbs_of_ne_intMin {x : BitVec w} (hx : x ≠ intMin w) : x.abs.toInt = x.toInt.natAbs := by simp [toInt_abs_eq_natAbs, hx] +theorem toFin_abs {x : BitVec w} : + x.abs.toFin = if x.msb then Fin.ofNat' (2 ^ w) (2 ^ w - x.toNat) else x.toFin := by + by_cases h : x.msb <;> simp [BitVec.abs, h] + /-! ### Reverse -/ theorem getLsbD_reverse {i : Nat} {x : BitVec w} :