Lean Cheat Sheet

Stream: new members

[Utensil Song]

I've been reading (and trying out the exercises in) many tutorials for Lean. The knowledge absorbed from scattered sources is becoming a memory burden and I have at least the personal need to create a cheat sheet that has high information density and is well organized for quick reference.

Apparently, I would not be the first to need such a cheat sheet, so I searched Zulip to see if there're already such cheat sheets. But I could not find one that's ideal.

There're:

• @Kevin Buzzard 's cheat sheet mentioned here, but it's a dead link
• @Patrick Massot 's cheat sheet mentioned here, but it has no direct link and I could not find it
• https://github.com/jldodds/coq-lean-cheatsheet which is a little dated and not so complete, there're better ones in Coq world such as https://www.cs.cornell.edu/courses/cs3110/2018sp/a5/coq-tactics-cheatsheet.html

What I have in mind is something as rich as https://cheats.rs/ ( it's a long page, please have a quick scroll-down ), it covers all most every aspect of the language and the ecosystem in a concise manner with links to the original sources (there're many open books/tutorials in Rust world too).

Its structuring of contents and its tech stack (see its source) are mostly reusable for Lean. I'm motivated to create a prototype and a skeleton for Lean based on it, at least cover the part I know of, distilling information from the books/tutorials that I've read. Just post here (before I even start doing so) to see if anyone has some plans/needs similar in mind.

[Patrick Massot]

The link to my cheat sheet is https://www.imo.universite-paris-saclay.fr/~pmassot/enseignement/math114/tactiques.pdf but this is very specific. It refers to a very specific teaching context, it even contains one tactic that is not in mathlib.

[Patrick Massot]

If you have time and energy to make something useful it could be great

[Kevin Buzzard]

The contents of the dead link looked like this: tactic_guide.png

[Kevin Buzzard]

The tactic guide got swallowed up into the natural number game, basically.

[Bryan Gin-ge Chen]

Any suggestions for improvements to the current tactic docs are welcome too.

[Jalex Stark]

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]

(I mean to pose the question: if I want to contribute to tactic docs, can I do a run of indiscriminately adding examples?)

Yes, I'm very much in favor of this.

[Kevin Buzzard]

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

[Utensil Song]

Bryan Gin-ge Chen said:

Any suggestions for improvements to the current tactic docs are welcome too.

As a beginner, I have a not so great first impression of the current tactic docs, I only understand the doc of a tactic after I have a concept about what the tactic does. I'm constantly confused about:

• Direction: what does the tactic applies to? the goal, the hypotheses, or both? Which tactic should I use if I need to do the same to 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? (This is partially addressed by the tags, I'll get back to its issues later)
• What: what does the tactics do?
• Variants: are there slightly modified versions to also do xxx, yyy?
• What else: 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 tactics 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 etc.

These questions are usually addressed by searching mathlib source for examples and searching Zulip for Q&A, and most tutorials answered some of them.

[Utensil Song]

Back to the 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

I agree that tags served well for a library reference doc, but they're not exactly a best entry point for beginners to figuring things out due to these issues. Arguably, these issues might not need to be solved within mathlib doc.

[Johan Commelin]

@Utensil Song I think that's a very good summary of the current state. I strongly encourage you to at least post these as issues on github. Because here on zulip it will get lost in the sea of history.

[Johan Commelin]

Zulip is too ephemeral for deep, wise, thoughts...

[Utensil Song]

Thanks, I need to ponder on how to turn these random thoughts into an actionable issue for a bit then I'll submit an issue. I noticed the recent efforts in leanprover-community/mathlib#2489 .

[Johan Commelin]

Well, you can post an issue anyway. Half work is better than lost work.

[Johan Commelin]

You can always edit/update the issue.

[Utensil Song]

leanprover-community/mathlib#3088

[Bryan Gin-ge Chen]

@Utensil Song Thanks for writing up the issue! I think the best way to make progress on this is to pick out some specific tactics where you think the tactic doc entry is poor and then try to rewrite it in a PR or give some concrete suggestions on Zulip or in a Github issue. Also, feel free to chime in on PRs on mathlib if you think the documentation can be improved.

[Utensil Song]

Patrick Massot said:

The link to my cheat sheet is https://www.imo.universite-paris-saclay.fr/~pmassot/enseignement/math114/tactiques.pdf but this is very specific. It refers to a very specific teaching context, it even contains one tactic that is not in mathlib.

@Patrick Massot Thanks! In order to understand it, I have translated it into English with some modifications to make it a little more clear(also removed the non-existent tactics): https://gist.github.com/utensil/dc635f2991255f76d8da797efdabbf15

(I don't know whether it's legal to translate it since it's teaching material thus might have copyright restrictions, if this is the case, I'll take it down)

[Utensil Song]

Kevin Buzzard said:

The contents of the dead link looked like this: tactic_guide.png

Also added this _Basic guide to tactics_ and _Basic tactic cheat sheet_ posted on Discord for a side-by -side comparison.

These only cover the basics (but already showing a pattern) and there're much more embedded in #mil and other tutorials (in a pedagogical way, great for a first read/try, but hard to loop up the essence later), I will keep working on the distillation.

[Utensil Song]

Just noticed Lean Quick Reference which is only for Lean 2, but still a good reference for how information can be organized together.

[Jason Orendorff]

(deleted)