feat: WF.GuessLex: If there is only one plausible measure, use it #2954
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
these are compagnions to `MatcherApp.addArg` and `CasesOnApp.addArg` when one only has a type to transform, but not a concrete values. Prerequisite for guessing lexicographic order (#2874)
it avoids some unnecessary work, and gives better error message (squiggly lines under the failing recursive calls).
|
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/mathlib4
that referenced
this pull request
Nov 24, 2023
leanprover-community-mathlib4-bot
added
the
builds-mathlib
nomeata
commented
Nov 24, 2023
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/mathlib4
that referenced
this pull request
Nov 27, 2023
|
This seems straightforward and reasonable, and fixes some of the performance regressions of introducing GuessLex (#2960). Will merge right after that (but separately for bisecting and more helpful history). |
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/mathlib4
that referenced
this pull request
Nov 27, 2023
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.
If here is only one plausible measure, there is no point having the
GuessLexcode see if itis terminating, running all the tactics, only for the
MkFixcode then run the tactics again.So if there is only one plausible measure (non-mutual recursion with only one varying
parameter), just use that measure.
Side benefit: If the function isn’t terminating, more detailed error messages are shown
(failing proof goals), located at the recursive calls.