refactor: make BitVec indexing more consistent with List indexing

[alexkeizer]

The current BitVec.getLsb/getMsb functions index bitvectors with Nats, returning false for out-of-bounds indexes.
I propose to rename these functions to getLsbD/getMsbD (D for default value), in line with List.getD.
This frees up the getLsb /getMsb name for indexing with a guaranteed in-bounds i : Fin _, just like List.get.

Similarly, rename msb (which might index out-of-bounds for an empty bitvector) to msbD, and add a new msb taking a known non-empty bitvector (i.e., BitVec (n+1)), c.f. List.headD/List.head. And add short-hands lsb/lsbD to get the least-significant bit for symmetry.

The comparison is not perfect: List.getD allows the caller to specify a default value for out-of-bounds indices, whereas the newly added BitVec.getLsbD assumes false as the default value. An indexing function which returns true for out-of-bounds indices does not seem necessary to me, but I am curious to hear other opinions on this.

[joehendrix]

I could be persuaded otherwise, but at the moment I'm not a fan of the naming change here.

As you point out there isn't a need for a default of true and so this change just adds a bit of typing or proving work (if you want to show the index is in bounds).

[alexkeizer]

A benefit of the new getMsb (Fin-indexed) is that we don't have to check the i < w side condition that getMsb (Nat-indexed) does need, and that we can reuse the existing Fin.rev. Thus, in contexts where we know an index is in bounds, this would allow us to use a simpler definition for getMsb.
Then again, if we know the index is in bounds, then this side-condition is easily simplified away.

My original reason for adding these Fin-indexed definitions is to easily implement a BitVec w -> List Bool conversion as List.ofFn x.getMsb or List.ofFn x.getLsb, where x : BitVec w.

If that is the only good use, though, I'm more than happy to keep the old name, and just inline the Fin-indexed versions in these defs.

[linesthatinterlace]

I could be persuaded otherwise, but at the moment I'm not a fan of the naming change here.

As you point out there isn't a need for a default of true and so this change just adds a bit of typing or proving work (if you want to show the index is in bounds).

I was just made aware of this PR. From my point of view I think the Fin bounds are often very sensible, because we have a whole API on Fin itself which makes using them as indexes for stuff much more straightforward. It's not just a subtype with a proposition! Because we have functions like Fin.succ, Fin.castSucc, Fin.succAbove, there's a whole number of reasons why the natural type of bit indexes of a bitvector of length n should be Fin n. So I think the naming change emphasising this is a positive one.