chore: name variables in Data/BitVec consistently

[tobiasgrosser]

This change canonicalizes the BitVec variable names to x y z : BitVec instead of alternative namings such as s t : BitVec or a b : BitVec. Variable names that carry semantic meaning such as (msbs : BitVec w) (lsb : Bool) remain untouched.

This is purely a naming change to make our bitvector proofs more consistent and polish the (auto-generated) documentation as a very small step towards polishing the documentation of the BitVec library in Lean.

[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 35e1554ef7c3fb01bdf1989e311cc5dcdc5b417c --onto 647a5e94925791f6a16b629b6c16ffad60a7f478. (2024-08-06 17:07:33)

[AnotherAlexHere]

This is purely a naming change to make our bitvector proofs more consistent and removes the last uses of i/j and similar simply enumerative variable names for BitVectors.

I think it may be helpful to explain the purpose of these changes and give examples.

[tobiasgrosser]

This is purely a naming change to make our bitvector proofs more consistent and removes the last uses of i/j and similar simply enumerative variable names for BitVectors.

I think it may be helpful to explain the purpose of these changes and give examples.

I updated the commit message accordingly.

[kim-em]

Thanks! Happy to merge when you mark it as ready.

[AnotherAlexHere]

Looks good!