tactic cheat sheet examples

Stream: general

[Mark Ettinger]

As I learn Lean, I've found this tactic cheatsheet very helpful: https://raw.githubusercontent.com/fpvandoorn/LeanCourse24/master/lean-tactics.pdf

However it would be super useful if there were a single document ( in contrast to spread out over the standard intro texts) which showed the use of each of these tactics in an example. Does such a thing exist already (or similar)?

[Kevin Buzzard]

The course notes for Imperial's Lean course https://b-mehta.github.io/formalising-mathematics-notes/Part_2/Part_2.html have tactic documentation written for mathematician beginners.

[Anthony Wang]

Mark Ettinger said:

As I learn Lean, I've found this tactic cheatsheet very helpful: https://raw.githubusercontent.com/fpvandoorn/LeanCourse24/master/lean-tactics.pdf

By the way, I think the canonical URL for that cheatsheet is https://leanprover-community.github.io/papers/lean-tactics.pdf which is slightly more up-to-date.

[Martin Dvořák]

I am fascinated by how many versions this document has!

[Jovan Gerbscheid]

Maybe an entry on grw should be added :)

[Asei Inoue]

How about https://lean-ja.github.io/lean-by-example/ ? (Japanese only)

[Aaron Liu]

unfortunately not everyone knows Japanese

[Aaron Liu]

This seems like a whole book not just a tactic cheat sheet

[Floris van Doorn]

Jovan Gerbscheid said:

Maybe an entry on grw should be added :)

leanprover-community/leanprover-community.github.io#692

[Jovan Gerbscheid]

Should push_neg be entirely removed from the list?

Relatedly, should push_neg be deprecated from Mathlib in favor of push ¬ _?

[Floris van Doorn]

I don't want the cheat sheet to be comprehensive (that would be too much), so I'm happy to leave it off. And I think knowing about push/pull is much nicer for new(ish) people to Lean, especially once we have tagged a whole lot more push-lemmas.

[Floris van Doorn]

I don't have a strong opinion of deprecating push_neg from Mathlib. Maybe not now, but maybe later, once push/pull is widely used for other operations?

[Patrick Massot]

I’m in favor of not having many ways of doing the same thing. If push ¬ is equivalent (or better) than push_neg then we can deprecate push_neg in Mathlib (especially if we can do that without triggering deprecation warning in projects depending on Mathlib).

[Jovan Gerbscheid]

The current syntax is push ¬ _ or push Not (and these are equivalent to push_neg). Do you think it would be good to have a macro to allow writing push ¬?

[Patrick Massot]

Sorry, that was a typo. push Not is fine.

[Sorrachai Yingchareonthawornchai]

Jovan Gerbscheid said:

Maybe an entry on grw should be added :)

Also, maybe an entry on suffices and wlog  can be added?

[Mark Ettinger]

@Kevin Buzzard Thanks for these notes. I feel they fill an important gap in the ramp-up docs, especially the tactics section but also the tips section.

[Jovan Gerbscheid]

Should tauto be removed from the cheat sheet now that grind supersedes it?

[Jovan Gerbscheid]

Also I was surprised that the sheet contains pick_goal n but not on_goal n =>. Isn't on_goal is the preferred form?

[Floris van Doorn]

Jovan Gerbscheid said:

Should tauto be removed from the cheat sheet now that grind supersedes it?

If grind is now preferred, I'm happy to remove tauto

Jovan Gerbscheid said:

Also I was surprised that the sheet contains pick_goal n but not on_goal n =>. Isn't on_goal is the preferred form?

I'm happy to change this!

Please PR fixes.

[Kim Morrison]

Floris van Doorn said:

If grind is now preferred, I'm happy to remove tauto

No, there are many places where tauto can not be replaced with grind (yet? :-). Perhaps you are thinking of cc.

[Kim Morrison]

#30619 adds the (off by default) linters:

• linter.tacticAnalysis.tautoToGrind which reports all uses of tauto that can be replaced by grind
• linter.tacticAnalysis.regressions.tautoToGrind which reports all uses of tauto that can not be replaced by grind

[Kim Morrison]

(tauto, or rather its constituent parts, e.g. assumption, contradiction, solve_by_elim, rfl, and constructorMatching is much more willing to unfold definitions than grind is)

[Jovan Gerbscheid]

I also noticed that contrapose/contrapose! isn't on the cheat sheet. (nor is absurd, which can be used together with exfalso to emulate contrapose)

[Mirek Olšák]

It is hard to be comprehensive, and to select representative tactics... this is my attempt
https://git.olsak.net/mirek/lean-teaching/src/branch/master/LeanTeaching/Lecture4_TacticZoo.lean

[Mirek Olšák]

If we could make the list of tactics produced by this meta-code hoverable, it would be nice! I have not yet figured out if it is possible to give MessageData a custom hover, or I need to fit into the Lean data categories (maybe DocElabInfo?)

import Batteries

open Lean Meta Elab Tactic Command in
def listStx (stx : Name) : CommandElabM Unit := do
  let cat := (Parser.parserExtension.getState (← getEnv)).categories.find! stx
  let env ← getEnv
  let mut tactics := #[]
  for (k, _) in cat.kinds do
    if let some tk := do
      Batteries.Tactic.getHeadTk (← (← env.find? k).value?) then
      let tk := tk.trim
      tactics := tactics.push tk
  tactics := tactics.qsort
  logInfo <| "\n".intercalate tactics.toList

run_cmd listStx `tactic

[Damiano Testa]

It seems like #help tactic could be useful.

[Mirek Olšák]

I know #help tactic but that is extremely messy. I want only the list, but see what the tactic does once I hover over it.

[Mirek Olšák]

Ideally with correctly displayed markdown... :slight_smile: am I asking too much?

[Damiano Testa]

If you are happy to hover over the parser name, you can get the ConstantInfo from the environment, but instead of the value, extract the name. Then MessageData.ofConstName will print the parser name with the hover.

[Mirek Olšák]

Actually, you are right -- #help tactic has the syntax element hoverable... so it might be possible to replace the string inside

[Mirek Olšák]

I would prefer if it was clean -- without parser names (users do not care about them).

[Mirek Olšák]

But thanks, I have another direction to investigate...

[Mirek Olšák]

Here we go :tada: List tactics

[François G. Dorais]

The #help command suite could use some sprucing up: PRs welcome!

[Mirek Olšák]

To make it a library version, I would be happy to remove the Lean.ParserDescr header, but I am not sure if it is feasible...

[Asei Inoue]

you may want https://seasawher.github.io/mathlib4-help/ ?