feat: complete BitVec.[getMsbD|getLsbD|msb] for shifts

[luisacicolini]

No description provided.

[leanprover-community-bot]

Mathlib CI status (docs):

• ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2024-10-01 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. (2024-10-03 09:04:31)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 0178f2b70df112a916efaaf8acede9ccea12b950 --onto a4fda010f3d44c02393d5afd5cf05509989daf63. (2024-10-05 21:59:30)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase ec5f206d8036b08c556eb7809a038936f838cbd0 --onto 9dac514c2fc80d3f60076314ad30a993a7b2c22f. (2024-10-07 15:45:18)

[tobiasgrosser]

Also, I feel you can have a slightly shorter title, e.g., feat: complete BitVec.[getMsbD|getLsbD|msb] for shifts

[tobiasgrosser]

I am afraid this simp is non-terminal, so you may want to turn it into a simp only. You can try to be strategic and only include the minimal set of theorems needed to get it through.

Also, do you really need a simp_all at the end?

[luisacicolini]

I am having some trouble refactoring the proofs of getMsbD_sshiftRight, getMsbD_sshiftRight' and getMsbD_ushiftRight to use simp only when non terminal. getMsbD_sshiftRight_exp and getMsbD_ushiftRight_exp are my attempts at this, which however made the proofs quite a lot longer and less elegant. I am wondering whether there are any proving strategies that I did not think about and would make these proofs better.

[bollu]

This looks fairly aggressive, and wonder if there are higher-level lemmas to be extracted here.

[tobiasgrosser]

Suggested change

	theorem getMsbD_ushiftRight {w} {x : BitVec w} {i n : Nat} :
	getMsbD (x.ushiftRight n) i = (decide (i < w) && if i < n then false else getMsbD x (i - n)) := by
	simp only [getMsbD, ushiftRight_eq, getLsbD_ushiftRight, Bool.if_false_left]
	by_cases h : i < w
	<;> by_cases h₁ : i < n
	<;> by_cases h₂ : i - n < w
	<;> simp (discharger := omega) [h, h₁, h₂]
	congr; omega
	theorem getMsbD_ushiftRight {x : BitVec w} {i n : Nat} :
	getMsbD (x.ushiftRight n) i = (decide (i < w) && if i < n then false else getMsbD x (i - n)) := by
	simp only [getMsbD, Bool.if_false_left]
	by_cases h : i < n
	· simp [getLsbD_ge, show w ≤ (n + (w - 1 - i)) by omega]
	omega
	· by_cases h₁ : i < w <;> by_cases h₂ : i - n < w
	· simp only [h, , h₁, h₂, ushiftRight_eq, getLsbD_ushiftRight]
	congr
	omega
	all_goals (simp [h, h₁, h₂]; try omega)

[tobiasgrosser]

Maybe you can refactor the other cases in similar ways?

[luisacicolini]

I changed the proof getMsbD_sshiftRight and it seems to me slightly better (if I understood correctly the rationale behind simp and simp only - CC @hargoniX). I left the two other versions as well (getMsbD_sshiftRight' and getMsbD_sshiftRight'') in case either of the two is preferrable.