feat: BitVec.eq_of_getElem_eq

[tobiasgrosser]

No description provided.

[ghost]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase a47c590a914e5ed564d07e8ec303c77b81f51c5c --onto 9ce15fb0c61e3a1bee17fd81647ed4d02b4f6c6d. (2024-08-30 06:10:07)

[TwoFX]

I think the preferred spelling of this would be to use Nat instead of Fin to be consistent with the bits of the API added in #5200.

Suggested change

	(pred : ∀ (i : Fin w), x[i] = y[i]) : x = y := by
	(pred : ∀ (i : Nat) (_ : i < w), x[i] = y[i]) : x = y := by

See also the analogous lemma List.ext_getElem.

[tobiasgrosser]

It seems for BitVec we used historically:

theorem eq_of_getLsbD_eq {x y : BitVec w}
    (pred : ∀(i : Fin w), x.getLsbD i.val = y.getLsbD i.val) : x = y := by

theorem eq_of_getMsbD_eq {x y : BitVec w}
    (pred : ∀(i : Fin w), x.getMsbD i.val = y.getMsbD i.val) : x = y := by

I guess we should at the very least remain consistent within BitVec.

I now added both variants to this PR and ported one theorem to show the code impact. Happy to flip to Nat, but would appreciate a comment why this is preferable over Fin.

[kim-em]

I don't think it's a good idea to prove theorems about zeroExtend without having proved the corresponding theorems about zeroExtend' first.

[kim-em]

This should use separate i : Nat and h : i < w arguments, otherwise it's only applicable for getElem of the coercion of a Fin.

[kim-em]

@tobiasgrosser, e.g. my first steps here would be #5247.

[tobiasgrosser]

This was resolved in #5247.