feat: add BitVec.[toInt_inj|toInt_ne]

[tobiasgrosser]

No description provided.

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• ❗ Std/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase e0c1afd12d4fc6b0e520774959aed06bf122aba9 --onto e362b50fa95d6823e59dd706803a93c25e888535. (2024-05-06 08:41:28)
• ❗ Std/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase e0c1afd12d4fc6b0e520774959aed06bf122aba9 --onto 883a3e752d78cf0d30628817379a6001252b5595. (2024-05-08 00:12:27)

[tobiasgrosser]

I addressed all comments. This now leads to an inconsistency with:

@[bv_toNat] theorem toNat_eq (x y : BitVec n) : x = y ↔ x.toNat = y.toNat :=
  Iff.intro (congrArg BitVec.toNat) eq_of_toNat_eq

@[bv_toNat] theorem toNat_ne (x y : BitVec n) : x ≠ y ↔ x.toNat ≠ y.toNat := by
  rw [Ne, toNat_eq]

would you like me to write a follow-up PR to address this inconsistency?

[semorrison]

I addressed all comments. This now leads to an inconsistency with:

@[bv_toNat] theorem toNat_eq (x y : BitVec n) : x = y ↔ x.toNat = y.toNat :=
  Iff.intro (congrArg BitVec.toNat) eq_of_toNat_eq

@[bv_toNat] theorem toNat_ne (x y : BitVec n) : x ≠ y ↔ x.toNat ≠ y.toNat := by
  rw [Ne, toNat_eq]

would you like me to write a follow-up PR to address this inconsistency?

Oops, thanks for noticing that! Yes, such a PR would be great.