-
Notifications
You must be signed in to change notification settings - Fork 28
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
Rule suggestion: elim *
#19
Comments
Which hypotheses would be forward-applied exactly? I see two possibilities:
The first option is
|
Great question, especially since the former behavior would be another solution to my ordering issue example. So while I agree that the latter behavior looks more useful in general, I would be happy with the first option 😄 . |
Btw, another way to look at the original issue: Aesop is called on multiple induction cases and in each case, we want to forward-apply the IH. So we really want This is a bit of a hack, but it would allow us to keep the rule set more predictable while reducing configuration overhead. |
An interesting idea, though it would have to be I'm not sure if having other implication hypotheses in the context is a common enough case to warrant this granularity. Could happen with some stray |
Yet another idea: if we want the more generally useful behaviour of |
The name resolution adjustment seems useful with such rules, yes. I'm also happy to just keep the rule local for now, we can wait and see if anyone else needs it :) . |
Now that I think more about it, changing the name resolution would encourage people to put their rules into the @[aesop norm 5 (disable := true) (name := n)]
def NS.rule : RuleTac := sorry
examle : True := by
aesop (add n) This may still lead to name clashes, but then people can use the full name to disambiguate. I think I'll leave this issue unresolved for now and return to hairy metavariable bugs. But I'll get back to it at some point. |
For what it's worth, I'm not a big fan of introducing name spaces (in the general sense) parallel to the regular Lean names. I'd like to get rid of the special parser name space used in |
To get rid of the last item in https://github.com/IPDSnelting/tba-2022/blob/master/TBA/Util/AesopExts.lean. I assume this can be useful for forward reasoning with IHs in other projects as well. If the syntax looks agreeable, I can give implementing this a try. I suppose the
*
would have to become a new kind ofaesop.feature
.The text was updated successfully, but these errors were encountered: