feat: BitVec.{toInt, toFin, msb}_udiv

[alexkeizer]

This PR adds a toFin and msb lemma for unsigned bitvector division. We don't have toInt_udiv, since the only truly general statement we can make does no better than unfolding the definition, and it's not uncontroversially clear how to unfold toInt (see toInt_eq_msb_cond/toInt_eq_toNat_cond/toInt_eq_toNat_bmod for a few options currently provided). Instead, we do have toInt_udiv_of_msb that's able to provide a more meaningful rewrite given an extra side-condition (that x.msb = false).

This PR also upstreams a minor Nat theorem (Nat.div_le_div_left) needed for the above from Mathlib.

[tobiasgrosser]

Suggested change

	theorem msb_udiv (x y : BitVec w) :
	(x / y).msb = (x.msb && y == 1#w) := by
	theorem msb_udiv {x y : BitVec w} :
	(x / y).msb = (x.msb && y == 1#w) := by

[alexkeizer]

I'm curious what rule people use to determine whether variable should be explicit or implicit; I think we do this pretty inconsistently in the file at the moment.

For me, I try to make variables implicit only if they can be inferred from the other hypotheses, not including the lhs of an equality or bi-implication, but make sure that any explicit variables that can be inferred from the lhs come at the end of the argument list. Hence, x and y here are explicit.

[kim-em]

I agree it is ambiguous, and inconsistent.

Note, however, that at least for a bi-implication the standard (at least, as enforced by a linter in Batteries) is that variables appearing on both sides of a bi-implication should be implicit.

I tend to follow (erratically!) the same rule for equalities, too.

Let's not get hung up on this for now.

[leanprover-community-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 1b15a0f27cfdedfc81470b1720f1d603417192e7 --onto a8a160b09147c3225150703ac727eea6ee9a3b0e. (2024-12-16 15:24:36)
• 💥 Mathlib branch lean-pr-testing-6402 build failed against this PR. (2025-01-09 15:41:45) View Log
• 💥 Mathlib branch lean-pr-testing-6402 build failed against this PR. (2025-01-10 02:39:20) View Log

[alexkeizer]

Mathlib CI status (docs):

* ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the `nightly-with-mathlib` branch. Try `git rebase 1b15a0f27cfdedfc81470b1720f1d603417192e7 --onto a8a160b09147c3225150703ac727eea6ee9a3b0e`. (2024-12-16 15:24:36)

I tried to rebase on the suggested hash, but this fails because I've modified a file that didn't yet exist in that version. I could resolve the conflict, but that seems like it might cause annoying merge conflicts later down the line.

Regardless, I've upstreamed a Nat lemma (Nat.div_le_div_left), so Mathlib will break, but I've upstreamed the statement as-is, so the fix should be as easy as removing the Mathlib version of the lemma

[alexkeizer]

This should now be ready for review, but since I'm on holidays I'll keep it as a draft until I'm back and can respond to reviews timely. Hopefully by then nightly-with-mathlib will have caught up, and I can rebase on it without trouble.

[alexkeizer]

awaiting-review

I just rebased on nightly-with-mathlib also

[alexkeizer]

changelog-library

[kim-em]

Hm, that's said, the CI step checking labels didn't get triggered automatically. :-(