Towards a more beginner-friendly tactic doc

[utensil]

As discussed in Zulip, we could:

Provide usage examples for each tactic

Jalex Stark 2:27 AM
Maybe every tactic doc should have a usage example in it, similar to say tactic#abel?
(I mean to pose the question: if I want to contribute to tactic docs, can I do a run of indiscriminately adding examples?)

Rob Lewis 2:40 AM
Yes, I'm very much in favor of this.

Kevin Buzzard3:05 AM
In NNG I went for summary, then details, then examples. It might even be best to do summary, then examples, then details, when it comes to docs. I guess the docs can say different things to the hover result, which might want to be more compact in general

Address more aspects of a tactic

• Direction:
  • What does the tactic apply to? the goal, the hypotheses, or both?
  • Which tactic should I use if I need to do the same in the opposite direction? (backward proof v.s. forward proof)
• Scenario:
  • Under what specific circumstances should I think about using the tactic?
• Scope:
  • What family does the tactic belong to?
  • what scope of the problem does the family solve?
• Behavior:
  • What does the tactic do?
• Variants:
  • Are there slightly modified versions to also do xxx, yyy?
• Alternatives:
  • What else can I try in a similar circumstance? (it's like an ordered tactic chain, such as ac_refl, cc, abel etc., one stronger than the other)
• Style:
  • Which tactics to use if I want to do the same in another proof style?
• Reduce:
  • What if I want to have more control on a tactic that's too smart? (such as from simp to squeeze_simp, simp_only, rw etc.)
• Simplify:
  • How can I simplify a series of steps( which seem to have a pattern ) to just one or few tactics?
• Partners:
  • Which tactics should I use together with this tactic?
• Parameters:
  • What parameters can I pass to the tactics? What do they control?
  • Can I just copy-paste a part of the expression? Why sometimes copy-paste doesn't work? When can Lean infer them for me?
• Equivalents:
  • in informal mathematical proofs
  • in Coq, Agda, Isabelle etc.

Improve the organization of tags

There're 3 major issues of tags:

• they're not clickable from a tactic and one has to explicitly use the filter function
• there're many of them and they're alphabetically ordered and not grouped, and tactics in them are again alphabetically ordered (thus no logical organization)
• some tags are underused e.g. conv, category theory, equiv, hypothesis management, monotonicity, transport etc. and not necessarily exhaustive

[robertylewis]

I would be very happy to see more structure put into the tactic docs. As of a year ago, mathlib had no documentation standards at all; tactic doc strings, if they existed at all, were purely by the generosity of the tactic writer. The current status is much better, but obviously there's a long way to go.

People are generally willing to contribute documentation. But there's obviously a balance: the more you ask for, the slower it will happen.

What I would suggest is writing a markdown template like yours above, with a few (say, 4-5) headers, and a few suggestions under each of those. Something like

# Summary
* What does the tactic do?
* What scope of problem does the tactic solve?

# Details
* What paramaters can I pass the tactic?
* Are there variants?

# Examples 
* Examples that show off all parameter options and variants

# Further notes
* Companion tactics
* Style
* ...

While your list contains a lot of important information, it's a lot, and not every tactic has an answer to every question. I would rather ask for the essential core and get consistent results than ask for the world and get messier results at a slower pace.

[robertylewis]

As for tags: I'm happy to accept pull requests that change the tag assignments themselves and the html display.

Sorting is complicated. I think it's very important that the docs are generated from the library and not maintained separately. It's hard enough keeping things up to date as it is; there's a reason we moved from a manually "curated" list of tactics to the generation scheme. Of course, this makes it difficult to sort, because sorting isn't a local thing.