Rule suggestion: elim *

[Kha]

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 of aesop.feature.

[JLimperg]

Which hypotheses would be forward-applied exactly? I see two possibilities:

• All hypotheses from the goal to which Aesop is initially applied.
• All hypotheses from all goals which arise during the search.

The first option is

• Easier to implement.
• More consistent with the current meaning of add h(?).
• Less useful(?).

[Kha]

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 😄 .

[JLimperg]

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 aesop (add ih elim), but this doesn't work because the IHs have different names. We could add syntax to specify these names in bulk, e.g. add ih* elim to add a rule for each hyp whose name starts with ih or add ih_a? elim to add a rule for the hyp ih_a if it exists.

This is a bit of a hack, but it would allow us to keep the rule set more predictable while reducing configuration overhead.

[Kha]

An interesting idea, though it would have to be *_ih for induction/...'s default naming scheme. And it doesn't help that Lean won't even show the hypothesis names in the goal view in this case, so users would have to guess at their internal names.

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 haves though I suppose.

[JLimperg]

Yet another idea: if we want the more generally useful behaviour of elim *, this just requires a rule like your elimAny. If we add this to the Aesop codebase, users could add Aesop.Rule.elimAny. Since this is a bit long, we could hack the resolution procedure for rule names to expand add elimAny into add Aesop.Rule.elimAny, provided that elimAny is not already in scope.

[Kha]

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 :) .

[JLimperg]

Now that I think more about it, changing the name resolution would encourage people to put their rules into the Aesop.Rules namespace, leading to potential name clashes. But a similar effect could be achieved by adding a way to disable rules and give them a short name. Syntax mockup:

@[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.

[Kha]

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 syntax as well, for example. A default namespace on the other hand seems fine to me; encouraging people to use it could be said equally about the root namespace, so people just have to realize in both cases that it's probably not a good idea.