feat: add BitVec.(getMsbD, msb)_(extractLsb', extractLsb), getMsbD_extractLsb'_eq_getLsbD

[luisacicolini]

This PR adds theorems BitVec.(getMsbD, msb)_(extractLsb', extractLsb), getMsbD_extractLsb'_eq_getLsbD.

[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 56733b953eee491cbd1a95018bdb6a76506f5e61 --onto 69a73a18fbfa1fc045bfbf1c4cf93b155d4c9387. (2025-01-27 12:27:39)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 56733b953eee491cbd1a95018bdb6a76506f5e61 --onto 20c616503abe5ce4253c56dbcd7766a91c675ba0. (2025-01-29 13:33:45)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 56733b953eee491cbd1a95018bdb6a76506f5e61 --onto e922edfc218090ab2e54092336c67fe3b970dfc2. (2025-01-30 20:26:30)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 56733b953eee491cbd1a95018bdb6a76506f5e61 --onto d68c2ce28bc11ec0271a97aa7a7316905f15a484. (2025-02-03 09:05:10)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 56733b953eee491cbd1a95018bdb6a76506f5e61 --onto 832d7c500d709deb5e7f0a5a6fd0f01865d1a303. (2025-02-03 10:25:47)

[luisacicolini]

changelog-library

[bollu]

Thanks for the API :) I request a couple of minor syntactic changes, and one simplification of a theorem statement.

[alexkeizer]

Some style comments

[luisacicolini]

awaiting-review

[luisacicolini]

I've now changed the statements to remove the parenthesization in getMsbD_extractLsb. As far as I could see, that yielded an additional condition and caused some changes in msb_extractLsb.

[luisacicolini]

awaiting-review

[bollu]

I have the same concern about the legibility of the RHS here. I wonder if there isn't a simpler RHS?

[luisacicolini]

I am missing what makes the rhs simpler I guess. The previous version was:

= (decide (i ≤  hi - lo)
      && (decide (lo + (hi - lo - i) < w)
      && x.getMsbD (w - 1 - (lo + (hi - lo - i))))

would this be simpler? Consider that simplifying the parenthesization means introducing the hypoyhesis on lo \le hi.
The way I see it, the current RHS is simpler, as it highlights the main characteristic of the theorem, being that we can indeed extract (at least) one bit even if hi < lo. But I am very confused here.

[luisacicolini]

Happy to write the comment anyways - once we reach consensus on a sensible RHS

[kim-em]

The proof of this theorem must start with

  rw [getMsbD_eq_getLsbD]
  rw [getLsbD_extractLsb]
  rw [getLsbD_eq_getMsbD]

and then simplify the inequalities.

After those rewrites, we get

(decide (i < hi - lo + 1) &&
    (decide (hi - lo + 1 - 1 - i < hi - lo + 1) &&
      (decide (lo + (hi - lo + 1 - 1 - i) < w) && x.getMsbD (w - 1 - (lo + (hi - lo + 1 - 1 - i))))))

The second inequality is automatic and can be dropped.
In the third inequality, + 1 - 1 should be dropped.
The first inequality implies that the -i in the 3rd inequality is not truncating.
Moreover, if hi - lo is truncating, then i is 0.
Thus, given the 1st inequality, lo + (hi - lo + 1 - 1 - i) = (max hi lo) - i and so the 3rd inequality becomes (max hi lo) - i < w.
Finally, one needs to simplify w - 1 - (lo + (hi - lo + 1 - 1 - i)) using the first two inequalities. But given the above this is just w - 1 - (max (hi lo) - i).

Can you make the proof follow that argument?

(And apologies, I haven't checked this argument beyond what is written here, but even if it is not quite right hopefully you can see the method to derive the appropriate RHS.)

[kim-em]

Here's the correct proof style:

@[boolToPropSimps] theorem and_eq_decide (a b : Bool) : (a && b) = decide (a = true ∧ b = true) := by sorry
attribute [boolToPropSimps] decide_eq_true_iff

@[simp] theorem getMsbD_extractLsb {hi lo : Nat} {x : BitVec w} {i : Nat} :
    (extractLsb hi lo x).getMsbD i = 
      (decide (i < hi - lo + 1) &&
      (decide ((max hi lo) - i < w) && 
      x.getMsbD (w - 1 - ((max hi lo) - i)))) := by
  rw [getMsbD_eq_getLsbD]
  rw [getLsbD_extractLsb]
  rw [getLsbD_eq_getMsbD]
  simp only [boolToPropSimps]
  constructor
  · rintro ⟨h₁, h₂, h₃, h₄⟩ 
    have p : w - 1 - (lo + (hi - lo + 1 - 1 - i)) = w - 1 - (max hi lo - i) := by omega
    rw [p] at h₄
    simp [h₄]
    omega
  · rintro ⟨h₁, h₂, h₃⟩ 
    have p : w - 1 - (lo + (hi - lo + 1 - 1 - i)) = w - 1 - (max hi lo - i) := by omega
    rw [← p] at h₃ 
    rw [h₃]
    simp
    omega

Perhaps you can all take a look at this, and

• work out what we need to add to boolToPropSimps
• digest this proof style, and see where else it can be applied?

[kim-em]

(This proof style will eventually be fully automated by grind, but not quite yet. We need the full linear arithmetic module.)

[luisacicolini]

That's extremely useful @kim-em, thanks a lot! The strategy is clear now

[kim-em]

Why is

@[simp] theorem getLsbD_extractLsb (hi lo : Nat) (x : BitVec n) (i : Nat) :
    getLsbD (extractLsb hi lo x) i = (decide (i < hi - lo + 1) && x.getLsbD (lo + i)) := by
  rw [extractLsb]
  rw [getLsbD_extractLsb']

missing? It seems this is clearly logically prior to the lemmas you're adding here.