Zulip Chat Archive

Stream: new members

Topic: Lean Cheat Sheet


view this post on Zulip Utensil Song (Jun 15 2020 at 10:07):

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:

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.

view this post on Zulip Patrick Massot (Jun 15 2020 at 11:53):

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.

view this post on Zulip Patrick Massot (Jun 15 2020 at 12:04):

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

view this post on Zulip Kevin Buzzard (Jun 15 2020 at 17:47):

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

view this post on Zulip Kevin Buzzard (Jun 15 2020 at 17:48):

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

view this post on Zulip Bryan Gin-ge Chen (Jun 15 2020 at 17:51):

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

view this post on Zulip Jalex Stark (Jun 15 2020 at 18:27):

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?)

view this post on Zulip Rob Lewis (Jun 15 2020 at 18:40):

(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.

view this post on Zulip Kevin Buzzard (Jun 15 2020 at 19:05):

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

view this post on Zulip Utensil Song (Jun 16 2020 at 10:12):

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.

view this post on Zulip Utensil Song (Jun 16 2020 at 10:41):

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.

view this post on Zulip Johan Commelin (Jun 16 2020 at 12:09):

@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.

view this post on Zulip Johan Commelin (Jun 16 2020 at 12:09):

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

view this post on Zulip Utensil Song (Jun 16 2020 at 12:20):

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 .

view this post on Zulip Johan Commelin (Jun 16 2020 at 12:25):

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

view this post on Zulip Johan Commelin (Jun 16 2020 at 12:25):

You can always edit/update the issue.

view this post on Zulip Utensil Song (Jun 16 2020 at 12:44):

leanprover-community/mathlib#3088

view this post on Zulip Bryan Gin-ge Chen (Jun 16 2020 at 16:12):

@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.

view this post on Zulip Utensil Song (Jun 18 2020 at 08:30):

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)

view this post on Zulip Utensil Song (Jun 19 2020 at 01:26):

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.

view this post on Zulip Utensil Song (Jun 22 2020 at 07:40):

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

view this post on Zulip Jason Orendorff (Jul 05 2020 at 07:22):

(deleted)


Last updated: May 11 2021 at 00:31 UTC