why (or why not) aesop?

Stream: mathlib4

[Thomas Murrills]

First, let me say that Aesop looks (very) cool!

My broad question here is: when should a to-be-ported tactic be rewritten using Aesop?

I noticed we ported continuity using Aesop, and from what I hear that seems to have worked very well. I was wondering which other tactics should be ported with Aesop under the hood, and how we can decide. Why use Aesop over a label attribute plus e.g. solve_by_elim, a simp wrapper, or a bespoke strategy in some given circumstance? What are the intended use cases that distinguish Aesop from other, similar strategies?

While I’m curious about the general case, I did also have a particular question that motivated this: I was wondering whether docs#tactic.interactive.mono should be ported via Aesop. It’s got a few configuration options, and I was wondering if Aesop could support these (even if indirectly, under some wrapping). in particular, we have mono left, mono right and mono/mono both as attributes, not just mono, plus analogous tactic syntax to restrict to left or right rules. It also has with … syntax which helps mono choose which rules to use.

[Moritz Doll]

I had that idea as well and this was Jannis response:
https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Tactic.20porting.20assignments/near/316258985

[Thomas Murrills]

Oh, I missed that message, thanks!

Hmm. I wonder if it would be possible (and/or worth it) to pull the plumbing out of Aesop to just do a single mono call?

I also wonder if it can replace non-terminal mono* calls (if that’s a thing).

It would be nice to have a sort of dictionary of standard frameworks in lean/mathlib4 for rewriting expressions with rulesets; as-is I’m not sure what the tradeoffs of each method are.

[Moritz Doll]

I guess it is trivially possible to remove non-terminal mono* calls by using have more, which might be a good idea in itself

[Jannis Limperg]

To answer the general question: any tactic that amounts to "apply a collection of tactics exhaustively until the goal is solved" is possibly a good fit for Aesop. The problem with mono is that it also does other things; in particular it doesn't necessarily aim to solve the goal.