feat: add BitVec.getElem_truncate

[tobiasgrosser]

No description provided.

[tobiasgrosser]

@semorrison, we modelled this PR after #5247, but I am a bit confused that we would not have getElem on the RHS of these identities. Could you briefly explain why the RHS has getLsbD?

[leanprover-community-bot]

Mathlib CI status (docs):

• ✅ Mathlib branch lean-pr-testing-5278 has successfully built against this PR. (2024-09-07 07:50:36) View Log

[tobiasgrosser]

I chatted with @alexkeizer, and his suggestion was to add:

theorem getLsbD_eq_getElem {x : BitVec w} {i : Nat} (h : i < w) :
    x.getLsbD i = x[i] := by
  simp [getLsbD, getElem_eq_testBit_toNat]

to get back to getElem after these rewrites to getLsbD, if the relevant hypothesis is flying around. Does this make sense from your perspective?

[leanprover-community-bot]

Mathlib CI status (docs):

• ✅ Mathlib branch lean-pr-testing-5278 has successfully built against this PR. (2024-09-10 06:48:19) View Log

[kim-em]

I chatted with @alexkeizer, and his suggestion was to add:

theorem getLsbD_eq_getElem {x : BitVec w} {i : Nat} (h : i < w) :
    x.getLsbD i = x[i] := by
  simp [getLsbD, getElem_eq_testBit_toNat]

to get back to getElem after these rewrites to getLsbD, if the relevant hypothesis is flying around. Does this make sense from your perspective?

Yes, this looks good. I think it can even be a simp lemma.

[kim-em]

Apologies for the delay reviewing here.

[tobiasgrosser]

@semorrison, I applied your suggestions. However, I am not use we want to implement them without adding a new hypothesis h : i < n. @alexkeizer's suggestion of introducing getLsbD_eq_getElem was precisely to have the other theorems to be able to have a weaker precondition and a weaker RHS, but allowing for an automatic translation to getElem, whenever a stronger precondition is available.

getLsbD_eq_getElem is not yet @[simp] as this will break the build without a flashed out getElem API. So I will enable it only after the API is complete.

[tobiasgrosser]

awaiting-review

[tobiasgrosser]

I moved this back to getLsbD on the RHS. @semorrison, feel invited to merge.

[leanprover-community-bot]

Mathlib CI status (docs):

• 🟡 Mathlib branch lean-pr-testing-5278 build against this PR was cancelled. (2024-09-16 06:01:21) View Log

[leanprover-community-bot]

Mathlib CI status (docs):

• 🟡 Mathlib branch lean-pr-testing-5278 build against this PR was cancelled. (2024-09-16 06:43:22) View Log

[leanprover-community-bot]

Mathlib CI status (docs):

• ✅ Mathlib branch lean-pr-testing-5278 has successfully built against this PR. (2024-09-16 07:36:11) View Log

[leanprover-community-bot]

Mathlib CI status (docs):

• ✅ Mathlib branch lean-pr-testing-5278 has successfully built against this PR. (2024-09-16 09:59:48) View Log