-
Notifications
You must be signed in to change notification settings - Fork 99
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
refactor: avoid relying on rfl's behavior on ground terms #832
base: main
Are you sure you want to change the base?
Conversation
`rfl` for ground terms will reduce at transparency `.all`, even if the current transparency is `.default`. Maybe it's prudent to not rely on this corner case, and have more explicit proofs.
I understand where this is coming from but I'm skeptical of I guess I mean a tactic that would locally unseal some defs but not use simp lemmas. Maybe it could even try to figure out what defs to unseal without user prompt. |
Yes, this PR is a mit premature, I should first figure out if this rfl behavior is intended or accidental. Using simp isn't unreasonable in the sense that the other half of that proof is also rewriting. But I am more hesitant to rely on DefEqs of irreducible definitions than others :-) Marking as draft for now. |
I don't think these two changes are problematic by themselves. I'm mostly questioning the general strategy of replacing To be more specific about my (currently purely theoretical) vision is for an Note that the equations used by Anyway, this discussion should probably be elsewhere. |
Ah, I see what you are getting at: An evaluator of ground terms that uses the equations as specified, but not necessarily as elaborated (which suffers at least for well-founded definitions). A good approximation to that is |
I’m working on leanprover/lean4#3772 again, so I expect his will be needed soon. I’d wager that |
I still don't think |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
These two changes are fine but I would still like a better solution for the general case.
rfl
for ground terms will reduce at transparency.all
, even if the current transparency is.default
. Maybe it's prudent to not rely on this corner case, and have more explicit proofs.