feat: BitVec.(not_sshiftRight, not_sshiftRight_not, getMsb_not, msb_not)

[luisacicolini]

No description provided.

[tobiasgrosser]

LGTM

[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 9eef72620448dc267188d954514b4548d909fc52 --onto 0196bca784f82f90b4efd2a85a400daf4ab767f8. (2024-09-27 08:19:14)

[hargoniX]

This proof is a bit unstructured, the <;> simp solves one of the two goals produced by by_cases and then the ; omega only handles the last remaining goal. Usually we do these kinds of proofs like this:

@[simp] theorem not_append {x : BitVec w} {y : BitVec v} : ~~~ (x ++ y) = (~~~ x) ++ (~~~ y) := by
  ext i
  simp only [getLsbD_not, getLsbD_append, cond_eq_if]
  split
  · simp_all
  · simp_all; omega

this is important for proof stability and being able to debug quicker proofs if they ever end up breaking in some way. For example if one of the simp happens to not be powerful enough anymore omega would be thrown at potentially another goal and you'd get a message about it not being able to solve the goal + an open goal still existing etc.

[hargoniX]

Looks good apart from the small style issue!

[luisacicolini]

thanks a lot! I changed the style of the theorem to make it more similar to the one you sent, not sure it's correct style-wise

[hargoniX]

You can use just simp [h] here. simp_all is a more powerful tool. It basically goes through all hypothesis h_x and does simp [all_hyps_except h_x] at h_x until a fixpoint.

[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 9eef72620448dc267188d954514b4548d909fc52 --onto 0196bca784f82f90b4efd2a85a400daf4ab767f8. (2024-09-27 09:27:38)

[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 9eef72620448dc267188d954514b4548d909fc52 --onto 0196bca784f82f90b4efd2a85a400daf4ab767f8. (2024-09-27 09:39:44)