feat: add Bitvec.ofInt_ofNat

[tobiasgrosser]

We use no_index to work around special-handling of OfNat.ofNat in DiscrTree, which has been reported as an issue in #2867 and is currently in the process of being fixed in #3684. As the potential fix seems non-trivial and might need some time to arrive in-tree, we meanwhile add the no_index keyword to the problematic subterm.

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• ❗ Batteries CI can not be attempted yet, as the nightly-testing-2024-08-17 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Batteries CI should run now. (2024-08-18 07:18:25)

[tobiasgrosser]

I am currently debugging why no_index is needed.

[tobiasgrosser]

I have two versions: one fails, and the other one works. Advice on what is going on would be appreciated. I would be OK with the no_index version but would prefer to add one sentence explaining why it is needed.

@[simp] theorem ofInt_ofNat (w n : Nat) :
    BitVec.ofInt w (no_index (OfNat.ofNat n)) = BitVec.ofNat w n :=
  rfl

@[simp] theorem ofInt_ofNat_no_noindex (w n : Nat) :
    BitVec.ofInt w (OfNat.ofNat n) = BitVec.ofNat w n :=
  rfl

example : BitVec.ofInt w 1 = 1#w + 0#w := by
  simp only [ofInt_ofNat] -- this one works
  simp only [BitVec.add_zero]

example : BitVec.ofInt w 1 = 1#w + 0#w := by
  simp only [ofInt_ofNat_no_noindex] -- this one fails
  simp only [BitVec.add_zero]

Corresponding zulip discussion: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/no_index.20required.20on.20ofNat.20instance/near/463300187

[tobiasgrosser]

@urkud kindly provide the relevant context to understand the no_index issue in the zulip thread. I am now convinced that no_index is needed at the moment and put the relevant information into the PR summary at the top. This PR is now ready to review.

[tobiasgrosser]

awaiting-review