Annotating `aesop`

Stream: mathlib4

[Kevin Buzzard]

We were told when aesop hit that we should go through mathlib tagging lots of lemmas with @[aesop] and then aesop would be brilliant. I am not convinced that this ever happened.

However I am actually quite confused about all this. I occasionally mention this post by Anand Rao where he tags some inequality lemmas with the aesop tag and then bam, aesop can solve inequality lemmas in partial orders (and lattices). But I am not sure that the conclusion of this is that those lemmas should globally be tagged @[aesop]. So this brings me to my question: is "making aesop better" just a question of "tagging as many lemmas in the library as possible with aesop" or is this not actually the correct way to use the tactic, and the correct way is to have lemmas which should only be tagged aesop when working on goals in a certain area, by which in practice I guess I mean making bespoke tactics like aesop_cat?

[Johan Commelin]

@Artie Khovanov has been looking into this recently. Let me try to find the other thread

[Johan Commelin]

#mathlib4 > Adding / modifying Aesop lemmas

[Bhavik Mehta]

The way I often use aesop is to locally add lemmas to its set, which are globally probably not sensible but are useful in my specific file. For instance in #20082, I write

attribute [aesop norm 10 tactic] Lean.Elab.Tactic.Omega.omegaDefault
attribute [aesop 2 simp] Set.subset_def Finset.subset_iff

(the first one tells aesop to try omega, it would be nice if the notation was cleaner here!) Both of these are absolutely not sensible for mathlib in general, but in that specific PR it makes proofs nicer. Similarly in #20759 (merged), all the proofs are something like aesop (add safe forward [le_antisymm, le_of_lt]): here instead of adding the attribute in the file, I just repeat the same call a few times, but it's the same pattern.

My pattern is to do what we used to do with simp: put it at the end and keep moving it upwards until it stops working. In the simp case, we'd usually stop at anything that's not a rw, but with aesop I can add apply lemmas using add ... forward too, or add local simp lemmas using add ... simp. I have no idea if this is how we're meant to use it, but I like it anyway!

[Kevin Buzzard]

The other thread seemed to end up talking about several different things. But I am coming to the same conclusion as Bhavik -- aesop is not some one-size-fits-all tactic, the way it's to be used is that a user needs to supply their own lemmas. Is this correct?

[Bhavik Mehta]

I think it's meant to be extensible (I believe that's what the e in aesop stands for!). But we also have the option of building common rulesets like Anand's example or aesop_cat or finsetNonempty. So, both?

[Anand Rao Tadipatri]

I agree with Bhavik that rule sets would be the ideal way of tagging and grouping lemmas related to a given area.

(Here's an example of what this looks like in practice).

Joachim Breitner suggests towards the end of the thread on lattices that syntax like aesop [cat] or aesop [graph] would be nicer than having bespoke tactics for each of these areas, since this would allow room for composite tactics like aesop [cat, order]. I agree and think that this in combination with rule sets would be the best way forward.