Tips and tricks

Stream: general

[Yury G. Kudryashov]

Should we add a doc page with various tips and tricks? E.g.,

• use --old if you're going to edit low-level files (should we make it default?);
• temporarily hide a part of a long proof behind sorry; to speed-up recompilation (saw recently somewhere on Zulip);
• if refine times out, try convert instead and see which terms Lean fails to unify;
• use library_search etc;
• what else?

[Stuart Presnell]

If there’s a complex-looking theorem or lemma that you think will be useful, bring it into context with ‘have := lemma_name‘ (or, if you want to see all the implicit arguments, ‘have := @lemma_name’). Feed it whatever arguments it needs, or use ‘_’ as a placeholder, to narrow in on the bit that you need. This can make it easier to see how to apply the theorem in your specific case.

[Stuart Presnell]

I find this to be a useful approach, but it’s not something you’ll learn from reading finished code.

[Trebor Huang]

Can't-learn-it-from-finished-code sort of tricks are exactly what semi- beginners like me need, I think

[Andrew Yang]

I think #lint should be mentioned as well.

[Scott Howard]

rintro rfl probably deserves mention, and maybe a bit of explanation. I know I had a lot of trouble telling what this does in proofs at first.

[Kevin Buzzard]

That should be taught in the docstring for rintro. Tactic docstrings should have examples. @Rob Lewis am I right about this? I am about to embark on writing down a bunch of examples of tactic usage as part of preparation for my class; should I be PR'ing them to mathlib?

[Johan Commelin]

I think we could do both. The docstring and the tips and tricks file.

[Bryan Gin-ge Chen]

Rob gave some thoughts on making tactic docs / docstrings more helpful in #3088.

[Scott Howard]

Ah, I missed it completely---it's in the docstring for rcases, which is referred to by rintro's docstring.

[Kevin Buzzard]

Right, but the fact that you missed it means that things can be better

[Rob Lewis]

I'm glad Brian beat me to the punch, I was going to link that same issue! Yes, if I had my way every tactic doc would have a standard structure with an ## Example usage section that exhaustively showed all the features. Definitely PR anything you write

[Kevin Buzzard]

Excellent. I'd not seen this issue before!

[Arthur Paulino]

I don't remember who taught me this, but #exit is super useful when working in the beginning of a large file that you don't want to be recompiled everytime you change a letter

[Rob Lewis]

Another tip I tell my students is how to restart the Lean server if things go haywire, and to bind a hotkey to do it if they find it happening a lot

[Stuart Presnell]

I've found it useful to set a keyboard shortcut in VS Code (I'm using Shift-Alt-N) to switch to checking nothing so I can quickly interrupt Lean if it starts sweating

[Yaël Dillies]

Arthur Paulino said:

I don't remember who taught me this, but #exit is super useful when working in the beginning of a large file that you don't want to be recompiled everytime you change a letter

And . for the similar but before the place you're touching.

[Yury G. Kudryashov]

There is an option "Check visible lines"

[Yury G. Kudryashov]

Another workflow tip: if you work on some large contribution, then it might be a good idea to start creating PRs with supporting lemmas before the main feature is ready (create new branch, cherry-pick parts of the diff, push, PR). In Emacs I use magit's d r main-feature-branch-name, then press v on the hunks I want to see in the new branch. Probably, VS code has similar functionality (built-in or in a plug-in).

[Stuart Presnell]

Use library_search, as Yury mentioned, but also simp? and tidy? to suggest lemmas that can make progress.

[Stuart Presnell]

And also: if at first library_search can't find a solution, do as much as you can to help it. For example, if you have x = y somewhere in your goal but you have h : y = x in context, try rewriting h to make it better match your goal. Similarly, if you have P ∧ Q in context and you think one of P or Q will be useful, make sure to break apart the conjunction. In general, library_search is good at searching the library but don't expect it to be clever beyond that one job.

[Alex J. Best]

I made a start on this and PR'd at https://github.com/leanprover-community/leanprover-community.github.io/pull/240, please suggest things to add, there or here.
So far I tried to stick to things that aren't mentioned in too many other places. So I avoided specific tactic syntax, those certainly are useful and some of those are hard to find, but I wanted to avoid overlap with the tactic doc and duplicate info, maybe we could add some links to "most useful development tactics you won't see in finished code" ?

[Yaël Dillies]

I have a trick, but I don't know whether it qualifies. If you have a lemma involving multiplication which doesn't dualize (in the order sense, most likely because you need ordered_semiring or stronger), it very often means you're missing a more general statement which does.

The way to get to that new statement is to replace multiplication by scalar multiplication. The idea is that your original statement had too many order assumptions which prevented it from dualizing, and scalar multiplication decouples them in the right way.

[Yaël Dillies]

Signs that a theorem is eligible for such generalization:

• You never use commutativity of multiplication (very strong sign!)
• You only consider binary products, or at worse a bounded number of them.
• It has a "summing part" and a "multiplication part"
• The ordered type you're using also has another role in the statement
• The ordered type you're using is concrete

[Yaël Dillies]

I applied this reasoning to

• The rearrangement inequality (#10861)
• Incidence algebras (branch#incidence_algebra)
• Convex functions (docs#convex_on.convex_le for example)
• Scalar multiplication of sets of reals (file#data/real/pointwise)

[Yury G. Kudryashov]

Sometimes you can also generalize from, e.g., λ x, x + a to "any monotone function".

[Yury G. Kudryashov]

Some proofs about translation numbers generalize from "a monotone map such that f (x + 1) = f x + 1" to "two monotone maps that commute".

[Filippo A. E. Nuccio]

Arthur Paulino said:

I don't remember who taught me this, but #exit is super useful when working in the beginning of a large file that you don't want to be recompiled everytime you change a letter

@Arthur Paulino : can you explain exactly how this works?

[Filippo A. E. Nuccio]

Stuart Presnell said:

I've found it useful to set a keyboard shortcut in VS Code (I'm using Shift-Alt-N) to switch to checking nothing so I can quickly interrupt Lean if it starts sweating

Seems useful, can you expand a bit on how to do this?

[Yakov Pechersky]

Every time you change a file, everything in that file below what you wrote (by default lean3 extension to VSCode) is recompiled. By writing #exit, you are telling Lean that "ignore the rest of this file". So you don't have to spend CPU on recompiling things below. You can delete that #exit once you're done.

[Arthur Paulino]

@Filippo A. E. Nuccio Suppose you're working on a 1000 lines long file, but you're tweaking a lemma that's declared in the 30th line. if you place #exit right after that lemma, you can play with it without demanding lean to compile everything else

[Stuart Presnell]

So writing #exit is equivalent to commenting out the remainder of the file.

[Yakov Pechersky]

Not exactly.

[Yakov Pechersky]

section foo

-- nothing

[Yakov Pechersky]

That has an error

[Filippo A. E. Nuccio]

Great, thanks -- I did not know! And is there a way to tell Lean not to restart the whole library from scratch? It sometimes happen to me to open a very deep file and to try a #where to see the local variables. Although I don't save it, Lean starts recompiling everything, and it takes forever...

[Yakov Pechersky]

section foo

#exit

That doesn't

[Filippo A. E. Nuccio]

And what about the checking nothing? Where is it (in VSCode)?

[Arthur Paulino]

Filippo A. E. Nuccio said:

Great, thanks -- I did not know! And is there a way to tell Lean not to restart the whole library from scratch? It sometimes happen to me to open a very deep file and to try a #where to see the local variables. Although I don't save it, Lean starts recompiling everything, and it takes forever...

Once I mentioned that even adding an empty line will trigger that. I don't remember where that thread is, but some people argued that it's a hard thing to avoid

Edit: found it!

[Yakov Pechersky]

image.png
At the bottom of the window. You can also press Ctrl-Shift-P and type "Checking" to see the options.

[Yury G. Kudryashov]

With --old, Lean doesn't recompile unchanged files. If you've modified data.set.basic, then rolled back, you might need to restart Lean server.

[Filippo A. E. Nuccio]

I see, thanks; but where do you put --old?

[Alex J. Best]

Fillippo, check out the PR I linked to above! It tries to answer all these questions

[Alex J. Best]

Filippo A. E. Nuccio said:

Great, thanks -- I did not know! And is there a way to tell Lean not to restart the whole library from scratch? It sometimes happen to me to open a very deep file and to try a #where to see the local variables. Although I don't save it, Lean starts recompiling everything, and it takes forever...

I still find that closing the file without saving and restarting lean works best in this situation

[Filippo A. E. Nuccio]

Thanks - and thanks also for starting the PR. I don't know if it counts here, but I often find it useful to temporarily use

have  :=  lemma_foo

to see in the infoview what the lemma lemma_foo needs as a variable (be it a thing, like a number, or an assumption) and to gradually construct the matching objects. Then I revert everything to an exact, or even term mode.

[Stuart Presnell]

Filippo A. E. Nuccio said:

And what about the checking nothing? Where is it (in VSCode)?

In VS Code on MacOS, Code > Preferences > Keyboard Shortcuts opens a window listing all the possible keyboard shortcuts, and then searching in this page for check lets you set a keybinding for Lean: Check Nothing.

[Filippo A. E. Nuccio]

Found, thanks!

[Stuart Presnell]

Yes, I mentioned introducing lemmas with have := ... earlier in the thread. I use it so often that I'm now unable to type have : without automatically following it with =, which leads me to confusion quite frequently!

[Filippo A. E. Nuccio]

Same here!

[Filippo A. E. Nuccio]

I would certainly insert a small section containing an explication of the use of $ to "avoir parenthesis" (I confess I am still unable to fully grasp how it works - I use it as a DIY tool but I would like to have nice instructions)

[Alex J. Best]

I added a bit about the $ sign to that PR, if you have any feedback on it that would be very helpful :smile:.

[Filippo A. E. Nuccio]

Thanks Alex! I have a couple of comments:
1) The first sentence sounds odd to me : starting with "As Lean..." , I would expect a comma and then to see a conclusion, but that is missing;
2) Also, between the two codes, the bit "can lead to annoying to find errors" sounds weird to me.
3) Towards the end, you write "as this function is in the or namespace." but I would put or in code-style, or something like that.

The whole text is very neat, thanks! I just have one question about your example with

some_function (a $..applications) another_argument

would it work as

some_function $ a $..applications another_argument

?

The final bit concerning the dot notation is very nice; I would also add that many things can fall under this pattern; for instance, the fact that a lemma whose statement is

lemma foo (assumptions) : continuous f :=

can be inserted in another lemma called continuous.bleah in the form of foo.bleah: ideally, finding a true example in the library (I can have a look if you want) would be even more useful, since this foo-bleah idiom sounds a bit strange to mathematicians who are not used to CS-jargon (I think, or at least this was my experience). What might be worth writing out explicitly is that a name like continuous.add is not like cotinuous_add; the "dot-notation" is "interactive", and if one has always done Math on books this looks like crazy/magic!

[Yury G. Kudryashov]

a $ b $ c $ d parses as a (b (c d))

[Alex J. Best]

I've added a continuous example!

[Alex J. Best]

And clarified that some_function $ a $..applications another_argument wouldn't work, as applications eats another_argument then. And I fixed all the comments, thanks!

[Filippo A. E. Nuccio]

Thanks!

[Julian Berman]

Is it worth mentioning "learn the naming convention for lemmas" as a tip and linking to that page?

[Yury G. Kudryashov]

a $ (b $ c d) e a (b $ c d) e parses as a (b (c d)) e
a $ (b $ c d) e parses as a (b (c d) e)

[Alex J. Best]

What do you mean?
The first check here fails

constant T : Type*
constant a : T → T → T
constant b : T → T
constant c : T → T
constant d : T
constant e : T
#check a $ (b $ c d) e
#check a (b (c d)) e

[Yury G. Kudryashov]

Fixed (I hope, not tested)

[Alex J. Best]

:ping_pong: does anyone with push access to leanprover-community/leanprover-community.github.io want to review leanprover-community/leanprover-community.github.io#240 :smile:?

[Arthur Paulino]

Does using variables ... count as a tip/trick?
(as opposed to repeating such parameters over and over)

[Riccardo Brasca]

LGTM!

[Alex J. Best]

I was thinking of this more as a place to put tips that are hard to find/explain elsewhere so as to not make it too long and overload the reader. My (personal) feeling is that the use of variables is covered in other more introductory material linked to on the site, though maybe could be emphasised more in the style guide perhaps.
I don't mind being out-voted on this though if others feel this list should be more comprehensive. I haven't added everything we talked about in this thread for basically this reason, not wanting to duplicate the tactic list, glossary etc

[Arthur Paulino]

No, I agree with you @Alex J. Best

[Filippo A. E. Nuccio]

Two things that might be added are the use of # where if one is willing to use a result in some namespace but it is not clear where the result is. The second I am thinking of is the way import works (in relation with the first point): in particular, the fact that even if a file has been imported but the relevant namespace has not been opened, there will be problems.

[Alex Ellis]

hello! I'm new to lean and to computer assisted proofs. if I'm interested in the theorem proving+verifying more than in programming with lean, which version should I play with? from the little reading I've done, it looks like lean{2,3,4} are mutually incompatible (though correct me if I'm wrong)

[Matthew Ballard]

What is your background? What do you want to prove/verify?

[Alex Ellis]

my background: used to me a mathematician (rep theory, higher categories, and applications to low dim topology). now I work in tech, mostly ML. there's nothing in particular I want to prove! just exploring curiously. once I learn more, I'd be interested in contributing to formalization projects, but I don't know much about what's going on in the lean community

[Matthew Ballard]

Lean 3 currently has a developed pure mathematics library - mathlib.

[Bryan Gin-ge Chen]

Until mathlib has been ported over to Lean 4 (which should hopefully happen within the next year or so), I'd recommend starting with Lean 3. The community website has a bunch of learning resources here: https://leanprover-community.github.io/learn.html

[Matthew Ballard]

Unless you want to roll your own "basic" theorems and proofs, then I would suggest starting there

[Alex Ellis]

thanks! yes, matlib is what I've been playing with so far. good to know there are plans to port it to lean4. I'm curious—what's the reason lean is choosing to have non-backwards-compatible releases?

[Matthew Ballard]

Greater functionality

[Matthew Ballard]

Unlike most programming languages where the terrain is pretty well-trodden, a lot is learned here with trial and error.

[Bryan Gin-ge Chen]

As the Lean 4 FAQ puts it "Lean is under heavy development, and we are constantly trying new ideas and tweaking the system. It is a research project and not a product."

[Matthew Ballard]

It also has more a section on significant changes from Lean 3 to Lean 4.

[Eric Wieser]

The best time to make a backwards incompatible release is when your userbase is small, and your core users (here mathlib contributors) are willing to put up with the incompatibility. Lean has the luxury of being in that position unlike many other languages.

[Matthew Ballard]

Personally, I think the benefits derived from the breaking changes will significantly outweigh the hassles. For example, program extraction + proofs is :fire: for me.

[Matthew Ballard]

I think the majority of the current user base feels similarly generally.

[Notification Bot]

15 messages were moved from this topic to #new members > Which version of Lean? by Rob Lewis.