feat: BitVec.toInt_abs

[bollu]

This PR implements BitVec.toInt_abs.

The absolute value of x : BitVec w is naively a case split on the sign of x. However, recall that when x = intMin w, -x = x. Thus, the full value of abs x is computed by the case split:

• If x : BitVec w is intMin, then its absolute value is also intMin w, and thus toInt will equal intMin.toInt.
• Otherwise, if x is negative, then x.abs.toInt = (-x).toInt.
• Finally, when x is nonnegative, then x.abs.toInt = x.toInt.

theorem toInt_abs {x : BitVec w} :
  x.abs.toInt =
    if x = intMin w then (intMin w).toInt
    else if x.msb then -x.toInt
    else x.toInt

We also provide a variant of toInt_abs that hides the case split for x being positive or negative by using natAbs.

theorem toInt_abs_eq_natAbs {x : BitVec w} : x.abs.toInt =
    if x = intMin w then (intMin w).toInt else x.toInt.natAbs

Supercedes https://github.com/leanprover/lean4/pull/5787

[leanprover-community-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 799b2b662825e646609963921f2c68489b2e664a --onto 72e952eadc6a171310f1d8e9d6e78acf98421494. (2024-11-21 13:01:42)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 799b2b662825e646609963921f2c68489b2e664a --onto 884a9ea2ff70bb4d0c6da4a1c23ffc26c3a974ee. (2024-11-25 14:16:57)

[tobiasgrosser]

Can you drop the mention of 'stacked pr' in the commit message?

[bollu]

@tobiasgrosser done

[bollu]

awaiting-review

[bollu]

changelog-library

[kim-em]

It doesn't need to be in this PR, but I would like to also have

theorem natAbs_toInt (x : BitVec w) : x.toInt.natAbs = if x.msb then x.toNat - (2^(w-1) - 1) else x.toNat

(didn't check the RHS carefully, but something like that ought to be true).