Recursing with several tactics

Stream: metaprogramming / tactics

[Yaël Dillies]

I am reviving #10645 and this requires writing a tactic that solves goals of the form roth_number_nat a = b. The idea of the tactic is very simple: you have obligations of the form roth_aux a m d l, roth_aux₁ a m d l, roth_aux₂ a m d l, I have a few lemmas that turn (uniquely) one of those goals into a combination of others (and termination is guaranteed but of course I don't care here).

[Yaël Dillies]

Now my naive idea was to make one tactic for each of roth_aux, roth_aux₁, roth_aux₂ to apply those lemmas correctly (there are several lemmas for each, so the tactic isn't just applying one lemma), but of course I need to declare the tactics in some order in the file, and I can't refer to the last tactic from the first.

Am I stuck?

[Jannis Limperg]

Have you tried making your tactics mutual?

[Yaël Dillies]

RIght now I'm going with a single inductive tactic indexed by an inductive three elements type, which I guess is the same?

[Yaël Dillies]

I am mostly wondering whether I missed an obvious solution.

[Jannis Limperg]

Yeah, that's also fine. The mutual solution essentially compiles to what I imagine you're doing. mutual has no downsides when you're in meta land (in non-meta land, termination checking doesn't work), so it's perhaps more idiomatic in this case.

[Junyan Xu]

Can you do tactic × tactic × tactic? Similar to how docs#pgame.le_lf is done.

[Yaël Dillies]

Wouldn't that make two of the three tactics run unnecessarily every time?

[Kyle Miller]

Another strategy is to have some tactics that look at the goal, decide whether they apply, and perform a single step, then iteratively apply these tactics. It's a sort of recursive-to-iterative transformation, and it's somewhat similar to norm_num plugins.

[Yaël Dillies]

Yes, that's how Bhavik started the implementation, but it feels a bit wasteful to call tactic.target several thousand times in the same proof.

[Kyle Miller]

If you care about that, you could give the target as an argument to these tactics and thread it through.

[Kyle Miller]

(I'm not sure if there's much of a performance penalty to tactic.target, but I've never measured it.)

[Kyle Miller]

Yaël Dillies said:

to apply those lemmas correctly (there are several lemmas for each, so the tactic isn't just applying one lemma)

Is there a finite list of lemmas you could generate that you could use apply_rules with?

[Yaël Dillies]

Yes, I am basically implementing a custom apply_rules.

[Yaël Dillies]

... except that I will later add memoisation to the mix, and that requires special handling.