Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

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

Merged
merged 34 commits into from
Jan 21, 2025
Merged

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

merged 34 commits into from
Jan 21, 2025

Conversation

luisacicolini
Copy link
Contributor

@luisacicolini luisacicolini commented Dec 30, 2024 •
edited
Loading

This PR defines reverse for bitvectors and implements a first subset of theorems (getLsbD_reverse, getMsbD_reverse, reverse_append, reverse_replicate, reverse_cast, msb_reverse). We also include some necessary related theorems (cons_append, cons_append_append, append_assoc, replicate_append_self, replicate_succ') and deprecate theoremsreplicate_zero_eq and replicate_succ_eq.

@github-actions github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Dec 31, 2024
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented Dec 31, 2024 •
edited
Loading

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)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 906aa1be4b29c423a97d6909bc315fa236529a79 --onto a955708b6c5f25e7f9c9ae7b951f8f3d5aefe377. (2025-01-16 13:16:09)

alexkeizer
alexkeizer reviewed Jan 1, 2025
View reviewed changes
src/Init/Data/BitVec/Basic.lean Outdated Show resolved Hide resolved
src/Init/Data/BitVec/Basic.lean Outdated Show resolved Hide resolved
src/Init/Data/BitVec/Lemmas.lean Show resolved Hide resolved
@luisacicolini luisacicolini marked this pull request as ready for review January 3, 2025 14:27
@luisacicolini luisacicolini requested a review from kim-em as a code owner January 3, 2025 14:27
@kim-em
Copy link
Collaborator

kim-em commented Jan 8, 2025

@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
Copy link
Contributor Author

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

@luisacicolini
Copy link
Contributor Author

awaiting-review

@github-actions github-actions bot added awaiting-review Waiting for someone to review the PR and removed awaiting-author Waiting for PR author to address issues labels Jan 12, 2025
@kim-em kim-em added awaiting-author Waiting for PR author to address issues and removed awaiting-review Waiting for someone to review the PR labels Jan 12, 2025
@luisacicolini luisacicolini mentioned this pull request Jan 13, 2025
Merged
github-merge-queue bot pushed a commit that referenced this pull request Jan 16, 2025
@luisacicolini @alexkeizer
feat: add Nat.[shiftLeft_or_distrib, shiftLeft_xor_distrib`, shiftL…
906aa1b 
…eft_and_distrib`, `testBit_mul_two_pow`, `bitwise_mul_two_pow`, `shiftLeft_bitwise_distrib]` (#6630)

This PR adds theorems `Nat.[shiftLeft_or_distrib`,
shiftLeft_xor_distrib`, shiftLeft_and_distrib`, `testBit_mul_two_pow`,
`bitwise_mul_two_pow`, `shiftLeft_bitwise_distrib]`, to prove
`Nat.shiftLeft_or_distrib` by emulating the proof strategy of
`shiftRight_and_distrib`.

In particular, `Nat.shiftLeft_or_distrib` is necessary to simplify the
proofs in #6476.

---------

Co-authored-by: Alex Keizer <[email protected]>
@luisacicolini
Copy link
Contributor Author

awaiting-review

@github-actions github-actions bot added awaiting-review Waiting for someone to review the PR and removed awaiting-author Waiting for PR author to address issues labels Jan 16, 2025
@kim-em
Copy link
Collaborator

kim-em commented Jan 21, 2025

Could you update the PR description, which is out of date now? Ping me when that's done and I'll merge!

@kim-em kim-em added will-merge-soon …unless someone speaks up and removed awaiting-review Waiting for someone to review the PR labels Jan 21, 2025
@luisacicolini
Copy link
Contributor Author

Thanks @kim-em, done now!

@kim-em kim-em added this pull request to the merge queue Jan 21, 2025
Merged via the queue into leanprover:master with commit edeae18 Jan 21, 2025
22 checks passed
luisacicolini added a commit to opencompl/lean4 that referenced this pull request Jan 21, 2025
@luisacicolini @alexkeizer
feat: add Nat.[shiftLeft_or_distrib, shiftLeft_xor_distrib`, shiftL…
02baa21 
…eft_and_distrib`, `testBit_mul_two_pow`, `bitwise_mul_two_pow`, `shiftLeft_bitwise_distrib]` (leanprover#6630)

This PR adds theorems `Nat.[shiftLeft_or_distrib`,
shiftLeft_xor_distrib`, shiftLeft_and_distrib`, `testBit_mul_two_pow`,
`bitwise_mul_two_pow`, `shiftLeft_bitwise_distrib]`, to prove
`Nat.shiftLeft_or_distrib` by emulating the proof strategy of
`shiftRight_and_distrib`.

In particular, `Nat.shiftLeft_or_distrib` is necessary to simplify the
proofs in leanprover#6476.

---------

Co-authored-by: Alex Keizer <[email protected]>
luisacicolini added a commit to opencompl/lean4 that referenced this pull request Jan 21, 2025
@luisacicolini @alexkeizer @kim-em
feat: add Bitvec reverse definition, `getLsbD_reverse, getMsbD_reve…
0241e24 
…rse, reverse_append, reverse_replicate` and `Nat.mod_sub_eq_sub_mod` (leanprover#6476)

This PR defines `reverse` for bitvectors and implements a first subset
of theorems (`getLsbD_reverse, getMsbD_reverse, reverse_append,
reverse_replicate, reverse_cast, msb_reverse`). We also include some
necessary related theorems (`cons_append, cons_append_append,
append_assoc, replicate_append_self, replicate_succ'`) and deprecate
theorems`replicate_zero_eq` and `replicate_succ_eq`.

---------

Co-authored-by: Alex Keizer <[email protected]>
Co-authored-by: Kim Morrison <[email protected]>
JovanGerb pushed a commit to JovanGerb/lean4 that referenced this pull request Jan 21, 2025
@luisacicolini @alexkeizer @JovanGerb
feat: add Nat.[shiftLeft_or_distrib, shiftLeft_xor_distrib`, shiftL…
8532e1c 
…eft_and_distrib`, `testBit_mul_two_pow`, `bitwise_mul_two_pow`, `shiftLeft_bitwise_distrib]` (leanprover#6630)

This PR adds theorems `Nat.[shiftLeft_or_distrib`,
shiftLeft_xor_distrib`, shiftLeft_and_distrib`, `testBit_mul_two_pow`,
`bitwise_mul_two_pow`, `shiftLeft_bitwise_distrib]`, to prove
`Nat.shiftLeft_or_distrib` by emulating the proof strategy of
`shiftRight_and_distrib`.

In particular, `Nat.shiftLeft_or_distrib` is necessary to simplify the
proofs in leanprover#6476.

---------

Co-authored-by: Alex Keizer <[email protected]>
@luisacicolini luisacicolini mentioned this pull request Jan 21, 2025
Open
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@alexkeizer alexkeizer alexkeizer left review comments

@tobiasgrosser tobiasgrosser tobiasgrosser left review comments

@kim-em kim-em kim-em left review comments

Assignees
No one assigned
Labels
changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN will-merge-soon …unless someone speaks up
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
5 participants
@luisacicolini @leanprover-community-bot @kim-em @tobiasgrosser @alexkeizer