feat: toInt_abs

[bollu]

We implement toInt_abs. A subtle wrinkle is to note that abs (intMin w) = intMin w, which complicates our proof.

Furthermore, toward this proof, we add an alternative to msb_eq_decide which is written purely in terms of 2^w, instead of 2^(w - 1). This reduces the impedance mismatch with toInt_eq_toNat_cond:

theorem toInt_eq_toNat_cond (x : BitVec n) :
    x.toInt =
      if 2*x.toNat < 2^n then
        (x.toNat : Int)
      else
        (x.toNat : Int) - (2^n : Nat)

which makes many of the proofs much easier.

Additionally, we add definitions for toInt_intMin that express the value in terms of an if-then-else (to handle the case where w = 0, instead of the expression -2^w % 2^(w - 1), which, while mathematically sound, is a pain to reason with.

Finally, we add two other lemmas, toInt_bounds_of_msb_eq_{true, false} which prove the bounds of x.toInt when x is positive (resp. negative). This is useful to coax omega into proving the impossibility of certain cases when working with toInt.

---

I'm not really sure what the best API design is here, and how I should split the API up, so advice is much appreciated

[tobiasgrosser]

Also, do not drop toNat_abs entirely.

[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 76164b284b0769672d8a643c4396356a6f053fba --onto 66dbad911eaaec4cd512662bd5cc67a2a16d2484. (2024-10-23 20:43:57)

[kim-em]

@bollu, I updated the PR title to include BitVec: it's important these are understandable without context.