feat: add BitVec.(getMSbD, msb)_replicate, replicate_append_replicate_eq and support theorems
#6326
Conversation
…nto msb-replicate
luisacicolini
changed the title
BitVec.(getMSbD, msb)_replicate and necessary theoremsBitVec.(getMSbD, msb)_replicate, replicate_append_replicate_eq and support theorems
|
@alexkeizer, can you do a round of reviews? |
github-actions
bot
added
the
toolchain-available
leanprover-community-bot
added
the
builds-mathlib
|
Mathlib CI status (docs):
|
src/Init/Data/BitVec/Lemmas.lean
Outdated
| by_cases h₀ : 0 < w | ||
| · by_cases h₁ : i < w * n <;> by_cases h₂ : n = 0 |
There was a problem hiding this comment.
I suspect the proof will be nicer if you use cases w and cases n rather than by_cases.
(cases is also morally the right thing to use, since by_cases invokes classical reasoning, which is wholly unnecessary here, but that is mostly my opinion on aesthetics that is not shared by the community as a whole)
|
thanks @alexkeizer for the review. I refactored the proof with |
| theorem getMsbD_replicate {n w : Nat} (x : BitVec w) : | ||
| (x.replicate n).getMsbD i | ||
| = (decide (i < w * n) && x.getMsbD (i % w)) := by |
There was a problem hiding this comment.
I think this would be much simpler if you introduced BitVec.reverse first, and prove this via
rw [← getLsbD_reverse, reverse_replicate, getLsbD_replicate, getLsbD_reverse]
Could you have a go at that? It should avoid all the index munging.
There was a problem hiding this comment.
thanks @kim-em! Am currently working on the reverse on a different branch to avoiding adding too much stuff here (I am trying to follow the same design strategies as List, treating the bitvec as a list of bools).
| theorem mod_sub_eq_sub_mod {w n i : Nat} (hwn : i < w * n) (hn : 0 < n) : | ||
| (w * n - 1 - i) % w = w - 1 - i % w := by |
There was a problem hiding this comment.
This proof can probably be shortened! But let's see if we can avoid it entirely.
This PR adds
BitVec.(getMsbD, msb)_replicateandreplicate_append_replicate_eqtheorems. An additional private theoremmod_sub_eq_sub_modis added to provegetMsbD_replicate. The proving strategy basically reducesgetMsbDtogetLsbDand tackles each case separately.Co-authored with @bollu.