[Merged by Bors] - fix(Tactic): make eta_expand idempotent#35607
[Merged by Bors] - fix(Tactic): make eta_expand idempotent#35607gasparattila wants to merge 3 commits intoleanprover-community:masterfrom
eta_expand idempotent#35607Conversation
The docstring of `eta_expand` says that it puts terms into a normal form, implying that it is idempontent, however, this is not the case in some tricky cases. This PR changes `eta_expand` so that it gives the normal form in one step.
PR summary fadcf92bfcImport changes for modified filesNo significant changes to the import graph Import changes for all files
Declarations diffNo declarations were harmed in the making of this PR! 🐙 You can run this locally as follows## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>The doc-module for No changes to technical debt.You can run this locally as
|
|
This pull request is now in draft mode. No active bors state needed cleanup. While this PR remains draft, bors will ignore commands on this PR. Mark it ready for review before using commands like |
Vierkantor
left a comment
Vierkantor
left a comment
There was a problem hiding this comment.
Could you explain why the original use of transform needs to be replaced with this new loop? Since the new version is more verbose and likely less efficient, I'd like to go back to transform if possible.
Vierkantor
added
the
awaiting-author
|
When the current implementation encounters an application, say This could be avoided if we could eta-expand only the subterms of the function in the application, but I couldn't find a way to do this using -awaiting-author |
github-actions
bot
removed
the
awaiting-author
| | e@(.app ..) => | ||
| let f := e.getAppFn | ||
| let args := e.getAppArgs | ||
| if f.etaExpandedStrict?.isSome then |
There was a problem hiding this comment.
| if f.etaExpandedStrict?.isSome then | |
| -- Note that we call `expandSubterms` instead of `etaExpandAll` below, | |
| -- because we also want to eta-expand the arguments to `f` (without beta-reducing them) | |
| -- in case those arguments are functions themselves. | |
| if f.etaExpandedStrict?.isSome then |
There was a problem hiding this comment.
I don't understand this explanation, so instead, I added a comment below to clarify that this implementation doesn't create new beta-redexes. In expandSubterms (f.beta args), I believe that etaExpandAll would give the same result, but expandSubterms avoids an unnecessary call to inferType.
Vierkantor
left a comment
Vierkantor
left a comment
There was a problem hiding this comment.
I see! Let's add an explanatory comment in that case. I think I got my explanation correct, please check.
bors d+
|
✌️ gasparattila can now approve this pull request. To approve and merge a pull request, simply reply with |
mathlib-triage
bot
added
the
delegated
|
bors r+ |
The docstring of `eta_expand` says that it puts terms into a normal form, implying that it is idempontent, however, this is not the case in some tricky cases. This PR changes `eta_expand` so that it gives the normal form in one step.
|
Pull request successfully merged into master. Build succeeded:
|
mathlib-bors
bot
changed the title
eta_expand idempotenteta_expand idempotent
The docstring of `eta_expand` says that it puts terms into a normal form, implying that it is idempontent, however, this is not the case in some tricky cases. This PR changes `eta_expand` so that it gives the normal form in one step.
The docstring of `eta_expand` says that it puts terms into a normal form, implying that it is idempontent, however, this is not the case in some tricky cases. This PR changes `eta_expand` so that it gives the normal form in one step.
The docstring of `eta_expand` says that it puts terms into a normal form, implying that it is idempontent, however, this is not the case in some tricky cases. This PR changes `eta_expand` so that it gives the normal form in one step.
4 participants
The docstring of
eta_expandsays that it puts terms into a normal form, implying that it is idempontent, however, this is not the case in some tricky cases. This PR changeseta_expandso that it gives the normal form in one step.