feat: add BitVec.getElem_[add|add_add_bool|mul|rotateLeft|rotateRight…

[tobiasgrosser]

…|twoPow|one|replicate]

... and mark getElem_setWidth as @[simp].

getElem_rotateLeft and getElem_rotateRight have a non-trivial rhs but we follow getLsbD_[rotateLeft|rotateRight]for consistency.

[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 16a16898d5cab567152234edc877f66ad43ac39a --onto 9460f79d28d3a72d7484766b5f2c83362e91dd5b. (2024-09-28 10:54:41)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 5605e0198a0bd848bffc82cab19bf2e9bcab60db --onto 9460f79d28d3a72d7484766b5f2c83362e91dd5b. (2024-09-28 12:08:24)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 5605e0198a0bd848bffc82cab19bf2e9bcab60db --onto 994cfa4c74a066df050ca889da912e71fa70cd85. (2024-09-30 04:35:41)

[tobiasgrosser]

@kim-em, I just tried this for getElem_rotateRight, but I seem unable to access the condition of the if-condition from omega:

@[simp]
theorem getElem_rotateLeft {x : BitVec w} {r i : Nat} (h : i < w) :
    (x.rotateLeft r)[i] =
      if (i < r % w) then
      (x[(w - (r % w) + i)]'(by /- I do not get `i < r % w` here -/ sorry)) else
      (x[i - (r % w)]'(by omega)) := by
  simp [← BitVec.getLsbD_eq_getElem, h]

[kim-em]

@kim-em, I just tried this for getElem_rotateRight, but I seem unable to access the condition of the if-condition from omega:

@[simp]
theorem getElem_rotateLeft {x : BitVec w} {r i : Nat} (h : i < w) :
    (x.rotateLeft r)[i] =
      if (i < r % w) then
      (x[(w - (r % w) + i)]'(by /- I do not get `i < r % w` here -/ sorry)) else
      (x[i - (r % w)]'(by omega)) := by
  simp [← BitVec.getLsbD_eq_getElem, h]

You need to name the condition: if h : c then t else e.

[tobiasgrosser]

@kim-em, I just tried this for getElem_rotateRight, but I seem unable to access the condition of the if-condition from omega:

@[simp]
theorem getElem_rotateLeft {x : BitVec w} {r i : Nat} (h : i < w) :
    (x.rotateLeft r)[i] =
      if (i < r % w) then
      (x[(w - (r % w) + i)]'(by /- I do not get `i < r % w` here -/ sorry)) else
      (x[i - (r % w)]'(by omega)) := by
  simp [← BitVec.getLsbD_eq_getElem, h]

You need to name the condition: if h : c then t else e.

Perfect. This was the hint I needed.

[kim-em]

Otherwise LGTM now.

[tobiasgrosser]

All comments addressed. This now looks very neat.