Lean4 cheatsheet

Stream: Lean for teaching

[Elisabeth Bonnevier]

I will be giving an intro to Lean4 at the mathematics department of my university this week. Has anyone made a cheatsheet of tactics for Lean4? I think it would be nice for the participants to have one while we are formalising.

[Martin Dvořák]

I have a cheatsheet, but it is useful only if you already know Lean 3 tactics:
https://github.com/madvorak/lean3-tactic-lean4

[Martin Dvořák]

You would probably like to have something like "if the goal looks like ABC, you can try XYZ", right?

[Elisabeth Bonnevier]

Martin Dvořák said:

You would probably like to have something like "if the goal looks like ABC, you can try XYZ", right?

Yes, preferrably

[Martin Dvořák]

I can create a draft, but someone else would have to polish it.

[Elisabeth Bonnevier]

I found this: https://leanprover-community.github.io//img/lean-tactics.pdf but it is for Lean 3 right?

[Elisabeth Bonnevier]

Martin Dvořák said:

I can create a draft, but someone else would have to polish it.

That would be awesome!

[Martin Dvořák]

Elisabeth Bonnevier said:

I found this: https://leanprover-community.github.io//img/lean-tactics.pdf but it is for Lean 3 right?

Yes.

[Patrick Massot]

Oh, this is an English version of my old teaching cheatsheet!

[Martin Dvořák]

Can you provide a .tex file of that document?

[Patrick Massot]

https://github.com/leanprover-community/lftcm2020/blob/master/lean-tactics.tex

[Martin Dvořák]

Patrick Massot said:

https://github.com/leanprover-community/lftcm2020/blob/master/lean-tactics.tex

Do you allow me to fork it and create a Lean 4 version?

[Patrick Massot]

Sure.

[Martin Dvořák]

Actually, does it have to be a fork, or can I simply copy the one document into a new repository I will create? In such a case, how can I acknowledge you as the original author?

[Johan Commelin]

Forking seems overkill. Just leave a comment in the TeX with some acknowledgements and a pointer to the original.

[Martin Dvořák]

Thanks!

[Johan Commelin]

My English copy doesn't even acknowledge Patrick :oops: :see_no_evil:

[Martin Dvořák]

So my copy will acknowledge you both, ok?

[Martin Dvořák]

Elisabeth Bonnevier said:

Martin Dvořák said:

I can create a draft, but someone else would have to polish it.

That would be awesome!

https://github.com/madvorak/lean4-cheatsheet/blob/main/lean-tactics.pdf

[Martin Dvořák]

Please PR any improvements you will have!
https://github.com/madvorak/lean4-cheatsheet

[Elisabeth Bonnevier]

Martin Dvořák said:

Elisabeth Bonnevier said:

Martin Dvořák said:

I can create a draft, but someone else would have to polish it.

That would be awesome!

https://github.com/madvorak/lean4-cheatsheet/blob/main/lean-tactics.pdf

This is great! Thank you so much!

[Martin Dvořák]

Will you be importing all of Mathlib4 by default? Or should I add what imports are needed for each tactic?

[Elisabeth Bonnevier]

Martin Dvořák said:

Will you be importing all of Mathlib4 by default? Or should I add what imports are needed for each tactic?

It would be nice to have which imports are needed :smile:

[Martin Dvořák]

OK, I'll add it!

[Martin Dvořák]

Done.
https://github.com/madvorak/lean4-cheatsheet/blob/main/lean-tactics.pdf
The document is not more cluttered, but hopefully still readable.

[Martin Dvořák]

PS: I also wrote import Mathlib.Tactic.Have even though a tactic have exists outside of Mathlib as well (but with a different syntax).

[Mario Carneiro]

I don't think we should be recommending people to use cases' except in porting situations

[Mario Carneiro]

there really isn't any reason to prefer it over either cases or rcases

[Mario Carneiro]

also a good portion of uses are covered also by have <a, b> := e

[Martin Dvořák]

What is the syntax of cases without additional symbol?

[Martin Dvořák]

Or should I recommend rcases there?

[Mario Carneiro]

what do you mean without additional symbol?

[Martin Dvořák]

Mario Carneiro said:

I don't think we should be recommending people to use cases' except in porting situations

It also applies to:
https://github.com/madvorak/lean3-tactic-lean4

[Martin Dvořák]

Mario Carneiro said:

what do you mean without additional symbol?

not cases' but cases

[Martin Dvořák]

Sorry for cluttering the sentence; I didn't feel like ending the backtick right before the question mark, so I added extra words.

[Mario Carneiro]

for unpacking an or it looks like:

cases e with
| inl a => ...
| inr b => ...

[Martin Dvořák]

Well, I don't want to use this syntax.

[Martin Dvořák]

So cases' and rcases are my options.

[Henrik Böving]

Why do you not want to use that syntax? It gives a more structure idea of what is happening doesn't it?

[Mario Carneiro]

rcases is closer to cases' if you like the way it looks, it just adds | between the names

[Martin Dvořák]

Henrik Böving said:

Why do you not want to use that syntax? It gives a more structure idea of what is happening doesn't it?

I am lazy to write so many lines/symbols.

[Mario Carneiro]

you can also use obtain which is the same as rcases but with a syntax closer to have

[Mario Carneiro]

obtain a | b := e

[Mario Carneiro]

Martin Dvořák said:

Henrik Böving said:

Why do you not want to use that syntax? It gives a more structure idea of what is happening doesn't it?

I am lazy to write so many lines/symbols.

Ideally there will be autocomplete thingies for this

[Mario Carneiro]

I don't think that alone is a good argument for changing preferred style guides

[Martin Dvořák]

I suppose here
https://github.com/madvorak/lean3-tactic-lean4
I will keep cases' as the other options have different syntax.

[Martin Dvořák]

On the other hand, here
https://github.com/madvorak/lean4-cheatsheet/blob/main/lean-tactics.pdf
I will change it to whatever you tell me to use instead.

[Mario Carneiro]

if you are transcribing lean 3 code then yes you should use cases', and in that case linters and the like will tell you how to fix it

[Martin Dvořák]

These two documents (repos) have different use cases. I think I don't have to keep them in sync.

[Martin Dvořák]

So just tell me which tactic is desirable for the Lean 4 Cheatsheet.

[Mario Carneiro]

I think you should recommend cases in the cheatsheet

[Mario Carneiro]

there are several alternative options, I don't know whether you want to elaborate on them on the page

[Martin Dvořák]

OK, and the whole line in the column "Appears in hypothesis" should be?

[Patrick Massot]

I think that mentioning all those imports is completely useless in such a document. You should mention only one import that bring all those tactics. This document is intended only for beginners and they shouldn't need to worry about minimal imports here.

[Martin Dvořák]

I need to describe it concisely.

[Martin Dvořák]

Patrick Massot said:

I think that mentioning all those imports is completely useless in such a document. You should mention only one import that bring all those tactics. This document is intended only for beginners and they shouldn't need to worry about minimal imports here.

@Elisabeth Bonnevier wanted to see the imports specifically.

[Mario Carneiro]

Martin Dvořák said:

OK, and the whole line in the column "Appears in hypothesis" should be?

what I posted above

cases expr with
| inl new_name => proof
| inr new_name => proof

[Mario Carneiro]

yeah, it's not one line. Some tactics are like that

[Martin Dvořák]

I see it is not one line. But for the sake of the document, I need to fit it into two lines.

[Mario Carneiro]

I think you shouldn't

[Patrick Massot]

I am pretty sure she didn't expect to have one import per tactic. Otherwise I can only tell her what I told you: this is a bad idea for beginners.

[Martin Dvořák]

Martin Dvořák said:

Will you be importing all of Mathlib4 by default? Or should I add what imports are needed for each tactic?

This is what I asked.

[Mario Carneiro]

if you try to compress the syntax for cases onto one line it will be confusing for readers to figure out how to use it correctly in multiline scenarios

[Patrick Massot]

Martin, you can use rcases for all this. I agree those Lean4-style branching tactics are much harder to explain.

[Mario Carneiro]

(It is technically legal to use cases expr with | inl new_name => proof | inr new_name => proof but this doesn't scale very well)

[Martin Dvořák]

Mario Carneiro said:

I think you shouldn't

The document is at its limit. I either have to keep cases' or change it to rcases or (in order to to allow cases as we want) I have to delete something else.

[Mario Carneiro]

cases expr with match_arms

[Martin Dvořák]

Mario Carneiro said:

cases expr with ...

OK, this goes into the document?

[Mario Carneiro]

yes

[Martin Dvořák]

What is match_arms in your edited response?

[Mario Carneiro]

another metavariable-looking thing

[Mario Carneiro]

you aren't going to be able to explain the full syntax in these constraints

[Martin Dvořák]

Martin Dvořák said:

Mario Carneiro said:

cases expr with ...

OK, this goes into the document?

Into all three occurences?

[Mario Carneiro]

for both 'and' and 'exists' you can use let <x, hx> := e

[Mario Carneiro]

or have, it doesn't really matter

[Martin Dvořák]

Or I can use rcases for all three and the syntax fits into the lines?

[Mario Carneiro]

I don't know, this seems to be mixing concerns about space in the document and best practices for tactic usage in a way that is hard to navigate

[Martin Dvořák]

Is rcases bad as a practice?

[Mario Carneiro]

I'm not a teacher. For classes you often need to specifically curate tactic lists which are optimized to keep the lexicon small

[Mario Carneiro]

rcases isn't bad, as I said there is more than one way to do it

[Martin Dvořák]

Well, since this isn't for my class, I will wait for what @Elisabeth Bonnevier prefers.

[Mario Carneiro]

but asking for one way to be the 'best' is hard, I expect that to be context dependent

[Martin Dvořák]

I can also make more branches of the repo, if more than one person is interested in having a document of this type.

[Martin Dvořák]

I will eventually also create a version in Czech (my native language) which might possibly differ in the content as well.

[Mario Carneiro]

Here are the ways to perform and elimination I can think of off the top of my head:

-- and elim
· let ⟨a, b⟩ := e
· have ⟨a, b⟩ := e
· obtain ⟨a, b⟩ := e
· rcases e with ⟨a, b⟩
· cases' e with a b
· induction' e with a b
· match e with
  | ⟨a, b⟩ => ...
· cases e with
  | intro a b => ...
· cases e
  next a b => ...
· induction e with
· | intro a b => ...
· induction e
  next a b => ...
· refine e.elim fun a b => ?_

-- and elim + intro
· fun ⟨a, b⟩ => e
· intro ⟨a, b⟩
· rintro ⟨a, b⟩

[Mario Carneiro]

interestingly, all of those examples work for exists elimination as well

[Martin Dvořák]

Some of them require more lines, right?

[Mario Carneiro]

what do you mean? As you can see some of them are two lines but none of them require more than is shown

[Martin Dvořák]

Oh sorry. I thought your claim was about or elimination. My bad!

[Mario Carneiro]

for or elimination the list is a bit different

[Kyle Miller]

Here's another for your list Mario:

cases e
next a b => ...

[Martin Dvořák]

Eliminating exists in the same way as and sounds believable.

[Mario Carneiro]

Here's the list for or elim:

-- or elim
· obtain a | b := e
· rcases e with a | b
· cases' e with a b
· induction' e with a b
· match e with
  | .inl a => ...
  | .inr b => ...
· cases e with
  | inl a => ...
  | inr b => ...
· cases e
  next a => ...
  next b => ...
· induction e with
  | inl a => ...
  | inr b => ...
· induction e
  next a => ...
  next b => ...
· refine e.elim (fun a => ?_) (fun b => ?_)

-- or elim + intro
· fun
  | .inl a => ...
  | .inr b => ...
· intro
  | .inl a => ...
  | .inr b => ...
· rintro (a | b)

[Martin Dvořák]

Nice! I saved it.

[Elisabeth Bonnevier]

Martin Dvořák said:

Will you be importing all of Mathlib4 by default? Or should I add what imports are needed for each tactic?

How do I import all of Mathlib4 by default? I only know how to import specific files with import statements at the start of the file.

[Elisabeth Bonnevier]

Martin Dvořák said:

Patrick Massot said:

I think that mentioning all those imports is completely useless in such a document. You should mention only one import that bring all those tactics. This document is intended only for beginners and they shouldn't need to worry about minimal imports here.

Elisabeth Bonnevier wanted to see the imports specifically.

If it is better to have one import that brings all, then do that :smile:

[Elisabeth Bonnevier]

Martin Dvořák said:

Well, since this isn't for my class, I will wait for what Elisabeth Bonnevier prefers.

I am an Agda user and have only learned basic Lean 4 in order to give an introduction to computer formalisation to mathematicians. So I don't know what the best tactics are. You who are more experienced with Lean should decide what would be best to recommend to beginners and I will adapt to that :smile:

[Kevin Buzzard]

You can import all of mathlib4 with import Mathlib. For my beginner mathematician students working with lean 3 I start every file with import tactic which imports essentially all the mathlib3 tactics; as far as I know there is no analogue of this yet, and perhaps there should be (I want all the tactics available to students to minimise misunderstanding but I don't necessarily want all the technical results about measure theory, functional analysis and commutative algebra to be available at all times!).

Note that import Mathlib should succeed in just a few seconds. If it doesn't then you need to type lake exe cache get into the command line, and this can be a bit flaky (you have to have a relatively recent curl for example). Lean 4 and the tools we use to play with it are still more of a project in places, rather than a finished product. This is why I still teach with lean 3 (well, that and the fact that I need all of the maths library because I'm doing more advanced mathematics with final year students, and only 40% of the maths library is ported to lean 4 right now)

[Martin Dvořák]

After you decide @Elisabeth Bonnevier tell me how you want me to change the document.
(1) Keep or remove the imports?
(2) Keep cases' or change it to cases or to rcases (I personally prefer the latter)?

[Elisabeth Bonnevier]

Martin Dvořák said:

After you decide Elisabeth Bonnevier tell me how you want me to change the document.
(1) Keep or remove the imports?
(2) Keep cases' or change it to cases or to rcases (I personally prefer the latter)?

Okay, if it's up to me, I would:
(1) keep the information about where the tactics are imported from
(2) use cases (that's what I've been using so far)

[Martin Dvořák]

https://github.com/madvorak/lean4-cheatsheet/blob/main/lean-tactics.pdf

[Martin Dvořák]

For the sake of consistency, wouldn't it be better to write the following?

have new_name : expr

[Martin Dvořák]

Kevin Buzzard said:

as far as I know there is no analogue of this yet, and perhaps there should be

Maybe we should make a file like https://github.com/leanprover-community/mathport/blob/e898d4a1467fae2a9941c37081d8fff5041d617c/Mathport/Syntax/Translate/Tactic/Mathlib.lean but for actual Lean 4 / Std4 / Mathlib4 tactics.

[Martin Dvořák]

Now that we have covered @Elisabeth Bonnevier 's use case, what do yall want me to change in the document so it will be useful for other teachers/users?

[Martin Dvořák]

What do you want me to change in
https://github.com/madvorak/lean4-cheatsheet/blob/main/lean-tactics.pdf
for better usability in other courses or groups?

[Martin Dvořák]

I should probably remove the imports. Anything else?

[Flo (Florent Schaffhauser)]

@Martin Dvořák I like that you have put the imports: this type of information is not easy to find when you start, so it is useful to have it here, at least in my view (even if you don't need it, you will wonder about it). Thanks for putting the cheatsheet together :+1:

[Martin Dvořák]

@Alex J. Best noticed an important problem: simp is missing in the cheatsheet.
I will add it, of course.
However, the cheatsheet is getting too long.
I suggest we should remove a few tactics, too.
My candidates for removal are apply? because it has never ever helped me (but other people say it is useful, so I am confused) and exfalso because students can use by_contra instead (I already removed contrapose for similar reasons).
What do you think?

[Alex J. Best]

As I said in the other thread while I like convert_to I don't think it belongs on a cheatsheet one page long necessarily

[Damiano Testa]

My personal experience: when learning Lean, I never used convert_to, while I hoped a lot to get help using library_search. For this reason, I would remove convert_to before exact?/apply?. It might be reasonable to join the two in the same entry, though.

As for exfalso, I found it very useful as a beginner.

[Alex J. Best]

Having rw appear twice seems a bit excessive to me also . Especially as in lean 4 the brackets are not optional so the syntax should already be quite reminiscent of a list

[Alex J. Best]

rw and simp can do the job of unfold most of the time so I'm not sure that needs to be there either

[Martin Dvořák]

I love exfalso because it documents the intention very well (and it is also a very cool name).
I love convert_to for it saved my ass so many times.
I agree that simp is a must.
I am quite unsure about one rw versus more of them.
About removing unfold I am quite worried (sure, we teach them simp but not dsimp only or what they would need to do the unfolding only).

[Eric Rodriguez]

unfold I think should go

[Eric Rodriguez]

I would maybe merge exact?/apply? and maybe even rw? together

[Jireh Loreaux]

Of course gcongr should be present, and aesop.

[Martin Dvořák]

Jireh Loreaux said:

Of course gcongr should be present, and aesop.

I'll first have to learn myself how to use these tactics! I am adding it to my TODO list.

[Martin Dvořák]

Alex J. Best said:

Having rw appear twice seems a bit excessive to me also . Especially as in lean 4 the brackets are not optional so the syntax should already be quite reminiscent of a list

Would you keep the first rw entry only?

[Martin Dvořák]

Alex J. Best said:

As I said in the other thread while I like convert_to I don't think it belongs on a cheatsheet one page long necessarily

I am a bit worried that if I show only convert then students might think that convert has the effect of convert_to instead.
The comparison makes you kinda understand both tactics, I believe.

[Damiano Testa]

I'm still not completely sold on the "one page only" restriction.

[Eric Rodriguez]

You could do one page for the basic stuff, and then two pages with extra stuff

[Martin Dvořák]

I can make a markdown version that is not restricted by the page (A4) size, which can contain more tactics than the LaTeX version (pdf). Still, I believe that for the document to be useful as a cheatsheet, it shouldn't contain much more stuff than it already does.

[Frédéric Dupuis]

I think refine should be there as well, I find this tactic very undertaught given how useful it is.

[Floris van Doorn]

I've also never used convert_to. Are all these tactics available in Mathlib.Tactic.Core? If so, I would just write that (once).

[Antoine Chambert-Loir]

In some contexts, apply? is very efficient.

[Antoine Chambert-Loir]

Maybe, tactics could be grouped according to how they are used.
simp, rw, are close, and so are apply, refine, convert...

[Martin Dvořák]

Antoine Chambert-Loir said:

In some contexts, apply? is very efficient.

Can you please give me an example? I have never benefited from what apply? gave me.

I don't doubt your claim. I just want to understand where or when apply? is useful.

[Alex J. Best]

I would say https://github.com/alexjbest/lorentz/blob/master/Lorentz/MondayDemo.lean#L70 is a situation where iterating apply? is the easiest way to construct the proof (ok the continuity tactic also exists, but in some similar situation where there is no existing tactic apply? is a life saver when you don't know the names of all the lemmas by heart)

[Martin Dvořák]

The first two steps were good!
Subsequently, I couldn't persuade apply? to give me Continuous.comp continuous_sin.
Should I introduce a different intermediate goal in order to get there?
I tried the following but failed...

The goal is:

Continuous fun b => sin (b ^ 2)

I introduced a simpler goal, for which exact? succeeded:

have : Continuous fun x => sin x
· exact continuous_sin

Unfortunately, I cannot extrapolate from this to the original goal. If I simple write

apply continuous_sin

as the next step, it fails. How did you obtain a hint towards

apply Continuous.comp continuous_sin

in your proof?

[Alex J. Best]

I just did it again and indeed it likes Continuous.comp' more, I ended up with

  refine Continuous.add ?hf ?hg
  refine Continuous.pow ?hf.h 3
  refine Continuous.comp' ?hf.h.hg ?hf.h.hf
  exact continuous_sin
  exact continuous_pow 2
  refine Continuous.comp' ?hg.hg ?hg.hf
  exact continuous_cos
  exact continuous_mul_left 5

[Alex J. Best]

The proof I wrote was hand written (note it uses apply not refine) but the tactic gets roughly the same proof

[Martin Dvořák]

Unfortunately Continuous.comp' is pretty low in the output and it doesn't strike me as useful when reading only its name.

[Patrick Massot]

You should also read that remaining goals, that' s by far the most important piece of information.

[Patrick Massot]

Note also the case of continuity goals is pretty special because there are so many lemmas whose conclusion is a continuity statement and which potentially apply everywhere. For instance, in the case of continuous functions between metric spaces, apply? will always suggest to prove the function is uniformly continuous, or prove it is sequentially continuous, or prove it is continuous at every point, etc. It would be nice if apply? could have heuristic to push these down the list, but this isn' t so obvious (but you can still hope @Scott Morrison will prove me wrong).

[Alex J. Best]

Martin Dvořák said:

Unfortunately Continuous.comp' is pretty low in the output and it doesn't strike me as useful when reading only its name.

Its certainly true that the ordering could be improved! but that is a nontrivial problem, as it verges on automated theorem proving :wink: a good algorithm for ordering that always puts what your next step will be at the top very quickly leads to a decent auto proof tactic

[Alex J. Best]

Thats not to say we shouldn't improve it with good heuristics, I'd still think there is some low hanging fruit there

[Kevin Buzzard]

How about ordering by some measure of "total number of characters in all remaining goals" for a start?

[Martin Dvořák]

It took me pretty long to realize that Continuous.comp' was about function composition.
Clearly, I'm the problem here.

[Antoine Chambert-Loir]

Martin Dvořák said:

Antoine Chambert-Loir said:

In some contexts, apply? is very efficient.

Can you please give me an example? I have never benefited from what apply? gave me.

I don't doubt your claim. I just want to understand where or when apply? is useful.

Working about permutations, their cycle types, their support, etc there are many equivalent ways of passing from one formulation to another, equivalences which mathlib knows and — at least I felt it so — finds by itself.

[Martin Dvořák]

I'm getting a feeling that you guys use apply? in situations where I use convert_to followed by exact? usually.
I think that, if you have the proof idea already in your head, convert_to leads to a pretty consistent workflow.
However, I am willing to believe that apply? is easier for most Lean users.

[Alex J. Best]

Kevin Buzzard said:

How about ordering by some measure of "total number of characters in all remaining goals" for a start?

Won't that just put False.elim at the top every time or something like that?

[Patrick Massot]

Yes, that's part of why this question isn't easy.

[Miguel Marco]

Maybe it is because I am too used to lean3, but I don't use the syntax

cases expr with
| intro a b => ...

in lean4.

Instead, I use the cases' tactic, which works like the casesone did in lean3.

[Martin Dvořák]

I was using cases' until very recently, too.
However, with the new quick-fix lightbulb in the VS Code lean4 plugin, I find cases easy to use.
Now I like cases better.

[Kevin Buzzard]

Yeah the lightbulb was crucial for me too

[Martin Dvořák]

Martin Dvořák said:

I can make a markdown version that is not restricted by the page (A4) size, which can contain more tactics than the LaTeX version (pdf). Still, I believe that for the document to be useful as a cheatsheet, it shouldn't contain much more stuff than it already does.

I started turning the original table into a markdown version:
https://github.com/madvorak/lean4-tactics/tree/main
Unfortunately, GitHub alternates row background between white and gray.
The latter makes the boundary between code and text hard to see.
Can I set the background of all rows to white?
If not, does it make sense to do it (the longer version of the cheatsheet) as a markdown document on GitHub?

[Damiano Testa]

I think that it does make sense to have the md version. I use dark mode, and I can barely notice the parity difference in cell coloring, but the code still stands out.

Also, I think that avoiding the parity with markdown may not be possible. If you really wanted, you might write the html equivalent and that may not get autoformatted, but I am not even sure about that.

[Martin Dvořák]

It looks OK in the dark mode (both the high-contrast version and the normal one).
Do you recommend that I continue with the formatting I started with?

[Damiano Testa]

Martin, if you are happy to go on with the webpage, I will certainly link it from the webpage for my module! I already have a link to your cheatsheet!

[Martin Dvořák]

Imma finish the markdown version in a few days.
Today, I was using to spend some time when Mathlib was building.

[Julian Berman]

Martin Dvořák said:

Can I set the background of all rows to white?

(You cannot FWIW, at least not while using GitHub Markdown syntax for it and not pure HTML -- but if you're satanic you can hack around it by inserting empty rows in your table -- i.e. https://gist.github.com/Julian/1e06883d37d0448685f3cf8417469e0a

[Martin Dvořák]

Haha, nice! And it works even better without the <tr></tr> at the very end.

[Martin Dvořák]

Damiano Testa said:

Martin, if you are happy to go on with the webpage, I will certainly link it from the webpage for my module! I already have a link to your cheatsheet!

My part is done. Link here:
https://github.com/madvorak/lean4-tactics

There are four rows with TODOs now.
They correspond to tactics that I don't personally use, but people wanted them in the cheatsheet.
Somebody will certainly fill them in.

[Antoine Chambert-Loir]

This page will be very useful (has already been).
Some minor comments :

• for some tactics, such as rw, the (at expr) indication suggest that parentheses have to be inserted, and it seems to be the part “in parentheses” which is optional, while the part “in brackets” has to be there!

• sometimes expr means one name, sometimes it means a list.

• I wouldn't insist on new_name: it can be an already used name, although that makes the preceding uses of that name unusable.

• simp? is useful, and almost unavoidable if one wishes not to leave bare simp commands in Lean code.

[Martin Dvořák]

Thanks a lot for noticing that parentheses vs brackets were messed up!!

I updated the document according to your suggestions (but new_name stayed there).

[Martin Dvořák]

@Patrick Massot
@Johan Commelin
@Kevin Buzzard
Do you [any subset of you] want credits for creating the previous-previous document? If so, in which form?

[Patrick Massot]

I think the correct action is to make this into a community owned resource, without attribution.

[Martin Dvořák]

Should it be written in the (Un)license file?

[Patrick Massot]

I think it should simply be put on the community website.

[Martin Dvořák]

Patrick Massot said:

I think it should simply be put on the community website.

If you are the community website maintainer, feel free to fork it or hardcopy it to the community website; after all, I unlicensed the document.

Nevertheless, I will keep the original version on my GitHub (in case that I don't like new redesigns, I will simply keep distributing my version to my students).

[Patrick Massot]

Of course you can distribute whatever you want to your students.

[Martin Dvořák]

Also this table
https://github.com/madvorak/lean3-tactic-lean4
could be hardcopied into
https://github.com/leanprover-community/mathlib4/wiki/Lean-4-survival-guide-for-Lean-3-users
(Lean 4 survival guide for Lean 3 users).

[Somo S.]

Martin Dvořák said:

Also this table
https://github.com/madvorak/lean3-tactic-lean4
could be hardcopied into
https://github.com/leanprover-community/mathlib4/wiki/Lean-4-survival-guide-for-Lean-3-users
(Lean 4 survival guide for Lean 3 users).

If there is a more general community article that is something like "Lean 4 survival guide for Lean 3 users", then that would be a more appropriate place. Otherwise new people like me who never got to use lean3 and generally avoid guides that assume I used lean3 before, would never stumble on such a useful cheatsheet.

[Martin Dvořák]

If you never used Lean 3, then https://github.com/madvorak/lean3-tactic-lean4 is not for you.

[Somo S.]

oh sorry, my fault .. should have read the discussion more carefully.. i though that was a link to your tactic cheatsheet .. which i found very useful despite not having learned lean3

[Somo S.]

speaking of which anyway, is the tactic cheatsheet going to be published somewhere on the Community website?

[Martin Dvořák]

Somo S. said:

oh sorry, my fault .. should have read the discussion more carefully.. i though that was a link to your tactic cheatsheet .. which i found very useful despite not having learned lean3

Yeah, I have been maintaining more than one sheet. Different users have different needs.

[Martin Dvořák]

Somo S. said:

speaking of which anyway, is the tactic cheatsheet going to be published somewhere on the Community website?

I think so; @Patrick Massot is in favor of putting it there.

[Patrick Massot]

Yes, I didn't have time for that yet, but anyone can open a PR to the website repository.

[Floris van Doorn]

There were some design decisions that I didn't like in Martin's cheat sheet, so I made my own for my Lean course: https://github.com/fpvandoorn/LeanCourse23/blob/master/lean-tactics.pdf
Martin's version was of course very helpful to get started.

Some changes:

• don't give import suggestions (except for a "please import Mathlib.Tactic" at the top)
• prefer rcases over cases
• simplify the syntax by suggesting names of hypotheses and removing parentheses
• different selection of tactics
• give more variants of tactics

[Martin Dvořák]

I like your version! It looks very clean and clear.

[Scott Morrison]

@David Thrane Christiansen just making sure you've seen this. No action necessary. :-)

[Scott Morrison]

Relatedly Terry Tao has just recently made his own cheatsheet at https://docs.google.com/spreadsheets/d/1Gsn5al4hlpNc_xKoXdU6XGmMyLiX4q-LFesFVsMlANo/edit#gid=0

[Utensil Song]

Tao's version is well organized, it can even support a simple tactic possibly named hint with an optional query to match goal/selected hypotheses and optional fuzzy matching the "mathematical English".

[Scott Morrison]

It's a pity we never ported hint from mathlib3. I liked it!

[Utensil Song]

Simple, extensible and helpful, like a triage for tactics

[Scott Morrison]

I'm hoping std4#215 will eventually be merged. It is a great common UI for suggestion tactics.

[Mac Malone]

I really like how Tao named the notion of terms used in proofs as "reasons" (e.g. for exact and have).

[Somo S.]

@Floris van Doorn said:

There were some design decisions that I didn't like in Martin's cheat sheet, so I made my own for my Lean course: https://github.com/fpvandoorn/LeanCourse23/blob/master/lean-tactics.pdf
Martin's version was of course very helpful to get started.

Some changes:

• don't give import suggestions (except for a "please import Mathlib.Tactic" at the top)

nice, though personally, i would prefer to know exactly where Mathlib.Tactic or Std.Tactic is required ahead of time. I think maybe it would be better if you indicated that with a less noisy annotation at the end of each description wherever that applies e.g. "This tactic does xyz[1]" (where [1] is a footnote at the bottom that says "requires Std.Tactic").

Alternatively, there could there could be a hyperlink to the definition of such a tactic, by following that link one could know ahead of time, if they need to import extra things

[Utensil Song]

"don't give import suggestions" helps to reduce visual noise for a cheat sheet, a general tip can be given at the top or in footnote to find where the tactic is, either by hover and click into the definition, or look for the name under Mathlib.Tactic source or doc.

Just as @Somo S. suggested, one might need to know if a tactic can be used without Mathlib (maybe for minimal deps in teaching), a small icon with hyperlink (to its definition in Mathlib or Std/Lean) might suffice for this purpose. But I'm afraid there are many subtle differences between the tactics with and without Mathlib, which might create more confusion as opposed to the intention of simplifying things, so one is better just get familiarized with the Mathlib flavor.

[Somo S.]

anyway, I think what can only end up ultimately emerging, is different kinds of cheatsheets for different kinds of usecases or pedagogies. In my work, I find it important to try to avoid mathlib or std wherever its not necessary or to favor clarity (of what lean is doing) over brevity.

[Johan Commelin]

I think that a "please import Mathlib.Tactic" is totally fine for a cheatsheet for beginners. I understand that other use cases are perfectly valid, but I wouldn't clutter a cheat sheet for maths students such info.

[Martin Dvořák]

import Mathlib.Tactic is totally fine for a cheatsheet for beginners

... assuming lake exe cache get works on their computer!

[Kevin Buzzard]

If lake exe cache get doesn't work on someone's computer then they should stop what they're doing and get it working, not read a tactic cheatsheet

[Mario Carneiro]

agreed, lake exe cache get not working is similar to getting the unknown package 'Mathlib' error: you should debug the issue because you don't yet have a working install

[Mario Carneiro]

We should have a troubleshooting page for common installation issues but it would be weird to have such information in a tactic cheatsheet

[Shreyas Srinivas]

I already created a PR for this

[Shreyas Srinivas]

For the trouble shooting page

[Shreyas Srinivas]

On the community website this is PR 370

[Somo S.]

@Johan Commelin said:

I wouldn't clutter a cheat sheet for maths students such info.

I thought its a general cheatsheet for anyone learning lean not just for math students? Again maybe there should be one thats for everyone or multiple that emphasize different usecases/applications.

[Johan Commelin]

The one by Floris was designed for a course for math students.

[Martin Dvořák]

Can somebody (who understands given tactics) please fill those TODOs?
https://github.com/madvorak/lean4-tactics
After that, the cheatsheet should be ready to go to the Lean community website.

[Floris van Doorn]

Most of them have an explanation here: https://github.com/fpvandoorn/LeanCourse23/blob/master/lean-tactics.pdf

[Martin Dvořák]

Catalan version:
https://github.com/madvorak/lean4-tactics/blob/main/README-CAT.md
Czech version:
https://github.com/madvorak/lean4-tactics/blob/main/README-CZE.md