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.ofFn and lemmas #1078

Open
wants to merge 22 commits into
base: main
Choose a base branch
from
Open

feat: add BitVec.ofFn and lemmas #1078

wants to merge 22 commits into from

Conversation

fgdorais
Copy link
Collaborator

@fgdorais fgdorais commented Dec 23, 2024 •
edited by kim-em
Loading

@fgdorais fgdorais added the awaiting-review This PR is ready for review; the author thinks it is ready to be merged. label Dec 23, 2024
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Dec 23, 2024
@leanprover-community-mathlib4-bot
Update Batteries branch for testing leanprover-community/batteries#1078
3017df3
@leanprover-community-bot
Copy link
Collaborator

Mathlib CI status (docs):

kim-em
kim-em reviewed Jan 5, 2025
View reviewed changes
Batteries/Data/BitVec.lean Outdated Show resolved Hide resolved
kim-em
kim-em reviewed Jan 5, 2025
View reviewed changes
Batteries/Data/BitVec.lean Outdated Show resolved Hide resolved
kim-em
kim-em reviewed Jan 5, 2025
View reviewed changes
Batteries/Data/BitVec.lean Outdated Show resolved Hide resolved
@kim-em
Copy link
Collaborator

kim-em commented Jan 8, 2025

This seems to have grown into two separate PRs smushed together?

@fgdorais
Copy link
Collaborator Author

fgdorais commented Jan 9, 2025

Yes, I was working on the split earlier today. I will push the prequel PR soon. I'm also inclined to drop the toInt for now. There's a lot of technical issues that I keep bumping into and I can't seem to find reasonable pathways to link all the necessary endpoints.

@fgdorais fgdorais mentioned this pull request Jan 9, 2025
Merged
@fgdorais fgdorais added depends on another PR This is stacked on top of another Batteries PR. and removed awaiting-review This PR is ready for review; the author thinks it is ready to be merged. labels Jan 9, 2025
@fgdorais
Copy link
Collaborator Author

fgdorais commented Jan 9, 2025

Split completed, Int part postponed to another PR.

kim-em
kim-em reviewed Jan 10, 2025
View reviewed changes
Batteries/Data/BitVec.lean Outdated Show resolved Hide resolved
@fgdorais fgdorais added awaiting-review This PR is ready for review; the author thinks it is ready to be merged. and removed depends on another PR This is stacked on top of another Batteries PR. labels Jan 15, 2025
hargoniX
hargoniX reviewed Jan 19, 2025
View reviewed changes
Batteries/Data/BitVec/Basic.lean
namespace BitVec

/-- `ofFnLEAux f` returns the `BitVec m` whose `i`th bit is `f i` when `i < m`, little endian. -/
@[inline] def ofFnLEAux (m : Nat) (f : Fin n → Bool) : BitVec m :=
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm not quite sure whether we want to have these functions in general. There is no chance that bv_decide can ever support this kind of BitVec as it would require reasoning about a function Fin n -> Bool which it cannot do. Whether this is an inclusion/exclusion criterium for BitVec stuff I don't know.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm using these for linear algebra over the 2-element field, so this is not completely related to bv_decide.

Batteries/Data/BitVec/Lemmas.lean Show resolved Hide resolved
Batteries/Data/BitVec/Lemmas.lean Show resolved Hide resolved
@fgdorais fgdorais added the depends on another PR This is stacked on top of another Batteries PR. label Jan 20, 2025
@kim-em kim-em added awaiting-author Waiting for PR author to address issues and removed awaiting-review This PR is ready for review; the author thinks it is ready to be merged. depends on another PR This is stacked on top of another Batteries PR. labels Jan 30, 2025
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the merge-conflict This PR has merge conflicts with the `main` branch which must be resolved by the author. label Jan 30, 2025
@fgdorais fgdorais mentioned this pull request Jan 30, 2025
Merged
github-merge-queue bot pushed a commit to leanprover/lean4 that referenced this pull request Jan 31, 2025
@fgdorais @bollu
feat: add BitVec lemmas about msb and shiftConcat (#6875)
9b5813e 
This PR adds a lemma relating `msb` and `getMsbD`, and three lemmas
regarding `getElem` and `shiftConcat`. These lemmas were needed in
[Batteries#1078](leanprover-community/batteries#1078)
and the request to upstream was made in the review of that PR.

---------

Co-authored-by: Siddharth <[email protected]>
@fgdorais fgdorais added awaiting-review This PR is ready for review; the author thinks it is ready to be merged. and removed awaiting-author Waiting for PR author to address issues merge-conflict This PR has merge conflicts with the `main` branch which must be resolved by the author. labels Jan 31, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@hargoniX hargoniX hargoniX left review comments

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

Assignees
No one assigned
Labels
awaiting-review This PR is ready for review; the author thinks it is ready to be merged. builds-mathlib
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
5 participants
@fgdorais @leanprover-community-bot @kim-em @hargoniX @leanprover-community-mathlib4-bot