feat: add BitVec.neg_neg

[tobiasgrosser]

.. as well as neg_neq_iff_neq_neg.

[tobiasgrosser]

Draft PR to indicate that @bollu or @alexkeizer should maybe double-check my style choices before Kim does his review.

[tobiasgrosser]

I am currently still unhappy with the BitVec.neg_neg proof, as the explicit use of Nat.mod_eq_of_lt is something that comes up very often also in other proofs and is always tedious to write:

theorem neg_neg {x : BitVec w} : - - x = x := by
  by_cases h : x = 0
  · simp [h]
  · simp only [toNat_eq, ofNat_eq_ofNat, toNat_ofNat, Nat.zero_mod] at h
    simp only [toNat_eq, toNat_neg]
    rw [Nat.mod_eq_of_lt (a := 2 ^ w - x.toNat) (by omega)]
    rw [Nat.mod_eq_of_lt (by omega)]
    omega

[tobiasgrosser]

I found a neat way to clean this up with two helper theorems sub_toNat_mod_cancel and sub_sub_toNat_cancel.

[leanprover-community-mathlib4-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 6dd502321f2b57a4b19c4b2a467ad900eeed8b91 --onto dd6ed124baef64a26ef5860f49597fdcef371239. (2024-08-10 06:06:43)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 6dd502321f2b57a4b19c4b2a467ad900eeed8b91 --onto 5f31e938c1bf5bb2d6d2d29b26ea932ade115357. (2024-08-11 10:02:55)

[tobiasgrosser]

This is now clean from my perspective and ready to review.