A glimpser glimpse of Lean

Stream: general

[Patrick Massot]

Some of you may be familiar with the Glimpse of Lean repository. It tries to provide a resource for people who want to give 2 to 3 hours long tutorials for mathematicians (as opposed to week-long LftCM). It has been used in many places. But it never really delivered the initial goal of fitting in three hours while still containing actual proofs (even at first year undergrad level). Part of this failure comes from trying to install Lean or use GitPod or CodeSpaces eating up half an hour. But part of it came from spending too much time on boring stuff.

On Friday I will try again giving a two hours long tutorial (in Strasbourg). I tried to write a reboot of Glimpse of Lean that really rushes towards proving stuff about limits of sequences of real numbers. I will try to use in lean4web, on the FRO server, and I’m grateful to @Jon Eugster and @Joachim Breitner for help with this technology and the server. I want to use only two files: the old introduction file with no exercise and one file with exercises. It’s probably still too long, because it requires a lot of tactics. I’d be interested in any input if someone has the patience to try to follow this (both beginners and advanced users feedback could be very useful).

The instructions are in the project README, but it really boils down to two links:

• the introduction file
• the explanations and exercises file

[Patrick Massot]

Note that this short track of Glimpse of Lean makes some unidiomatic choices to limit to amount of tactics. It does not explain rw for equalities (using congr and gcongr everywhere), and it uses apply instead of exact for instance. I’m open to ideas to avoid this, but the tutorial already cover a dozen tactics, which is more than I initially wanted.

[Patrick Massot]

Let me ping @Floris van Doorn and @Rémy Degenne since I’m sure they used Glimpse of Lean before (note the previous longer version still exists).

[Johan Commelin]

Very nice! I created two PRs with some very tiny suggestions. Feel free to incorporate/discard as you like.

[Daniel Weber]

A minor comment - looking at the definitions, I note that some definitions (seq_limit both in the introduction and the exercises and continuous_at in the introduction) have their return type Prop specified, while the rest of the definitions have it omitted. Perhaps it would be clearer to have it omitted in all places?

[Daniel Weber]

Would it be possible to disable ring attempting ring_nf in the exercises file? I can imagine someone trying ring in an unrelated location and being confused by the output

[Daniel Weber]

Regarding the ordering, wouldn't the implication convergent -> Cauchy make more sense before the subsequence section?

[Daniel Weber]

You could avoid the tactic constructor by introducing the lemma And.intro instead, but I'm not sure if this is better

[Daniel Weber]

I think the example in line 432 might be a bit intimidating at first year undergrad level, and as the particulars there are inconsequential perhaps it could be replaced with something more basic?

[Patrick Massot]

Thanks a lot Johan and Daniel!

[Patrick Massot]

Daniel Weber said:

Would it be possible to disable ring attempting ring_nf in the exercises file? I can imagine someone trying ring in an unrelated location and being confused by the output

Yeah, I wondered about that one. I really wanted to keep vanilla tactics, but ring is so annoying with ring_nf…

[Patrick Massot]

In Verbose Lean I have

/-- The non-annoying ring tactic which does not pester users with `"Try this: ring_nf"`. -/
macro (name := ring) "na_ring" : tactic =>
  `(tactic| first | ring1 | ring_nf)

[Patrick Massot]

Daniel Weber said:

I think the example in line 432 might be a bit intimidating at first year undergrad level, and as the particulars there are inconsequential perhaps it could be replaced with something more basic?

This file is really not meant for undergrads. I’m using super elementary math to make sure any mathematician has no trouble at all with the math content but still feels there is some math content (as opposed to pure logic). Again it is mostly meant for the cases where some math department asks me to give a two or three hours long introduction to Lean. That being said, there is no reason to actively prevent other people from using this file, so I’m open to specific suggestions here. I was looking for something that is clearly an actual mathematical result rather then something like a < b → a ≤ b.

[Floris van Doorn]

Patrick Massot said:

In Verbose Lean I have

/-- The non-annoying ring tactic which does not pester users with `"Try this: ring_nf"`. -/
macro (name := ring) "na_ring" : tactic =>
  `(tactic| first | ring1 | ring_nf)

Yes, I'm also using this for my teaching material.

Maybe we should change ring so that it only gives the warning when the option linter.ring_nf_warning is true, and this linter is true in Mathlib but false by default in other projects?

[Floris van Doorn]

I think the new shorter introduction file is nice! My experience with Glimpse in Lean is that basically everyone only does the basic logic exercises, and doesn't get further (except if they continue by themselves after the tutorial). So condensing the logic part down even further, and then doing some reasoning about limits seems really nice.

[Daniel Weber]

Patrick Massot said:

This file is really not meant for undergrads. I’m using super elementary math to make sure any mathematician has no trouble at all with the math content but still feels there is some math content (as opposed to pure logic). Again it is mostly meant for the cases where some math department asks me to give a two or three hours long introduction to Lean. That being said, there is no reason to actively prevent other people from using this file, so I’m open to specific suggestions here. I was looking for something that is clearly an actual mathematical result rather then something like a < b → a ≤ b.

Perhaps docs#Real.exists_isLUB ?

[Bhavik Mehta]

I will try using this shorter tutorial today, thank you for making it!

[Jon Eugster]

Patrick Massot said:

In Verbose Lean I have [...]

I usually even just do

import Mathlib.Tactic.Ring.RingNF

@[inherit_doc Mathlib.Tactic.RingNF.ring]
macro "ring" : tactic =>
  `(tactic| first | ring1 | ring_nf)

example : a + a = 2 * a + b := by
  ring -- no warning about `ring_nf`
  sorry

Strictly speaking not a vanilla-tactic anymore, but nobody's going to notice and they can still use ring as always. (ofc, implementing this in mathlib through Floris' suggestion would be even better)

[Patrick Massot]

Oh, I just noticed that the traditional version of Glimpse of Lean already uses that exact macro.

[Patrick Massot]

I added it to the short version lib (it should update tonight).

[Patrick Massot]

Daniel Weber said:

Patrick Massot said:

This file is really not meant for undergrads. I’m using super elementary math to make sure any mathematician has no trouble at all with the math content but still feels there is some math content (as opposed to pure logic). Again it is mostly meant for the cases where some math department asks me to give a two or three hours long introduction to Lean. That being said, there is no reason to actively prevent other people from using this file, so I’m open to specific suggestions here. I was looking for something that is clearly an actual mathematical result rather then something like a < b → a ≤ b.

Perhaps docs#Real.exists_isLUB ?

It’s a nice idea but it requires to explain a bit too many notations.

[Patrick Massot]

I also added https://github.com/PatrickMassot/GlimpseOfLean/blob/master/tactics.pdf which covers only the tactics described in this shorter glimpse of Lean (based on https://github.com/leanprover-community/leanprover-community.github.io/blob/lean4/papers/lean-tactics.tex which was based on my old undergrad teaching tactic cheatsheet).

[Patrick Massot]

Here is a report on that experiment. As planned I used this new variant of Glimpse of Lean in Strasbourg on Friday. I’m pretty happy with the result.

I started with showing the introduction file, which took a lot more time than what I hoped for. As often happen when I show Lean in talks, I spent a huge amount of time answering question about the magical intro tactic. There is something I really don’t understand here. I have a goal which starts with ∀ ε > 0, … and even when I type two intro lines intro ε; intro hε many people find it super confusing that the tactic script does not contain the characters ε > 0.

But then the exercises went well. Most people stayed for two hours and a half and reached the intended goal of proving something about sequences (many participants were proving the squeeze theorem). And they seemed happy.

[Patrick Massot]

It’s hard to assess whether lean4web behaved nicely because the wifi connection was very bad. But I am super happy to have spent no time on installing or creating GitHub accounts.

[Patrick Massot]

As usual it was very interesting to see how professional mathematicians struggle to decompose proofs into atomic steps. For instance, for many people, using h : a = b to replace a by b is indistinguishable from using h : b + c = 0 to replace b by -c. They simply don’t see what I mean when I say the second one is doing one more step.

[Kevin Buzzard]

I've also seen this phenomenon about confusion with intro, from smart people. Even when doing dumb stuff like composite of surjective is surjective: I say "OK so we need to prove that gf : X -> Z is surjective, so we need to prove that for all z in Z there's x in X with gf(x)=z, so let z in Z be arbitrary with intro z" and I instantly get the question "how did the system know that z was in Z?". I guess I'm just too familiar with the system to figure out why this is confusing. I just explain that the goal is "for all z in Z, ..." and the system knows this, but I guess on paper we would say "now let $z\in Z$ be arbitrary" and in Lean we just say "now let $z$ be arbitrary and it's obvious where it is".

[Julian Berman]

The same sort of thing seemed like it happened in @Alex Kontorovich's recent video, there is a few minutes of questions when intro is mentioned.

[suhr]

Patrick Massot said:

I started with showing the introduction file, which took a lot more time than what I hoped for. As often happen when I show Lean in talks, I spent a huge amount of time answering question about the magical intro tactic. There is something I really don’t understand here. I have a goal which starts with ∀ ε > 0, … and even when I type two intro lines intro ε; intro hε many people find it super confusing that the tactic script does not contain the characters ε > 0.

This problem is easy to solve: intro ε (hε: ε > 0). Now your proof script is both less confusing (contains ε > 0) and more readable (you don't have to look into Lean Infoview to know what hε stands for).

[Jeremy Avigad]

Wow, this strikes me as a watershed moment. Type theory can be a pain in the neck, but its utility stems from the fact that context often dictates what sorts of objects we are dealing with and what assumptions are at play. So, when I read Patrick and Kevin's messages, what I hear is "I really don't understand why mathematicians find type theory confusing." How wonderful!

[Jeremy Avigad]

Patrick, Kevin, you have come to the dark side.

[suhr]

A proper explanation requires explaining Lean as a theory of constructions rather than as a magic box of proof checking.

[Alex Kontorovich]

suhr said:

This problem is easy to solve: intro ε (hε: ε > 0). Now your proof script is both less confusing (contains ε > 0) and more readable (you don't have to look into Lean Infoview to know what hε stands for).

I like that idea! At my presentation, a lot of people seemed to be confused because I gave the hypothesis ε > 0 the name ε_pos, and people were asking if _pos was a special Lean command that lets you say that something is positive... :man_facepalming:

[Alex Kontorovich]

(I was also trying to show them something in 30 mins, not 2 hours, so it was a (glimpse)^3 of Lean...)

[Anne Baanen]

suhr said:

A proper explanation requires explaining Lean as a theory of constructions rather than as a magic box of proof checking.

Hmm, that sounds like a much too negative description of what Patrick is trying (quite successfully, I should say!) to do here. The fact that we can explain how to use Lean productively without having to resort to multiple lectures on the CIC is a big win. By all means, dive into type theory if the interest is in explaining why Lean does things the way it does. But knowing that it works this way is more than enough for my daily Lean use, and I studied type theory! Not throwing others in the deep end right at the start is a well-thought throug strategy that Patrick, Kevin, Alex (and indeed myself!) have worked hard on, and the work quite clearly pays off.

[suhr]

The problem with "magic box" explanations is that people get stuck once they make an unfortunate step out of leaned bounds. Knowing a few core ideas gives you full freedom, you are only limited by how well you mastered them.

Basically, a programmer's view on magic.

But I agree that non-magic course is hard to make short (though it does not require multiple lectures on CIC) and probably even impossible for such a tiny tutorial like the Glimpse of Lean. Magic is good for getting started quickly, it's only becomes a problem in long term.

By the way, it's hard to be negative towards Patrick's work. I might somewhat disagree with it, but it has a style.

[Patrick Massot]

This specific issue has nothing to do with foundations. I would expect any proof assistant, relying on any foundations, to be able to understand that if the current goal is P implies Q then the any command described as “assume the premise of the implication we have to prove” will be able to assume P is true without asking users to spell out P in the command. You are probably confused because you think about what happens in Lean when using an implication. There is becomes vaguely relevant to understand the link between functions and implications in Lean (only vaguely because it could be a notation trick instead of a foundational fact).

[suhr]

Fair enough, every system in the style of natural deduction would work the same way. You have

P ⊢ Q
--------
⊢ P → Q

which is implication introduction rule.

But I would guess, mathematicians are not used to think about proofs that mechanically. So one is free to assume anything, just not every assumption would make sense. Good old "a proof of P → Q is a construction which combined with an evidence of P gives an evidence of Q" should get you back on track: if you assume something, it ought to be P.

That's but a speculation, of course: I have never seen confusion about intro among programmers, and I don't really know how mathematicians think about proofs.

[Daniel Weber]

Crazy idea: avoid introducing names for proofs and instead use ‹a = b› notation

[Edward van de Meent]

it gets annoying to type tho :smiling_face_with_tear:

[Patrick Massot]

This is becoming really off-topic for this thread, but Daniel’s suggestion is implemented in the nameless flavor of Verbose Lean (which technically names assumptions but never refers to those names). See for instance https://github.com/PatrickMassot/verbose-lean4/blob/master/Verbose/English/Examples.lean#L19-L37.

[Patrick Massot]

Note that this mode of Verbose Lean can be configured to do a lot more than ‹a = b›, see https://github.com/PatrickMassot/verbose-lean4/blob/master/Verbose/English/Examples.lean#L91-L113 for a more realistic example (it can be fun to spot all lemmas that are applied automatically here).