feat: decide +revert and improvements to native_decide
#5999
Conversation
This file contains 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
This PR adds configuration options for `decide`/`decide!`/`native_decide` and refactors them to be frontends to the same tactic. Adds a `+revert` option that cleans up the local context and reverts all local variables the goal depends on, along with indirect propositional hypotheses. Makes `native_decide` fail at elaboration time on failure without sacrificing performance (the decision procedure is still evaluated just once).
nomeata
reviewed
Nov 7, 2024
| structure DecideConfig where | ||
| /-- If true (default: false), then use only kernel reduction when reducing the `Decidable` instance. | ||
| This is more efficient, since the default mode reduces twice (once in the elaborator and again in the kernel), | ||
| however kernel reduction ignores transparency settings. The `decide!` tactic is a synonym for `decide +kernel`. -/ |
There was a problem hiding this comment.
Maybe decide! is young enough that we can remove it in favor of the more explicit, but still convenient, decide +kernel syntax? Or is decide! fundamental enough that it deserves the short form/
There was a problem hiding this comment.
That makes sense deprecating decide!, since ! is not really evocative of doing kernel reduction. I'll leave that for a future PR.
There was a problem hiding this comment.
Sure. But still before the next stable release?
github-actions
bot
added
the
toolchain-available
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/batteries
that referenced
this pull request
Nov 7, 2024
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/mathlib4
that referenced
this pull request
Nov 7, 2024
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/batteries
that referenced
this pull request
Nov 7, 2024
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/mathlib4
that referenced
this pull request
Nov 7, 2024
leanprover-community-bot
added
the
builds-mathlib
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/batteries
that referenced
this pull request
Nov 8, 2024
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/mathlib4
that referenced
this pull request
Nov 8, 2024
github-merge-queue
bot
removed this pull request from the merge queue due to failed status checks
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/batteries
that referenced
this pull request
Nov 8, 2024
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/mathlib4
that referenced
this pull request
Nov 8, 2024
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
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.
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 configuration options for
decide/decide!/native_decideand refactors the tactics to be frontends to the same backend. Adds a+revertoption that cleans up the local context and reverts all local variables the goal depends on, along with indirect propositional hypotheses. Makesnative_decidefail at elaboration time on failure without sacrificing performance (the decision procedure is still evaluated just once). Nownative_decidesupports universe polymorphism.Closes #2072