Idiomatically adding extra hypotheses to Aesop

Stream: metaprogramming / tactics

[Geoffrey Irving]

The bound tactic supports registering extra hypotheses in a call as bound [h0, h1 x] similar to linarith. However, this is handled in elaboration before getting to the aesop call, and I just realized that this breaks tactic script generation from bound? which calls ‘aesop?` as the hypotheses wouldn’t show up in script generation.

@Jannis Limperg Is there a more idiomatic way of registering extra hypotheses, including hypotheses that are general terms? The most important thing is that they participate in forward rules, in particular so that added 0 < x turn into 0 <= x.

[Jannis Limperg]

For hypotheses, you should be able to do aesop (add ... hyp) as usual. Composite terms are not currently supported, but I'm implementing this now. (I've wanted to support this for some time.)

[Geoffrey Irving]

Ah, nice! Is hyp mentioned in the README? I don’t see it on a skim just now.

What’s the ETA for composite terms? I’d love to have it for bound.

[Jannis Limperg]

There's one sentence about local hyps in the reference section of the README, but maybe I should stress this in the tutorial as well. ETA for composite terms tomorrow hopefully, but my estimates are always extremely optimistic.

[Geoffrey Irving]

Is it possible to put in the list of rule builders?

[Geoffrey Irving]

That was the first (and second and third) places I looked. :)

[Geoffrey Irving]

Tomorrow is terrific, even if it slips, as likely bound will take more time. Is there an issue or PR so that I can register that bound depends on that?

[Geoffrey Irving]

Actually, where’s that sentence? Searching for “local hyp” finds nothing.

[Geoffrey Irving]

Ah:

The local set contains rules from (add ...) clauses.

Unfortunately it doesn’t say what the syntax is.

[Geoffrey Irving]

Wait, I’m confused: what can it be used for if composite terms aren’t allowed? It can’t be a local thing, since that’s already a hypothesis. And there are very few singleton global hypotheses that make sense to add, as most theorems have their own hypotheses.

[Jannis Limperg]

Geoffrey Irving said:

Tomorrow is terrific, even if it slips, as likely bound will take more time. Is there an issue or PR so that I can register that bound depends on that?

aesop#110. Now I just need to remember to close it in the commit message. :)

[Jannis Limperg]

Geoffrey Irving said:

Actually, where’s that sentence? Searching for “local hyp” finds nothing.

The rule names can also refer to hypotheses in the goal context, but not all
builders support this.

[Jannis Limperg]

I think the stuff with the local rule set is outdated actually...

[Jannis Limperg]

Geoffrey Irving said:

Wait, I’m confused: what can it be used for if composite terms aren’t allowed? It can’t be a local thing, since that’s already a hypothesis. And there are very few singleton global hypotheses that make sense to add, as most theorems have their own hypotheses.

The local rule set used to contain everything that was added for that specific Aesop call. (I call these rules local.) And a local rule can be, but doesn't have to be, based on a local hypothesis.

[Geoffrey Irving]

Ah, I see: I misinterpreted. “hyp” wasn’t syntax, but a name for an argument. So a lot of the above conversation was confusion on my end.

To restate: say I have a global identifier with no hypotheses (“foo”, say). Is there an add syntax that has equivalent semantics to adding it as a hypothesis prior to starting Aesop? My sense is no, because:

1. If it’s an apply or norm rule, it won’t participate in forward rules.
2. If it’s a forward rule it won’t work, as forward rules expect to have hypotheses over their own.

Is (2) wrong, such that I could register a forward rule with no hypotheses that would immediately fire at the beginning of Aesop?

[Geoffrey Irving]

I think this is an independent feature from the composite term one.

[Geoffrey Irving]

The main thing I want relative to actually just adding it as a hypothesis prior to calling Aesop is participation in proof script generation via aesop?

[Jannis Limperg]

I can remove the restriction that forward rules must have premises. (This is an artificial restriction, so I just need to delete two lines.) You can then register your constants as forward rules with no immediate premises. This is quite inefficient at the moment because the rule will fire for every goal, construct the new hypothesis and then realise that the hypothesis was already added. But with the new forward architecture that's in the works, this will become efficient.

Alternatively, you could add the hypotheses yourself, generate the syntax of an assert tactic for each and combine these tactic syntaxes (is that a word?) with the script that Aesop generates.

[Geoffrey Irving]

That restriction does seem useful to catch mistakes, so I’ll leave it to your judgement. The alternative would be a new rule builder that does this specific thing.

For now I might just strip bound?’s support for hypotheses.

[Jannis Limperg]

I've now removed the restriction on forward rules.

[Geoffrey Irving]

Thank you! Is there something I can follow for when they won't be slow?

[Jannis Limperg]

aesop#111

[Jannis Limperg]

I've also implemented composite terms in local rules and, as a bonus, nice syntax for adding tactics. So you can now write (add safe (h x)), where h and x may be hypotheses, and (add safe (by norm_num)). The parentheses are mandatory.

[Geoffrey Irving]

The tactic syntax is cool.

[Jannis Limperg]

In the process, I've had to make a backwards-incompatible syntax change: the rule_sets clauses are now written (rule_sets := [...]) instead of (rule_sets [...]).

[Jannis Limperg]

Geoffrey Irving said:

Thank you! Is there something I can follow for when they won't be slow?

I should say that unless you have many complex forward rules, the current implementation is probably still fast enough. It's the Python of forward reasoning tactics.

[Geoffrey Irving]

I should probably switch bound to it now then. Or rather, not now, but as soon as it hits main mathlib. What's the typical ETA for that?

[Geoffrey Irving]

Usually there are only 1 or 2 extra hypotheses at most (zero is most common), so it is probably just fine.

[Geoffrey Irving]

Actually I'll know immediately when that change lands in Mathlib, since I'll have to do the := change. Useful signal! :)

[Jannis Limperg]

I'll do the Aesop bump for Mathlib soon-ish.

[Jannis Limperg]

There's now also a command add_aesop_rules that can be used to add tactics or composite expressions to global rule sets. Mathlib bump is in progress.

[Geoffrey Irving]

(deleted)