Documentation of all tactics

Stream: mathlib4

[Jon Eugster]

Robert Maxton said:

I think this is mostly an artifact of the lack of good (esp. good "canonical") documentation for tactics. To my knowledge the only way of getting any sort of systematic coverage of what tactics are available is through Haruhisa's trick, which yes, results in a big barrier to entry that scales with the number of tactics. But if we had, in any of our three major documentation sources, a guide to the most common/"center path" tactics that work most of the time in each field, then having variants IMO ceases to be a barrier to entry; new users should follow the documentation and use the rarely-changing shortlist of common tactics to get started, and treat the variants as "advanced usage."

... Actually, do the various textbooks take PRs? Because I might just contribute an appendix somewhere myself.

I'm trying to advocate this automatically generated list of all tactics in Mathlib which is already linked on leanprover-community.github.io

If you have the time and motivation, contributing to it would be much appreciated and I think it would be a good investment of time as Verso should help us keeping the document updated in the future.

There are two fronts to contribute:

• Create PRs to mathlib (and dependencies) marking alternative forms of tactics with @[tactic_alt original_tactic], cleaning-up docstrings as you do so, i.e. describing all tactic alternatives in the main tactic's docstring. I already did this for abel, see the merged #21085. This reduces the number of individual tactics on the list. (e.g. there are currently 7 different have tactics on the list)
• In the sections before "All tactics" there is a draft for categorising some tactics manually into small and useful bits. These sections could always need some more thought and editing in order to be as useful as they can be. At this stage it would also be appreciated if you completely scrapped some sections or introduced new ones depending on what you think would be useful! I'm happy to merge any PRs to that repository :smile:

I believe in this approach because there is no documentation written which can rott: The sorted & curated lists of tactics are something any documentation would need as a base and everything else comes directly from the source code.

[Jon Eugster]

There are also 19 tactics starting with simp... on the list, so certainly there is another option for improvement...

[Bhavik Mehta]

In https://leanprover-community.github.io/mathlib-manual/html-multi//Tactics/All-tactics/#Lean___Parser___Tactic___match, hovering over match gives a pretty unhelpful docstring. In this case it's fine, since I'm looking at a helpful description anyway, but this looks like Verso doing something suboptimal if match gives this message in other situations too.

[Jon Eugster]

nice spot: I've asked this question at https://github.com/leanprover/verso/issues/351 with detailed description.
(although, arguably for this particular example the solution might be to just remove the conflicting syntax which has been deprecated a year ago)

[Michael Rothgang]

I went a bit further through the tactic list, and have tried to categorise very apparent duplicates.

In mathlib, so easily actionable

• measurability (four versions)
• use and use! (the doc-string already explains both variants, so this may just need tactic_alt)
• choose and choose! (same story)
• I wonder if the doc-strings for by_contra and by_contra! can be combined: this requires closely looking at them, though

Definitely defined in core

• apply, apply at and apply with a config should be unified
• three versions change which could be combined
• bv_decide and bv_decide? are present twice each

• simpa_all?, simp_all?!, dsimp? and dsimp?! have the exact same doc-string as simp?: that's not helpful :-)
  Perhaps dsimp should explain dsimp!, dsimp? and dsimp?!` also; similarly for simp_all.

• trace (two copies)

I'm not sure if the following are in core or not

• maybe the repeat(')(1) versions should also be combined
• should rename and rename' be combined?
• there are many variants of have('), some in mathlib, some in core
• observe? has the same doc-string twice: combining them would be useful