feat: add Bitvec reverse definition, getLsbD_reverse, getMsbD_reverse, reverse_append, reverse_replicate and Nat.mod_sub_eq_sub_mod

[luisacicolini]

This PR defines reverse for bitvectors and implements a first subset of theorems (getLsbD_reverse, getMsbD_reverse, reverse_append, reverse_replicate) and an additional theorem necessary for one of the proofs (Nat.mod_sub_eq_sub_mod).

The main objective is to simplify the proofs in #6326. I sadly could not find a way to avoid adding Nat.mod_sub_eq_sub_mod, any suggestion in this direction would be greatly helpful.

[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 9b28c5879a77f9f0212a7f39ea83f56c71abda42 --onto 2c87905d77b707c3283c1de759fd63269ac386a1. (2024-12-31 15:59:57)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 9d622270a16070d4a7a21f058c1a9ad91dce65e2 --onto 8d9d81453bd28aa9799e6bf2ad52def1d75549cb. (2025-01-02 22:56:45)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 9d622270a16070d4a7a21f058c1a9ad91dce65e2 --onto 78ddee911287bf7b0069a695b01001db2654a765. (2025-01-06 21:26:29)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 9d622270a16070d4a7a21f058c1a9ad91dce65e2 --onto 00ef231a6e03398c2ad3b577ab036f901ec88543. (2025-01-08 16:15:45)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 9d622270a16070d4a7a21f058c1a9ad91dce65e2 --onto d2c4471cfa4611977bf4927b5cd849df1a4272b7. (2025-01-12 08:13:01)

[kim-em]

@luisacicolini, please add the changelog-library label to the PR. You can do this by writing the label name in a comment. (I'm faster to look at PRs that have a green tick!)

[luisacicolini]

Thanks a lot @kim-em :)
While at it, I also added a replicate_append lemma. All sorrys should be clear now!

[luisacicolini]

changelog-library

[kim-em]

I suspect, but won't ask for this PR, that proving things about replicate would actually get easier by generalizing, i.e. defining a BitVec.flattenList' : (L : List (\Sigma n, BitVec n)) -> BitVec (L.map fst).sum and then a BitVec.flattenList : (L : List (BitVec n)) -> BitVec (L.length * n), and finally defining BitVec.replicate x n := BitVec.flattenList (List.replicate x n) and deriving all facts from facts about the more general operations.

[kim-em]

Thanks a lot @kim-em :) While at it, I also added a replicate_append lemma. All sorrys should be clear now!

And please remember to comment awaiting-review, as if the awaiting-author label is still present I might not remember to look!

[luisacicolini]

Had to add an extra cons_append_append lemma to fix all the casts, but proof eventually went through.

[luisacicolini]

awaiting-review

[kim-em]

I'm sorry to keep asking for more and more changes here, but I think there's opportunity to fill in obvious missing lemmas and get easier proofs.

Could this be by:

theorem cons_append (x : BitVec w₁) (y : BitVec w₂) (a : Bool) :
    (cons a x) ++ y = (cons a (x ++ y)).cast (by omega) := by
  apply eq_of_toNat_eq
  simp only [toNat_append, toNat_cons, toNat_cast]
  rw [Nat.shiftLeft_add, Nat.shiftLeft_or_distrib]

The lemma Nat.shiftLeft_or_distrib is missing and would need to be written.

[kim-em]

The idea here is that switching to Nat as soon as possible means you don't need to handle all in index inequalities. It's great that omega can solve them, but hopefully we can just avoid them to begin with.

[luisacicolini]

Thanks for the advice @kim-em :) I'm working on the proof of Nat.shiftLeft_or_distrib but it seems to me like the best way to prove it is to add shiftLeft_bitwise_distrib, bitwise_mul_two_pow, and potentially a few more theorems (basically do what the proof of shiftRight_and_distrib does). If this sounds sensible I'm happy to add the necessary theorems, but maybe it's better to do it in another PR, since this is quite big already?

[luisacicolini]

Currently working here on this to avoid having a massive PR!

[luisacicolini]

now in #6630 :)

[kim-em]

Suggested change

	(x₁ ++ x₂)++ x₃ = (x₁ ++ (x₂ ++ x₃)).cast (by omega) := by
	(x₁ ++ x₂) ++ x₃ = (x₁ ++ (x₂ ++ x₃)).cast (by omega) := by