feat: proposed change to BitVec API

[kim-em]

This renames BitVec.getLsb to getLsbD (D for "default" value, i.e. false), and introduces getLsb? and getLsb' (which we can rename to getLsb after a deprecation cycle).

(Similarly for getMsb.)

Also adds a GetElem class so we can use x[i] and x[i]? notation.

Later, we will turn

theorem getLsbD_eq_getElem?_getD (x : BitVec w) (i : Nat) (h : i < w) :
    x.getLsbD i = x[i]?.getD false

on as a @[simp] lemma.

This PR doesn't attempt to demonstrate the benefits, but I think both arguments are going to get easier, and this will bring the BitVec API closer in line to List/Array, etc.

[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 44985dc9a64bb6f4f898abb7be24e7be47f42bb7 --onto 9ce15fb0c61e3a1bee17fd81647ed4d02b4f6c6d. (2024-08-29 06:37:58)
• ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2024-08-29 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. (2024-08-30 01:58:41)

[alexkeizer]

I like the getLsb -> getLsbD rename (in fact, I've proposed this exact change before, back when bitvectors were still in now-batteries/then-std4)

[alexkeizer]

I think it might make sense to bundle the proof, and have this take an i : Fin w, akin to how List.get does it.
IIRC, there are some places we currently have getLsb i with i : Fin w (relying on the Fin to Nat coercion). If we bundle the proof in a single Fin argument, these call sites will just magically keep working

[kim-em]

Agreed.