fix: wildcard generalize only generalizes visible theorems
#4846
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
|
If there is a preferred way to fix this, or if this is actually the expected behaviour then let me know, happy to close the PR then. awaiting-review |
github-actions
bot
added
awaiting-review
|
Mathlib CI status (docs):
|
`generalize ... at *` sometimes will try to modify the recursive hypothesis corresponding to the current theorem being defined, which may not be the expected behaviour. It should only try to `generalize` hypotheses that it can actually modify and are visible, not implementation details. Otherwise this means that there are discrepancies between `generalize ... at *` and `generalize ... at H`, even though `H` is the only hypothesis in the context. This commit uses `getLocalHyps` instead of `getFVarIds` to get the current valid `FVarIds` in the context. This uses `isImplementationDetail` to filter out `FVarIds` that are implementation details in the context and are not visible to the user and should not be manipulated by `generalize`. Closes 4845
kim-em
force-pushed
the
wildcard-generalize
branch
from
e21c10f to
34819d8
Compare
|
@ymherklotz, apologies for my unreasonable delay here. This looks good. I've just rebase on |
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/batteries
that referenced
this pull request
Oct 25, 2024
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/mathlib4
that referenced
this pull request
Oct 25, 2024
leanprover-community-bot
added
the
builds-mathlib
|
Mathlib CI status (docs):
|
tobiasgrosser
pushed a commit
to opencompl/lean4
that referenced
this pull request
Oct 27, 2024
…ver#4846) `generalize ... at *` sometimes will try to modify the recursive hypothesis corresponding to the current theorem being defined, which may not be the expected behaviour. It should only try to `generalize` hypotheses that it can actually modify and are visible, not implementation details. Otherwise this means that there are discrepancies between `generalize ... at *` and `generalize ... at H`, even though `H` is the only hypothesis in the context. This commit uses `getLocalHyps` instead of `getFVarIds` to get the current valid `FVarIds` in the context. This uses `isImplementationDetail` to filter out `FVarIds` that are implementation details in the context and are not visible to the user and should not be manipulated by `generalize`. Closes leanprover#4845
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.
generalize ... at *sometimes will try to modify the recursive hypothesis corresponding to the current theorem being defined, which may not be the expected behaviour. It should only try togeneralizehypotheses that it can actually modify and are visible, not implementation details. Otherwise this means that there are discrepancies betweengeneralize ... at *andgeneralize ... at H, even thoughHis the only hypothesis in the context.This commit uses
getLocalHypsinstead ofgetFVarIdsto get the current validFVarIdsin the context. This usesisImplementationDetailto filter outFVarIdsthat are implementation details in the context and are not visible to the user and should not be manipulated bygeneralize.Closes #4845