Best practices with powerful tactics

Stream: Analysis I

[Rado Kirov]

I recently learned about simp? and aesop?, so now I wonder is it best practice in the final proof to expand these tactics to the output of their ? equivalents or leave them unexpanded. Especially for aesop the outcome can be quite long, but sometimes I can massage it down to manageable size.

[Kevin Buzzard]

The mathlib rules (as I understand them) are that if these tactics are being used as finishing tactics (ie to close a goal rather than just change it) then it's usually fine to leave them as they are. The exceptions are: if simp takes a long time and simp only ... is much quicker then feel free to squeeze, and I personally sometimes take a look at what proof Aesop found in case it was just rfl or intros;.ext; simp or whatever, and might well replace the Aesop call with the simpler call in this case.

[Damiano Testa]

In terms of general principles, there are issues of maintainability and performance that sometimes push in opposite directions.

There have been some pretty extensive related discussions talking about the difference between flexible and rigid. Mathlib even has a linter that will help identify potential maintainability issues caused by non-terminal simps and related tactics.

[Damiano Testa]

See for instance #mathlib4 > flexible vs rigid tactics.

[Dan Abramov]

Not sure it's helpful but the rule of thumb I've settled on using for myself (specifically in the context of Analysis book exercises) is to:

• Only use aesop or simp if I can retrace the argument mentally on the spot and I'm confident in it (but it's annoying to type).
• Only use simp only rather than simp, and always verify that each suggested lemma was actually necessary.
• If I've settled on aesop or similar, then I'll clean up the lines before to remove other stuff it's able to do. Unless the shape of the proof disappears completely, in which case I'd still leave enough of the skeleton to retrace the argument. So basically, only skip out "trivial" parts.

[Rado Kirov]

Those are good rule of thumb, I will try to follow them going forward, and maybe one day go back and clean up.