-
Notifications
You must be signed in to change notification settings - Fork 580
feat: bv_decide support for simple pattern matching on enum inductives #7329
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.
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
Merged
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Mathlib CI status (docs):
|
31c4eac
to
b8be79a
Compare
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Labels
changelog-language
Language features, tactics, and metaprograms
toolchain-available
A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
2E50
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This PR adds support to bv_decide for simple pattern matching on enum inductives. By simple we mean non dependent match statements with all arms written out.
This PR enables use cases such as:
There is an important thing to consider in this implementation. As the enums pass can now deal with control flow there is a tension between the structures and enums pass at play:
cond
chains. This in turn can be used by the structures pass to float projections into control
flow which might be necessary.
need to handle. For example a structure might contain a field that contains a fact about
some enum. This fact needs to be processed properly by the enums pass
To resolve this tension we do the following:
enums pass as described above. This comes down to adding a few more lemmas to a simp
invocation that is going to happen in the enums pass anyway and should thus be cheap.