feat: BitVec.toNat_{add,sub,mul_of_lt} for BitVector non-overflow reasoning

[bollu]

These theorems are useful when one wants to simplify the goal state, under knowledge that the bitvector operations don't overflow. This can produce much smaller goal states that eventually allows bv_omega to quickly close the goal.

Note that the LHS of the theorem is not in simp normal form, since e.g. (x + y).toNat is normalized to (x.toNat + y.toNat) % 2^w. It's not immediately clear to me what should be done about this.

[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 a6830f90ab365e14ccb7ca31201de37f8c1e978c --onto d8e0fa425b3225fc0c35c07247ecb11b49bb00ed. (2024-09-20 17:19:33)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 5017b2bfbf3af3752db0d34dabc9d3119a352cdc --onto e551a366a0bbb27d5f853cc8e87cbd381a76ffc0. (2024-09-24 03:57:33)

[tobiasgrosser]

Hey @bollu, which part of the theorem is not in simp normal form, the LHS or the hypothesis? With respect to the hypothesis, I am curious how you turn it into toNat in the first place?

[bollu]

@tobiasgrosser updated the message to be more accurate: It's the LHS of the equality that's not in simp normal form.

[kim-em]

It's fine if the LHS of a non-simp lemma is not in simp normal form --- it just means you'll only be able to rewrite by it prior to calling simp.

I'd consider the argument that toNat_add and so on should not be simp lemmas, but this would take some work to make viable, I think.