A tutorial of Lean for mere mortals

Stream: general

[Alcides Fonseca]

Today I have taught a smallish tutorial on Lean, expecting only a basic understanding of Haskell and proof by induction on paper. I believe it went quite well, with lots of participation and success in the few exercises. I have written about it and published the materials online at https://wiki.alcidesfonseca.com/blog/lean-tutorial-mere-mortals/. Feel free to provide feedback.

This is given from the point of view of a non-mathematician that has little knowledge about logic or Lean. It is designed to help people learn the basics so they can learn more afterwards. I present Lean as three languages (that are the same): the computable language (inductive, structures, def, bool), the language of proofs (example, theorem, lemma, axioms and it is written using tactics) and the tactic meta language (anything with meta). Of course I focused on the first two. I know that you can define lemmas and theorems using def, but mixing the two makes this difficult to beginners.

And as a beginner, I spend a lot of time reading the lean standard library (and mathlib) and I have to confess it gives me a headache trying to figure out a lemma or tactic that might help me where I am stuck (library_search is only helpful when you are close to the goal). And yes, reading the source code is much more useful than the documentation. I understand it is an ongoing project, so I am not really complaining. But maybe a less concise and more novice-friendly code in the standard library would help.

Another aspect where I believe Lean could be improved for users like me is to have more "procedimental"-style tactics. For instance, "existsi" is perfect for my style, but there is no equivalent for handling \exists in both the goal and context. I always have to write an auxiliary lemma for each case in the "first language" style, which makes things confusing. Concluding: I like the division of the languages, I find proofs in this style (mine or from NNG) very readable, but the ones in the standard library are really concise (good) but hard to understand at a glance (bad).

[Bryan Gin-ge Chen]

Thank you for sharing! It's definitely true that the core library and mathlib are both difficult to read for beginners, so more tutorials are always welcome.

Could you say which documentation you were referring to when you said "And yes, reading the source code is much more useful than the documentation." ?

[Alcides Fonseca]

"Theorem Proving in Lean", "The lean reference manual" and "Mathlib reference". But cmd+clicking each symbol to see its source and nearby lemmas ends up being much more useful.

[Mario Carneiro]

For instance, "existsi" is perfect for my style, but there is no equivalent for handling \exists in both the goal and context. I always have to write an auxiliary lemma for each case in the "first language" style, which makes things confusing.

I don't understand what you mean here. If you have exists in the context, you can't use existsi, the proof rule has a very different form

[Mario Carneiro]

are you saying you want existse to be a synonym of cases?

[Bryan Gin-ge Chen]

Alcides Fonseca said:

"Theorem Proving in Lean", "The lean reference manual" and "Mathlib reference". But cmd+clicking each symbol to see its source and nearby lemmas ends up being much more useful.

I see. Yes, I'm not sure what kind of documentation could beat jump-to-definition or other in-editor tools if your primary aim is to find lemmas related to a definition.

TPiL at least is meant less as a comprehensive reference and more as an introduction to the language; without reading TPiL or something similar first, I don't think I would have been able to even parse the types of the declarations in the source code, let alone their proofs. Any suggestions as to how the mathlib docs might be made more useful? Contributions are certainly welcomed!

[Alcides Fonseca]

Not from the context, but rather when you have a goal in the format ∃x:N you can use "existsi 0" to get rid of it. But when you have a ∃ x in both the context and goal, there is no "procedimental" tactic that allows us to cut both of them at the same time. The solution is to use "exists.elim", which has a more functional style, more difficult to read.

[Mario Carneiro]

if you have exists x in the context and the goal, you first remove the exists in the context with cases h, then remove it from the goal with existsi x (and you have to specify x because otherwise it isn't clear that you want the witness to one to be the one you got from the other).

[Mario Carneiro]

I wouldn't recommend using exists.elim unless you like term mode proofs (and you very clearly don't)

[Mario Carneiro]

BTW procedimental isn't an (English) word. Perhaps you mean procedural

[Alcides Fonseca]

Thank you for the feedback. I spent hours looking for this alternative and I coudn't find it! I had no idea that using cases on an existencial quantifier would have that effect. @Bryan Gin-ge Chen , this is one example of something that the documentation does not explain, as one might need to understand the implementation of ∃ to figure it out that cases can be used to take it apart. And even by looking at its source code, I cannot understand why cases works.

[Mario Carneiro]

I would hope this is mentioned in TPIL

[Mario Carneiro]

The reason it works at a fundamental level is because exists is an inductive type and cases destructs inductive types

[Mario Carneiro]

I don't know if this appears in NNG because the theorems that are proven all have a simple logical form. Probably the upcoming book Mathematics in Lean will have the right balance of logic and tactics to make cases prominent

[Alcides Fonseca]

TPiL shows the functional version using exists.elim. ∃ has a single constructor. What I missed is that all parameters to the constructor show up in the context. I have never needed something that would do that.

[Mario Carneiro]

TPIL starts in term mode but it covers some tactics eventually

[Mario Carneiro]

What I missed is that all parameters to the constructor show up in the context

No, what is needed is that an element of the inductive type is in the context. It doesn't need to be the constructor, and in fact cases is what you use when you want to express an arbitrary element of an inductive type as one of the constructors

[Bryan Gin-ge Chen]

TPiL mentions that exists is defined inductively and it also shows some examples of using cases to destruct inductive types, but it's true that it doesn't show using cases on an exists.

[Mario Carneiro]

it's the tactic version of a match statement

[Mario Carneiro]

Probably TPIL should be updated to have both term and tactic mode examples in parallel. @Jeremy Avigad What do you think?

[Bryan Gin-ge Chen]

Now that I think of it, I used to write a lot of exact exists.elim blah too, probably because I didn't realize how much easier it was to use cases or rcases.

[Mario Carneiro]

I'm not really sure what the best reference is for learning the absolute basics of tactics. Probably Mathematics in Lean

[Alcides Fonseca]

So during the tutorial, we discussed using Lean for our FP undergraduate course (right now we use proofs on paper). The mix of term and tactic styles in the documentation is actually a huge problem for this purpose. If I expand this tutorial (I'd like to do something similar to "Programming Language Foundations in Agda" in Lean), I am planning on only using tactic style. Being able to use the two styles to separate computable and logical components is what makes Lean a much more interesting target than Agda.

[Mario Carneiro]

You should definitely look at MiL because although it is still under construction it sounds like it has similar design criteria

[Bryan Gin-ge Chen]

See https://leanprover-community.github.io/mathematics_in_lean/

[Alcides Fonseca]

Mario Carneiro said:

You should definitely look at MiL because although it is still under construction it sounds like it has similar design criteria

Section 2 follows the pattern I am advocating (for this particular audience, ofc). But sections 1 and 2 also have several examples in the other style. Nevertheless, I might take a go at 2 and 3 to revise my Lean knowledge.

[Alcides Fonseca]

For our students (Informatics Engineering, similar to SE), anything with abelian groups or topology will not be usable. Thats the motivation for working on this particular tutorial, as it will not depend on any mathematical background (I have none!) and all examples can be PL-related.

[Mario Carneiro]

I think section 1 is an introduction meant to show the gamut of lean proof styles, like your "three languages"

[Bryan Gin-ge Chen]

Have you seen the Hitchhiker's guide to logical verification? It's one of the links here: https://leanprover-community.github.io/learn.html#textbooks

[Alcides Fonseca]

My point with the three languages is that (in my opinion, which I understand is far from being popular around here) is that you should always use tactic-style for any kind of proof, and leave term-style for code that will be executed. It's not like I want to change the way the community writes Lean, but rather if I want our undergraduates to use it, the provided documentation has to be quite limited (most documentation eventually digs into more difficult aspects before introducing everything we need). My solution for this is to write our own documentation in this style (with quite a limited depth and scope, which is desirable for such purpose).

As an example, in my compilers course, I provide documentation for a subset of LLVM that is self-contained. I do not rely on public documentation (although students can use it for reference) as it frequently discusses topics that I don't want students to spend time worrying about.

[Alcides Fonseca]

Bryan Gin-ge Chen said:

Have you seen the Hitchhiker's guide to logical verification? It's one of the links here: https://leanprover-community.github.io/learn.html#textbooks

I believe I am the target audience for this book, but I haven't had the time to read it. I usually learn programming languages by doing (and not reading), but Lean has been quite a challenge and I have read (and watched talks) about it much more than any other language I've learnt in the past. This is on my to-read pile, as it discusses several internal aspects of Lean. But I believe it is not the right book for someone who only wants to prove some simple properties about programs.

[Jannis Limperg]

Alcides Fonseca said:

So during the tutorial, we discussed using Lean for our FP undergraduate course (right now we use proofs on paper). The mix of term and tactic styles in the documentation is actually a huge problem for this purpose. If I expand this tutorial (I'd like to do something similar to "Programming Language Foundations in Agda" in Lean), I am planning on only using tactic style. Being able to use the two styles to separate computable and logical components is what makes Lean a much more interesting target than Agda.

Have you considered Coq? It's less elegant than Lean in some ways but much more mature, meaning better docs etc. It also has the tactic-style proofs you want.

[Alcides Fonseca]

I've tried to learn coq, idris and agda in the past, but I have found all of them to be quite heavy in their syntax. I've never had the time to overcome that initial curve. NNG made me a fan of Lean and interacting with an SMT solver might be very useful for my own work. The Software Foundations book uses coq in their examples, and it might be an alternative for teaching, although I believe the subtle syntax diferences make Lean more programmer-friendly than coq. Thanks for the suggestion!

[Mario Carneiro]

My point with the three languages is that (in my opinion, which I understand is far from being popular around here) is that you should always use tactic-style for any kind of proof, and leave term-style for code that will be executed.

I don't dispute your characterization of the three languages at all, and also I don't think your view is unpopular. Indeed most of the leading figures around here have converged on a primarily tactic mode style. The term mode proofs in mathlib are primarily from older proofs and short proofs (and there are a lot of short proofs in mathlib because it is aiming for high coverage).

[Jeremy Avigad]

@Mario Carneiro In TPiL, the cases tactic is discussed here: https://leanprover.github.io/theorem_proving_in_lean/tactics.html#more-tactics. TPiL is good for someone who wants a bottom up introduction to dependent type theory; for tactic proofs, I agree, MiL, Hitchhiker's Guide, and the other resources out there do better.

[Mario Carneiro]

It just seems like a shame that all the resources right now focus on one or the other, when I feel that teaching them in parallel would be very instructive. I'm not sure where such a thing could best be shoehorned in, but TPiL does a good job of laying the term mode foundations, while other sources would have to be more radically altered to accomodate the low level view

[Scott Morrison]

I think teaching them in parallel, or shortly after each other, is really valuable.

[Scott Morrison]

One of the most profound :light_bulb: moments in my learning of Lean was watching Mario demonstrate golfing a tactic mode proof into term mode.

[Scott Morrison]

I think that learning how to convert a tactic mode proof into term mode is the step for a student that really demonstrates the first basic competence: after you can do that, you actually understand something about the system.

[Scott Morrison]

It's perfectly fine if after that they never do another such conversion again. (I like tactic mode proofs: term mode proofs are indecipherable after the fact to me.)

[Johan Commelin]

@Alcides Fonseca Nice job!
@rest can we somehow make it possible that upon hovering over an \exists it says

To prove a goal that starts with \exists, use `use` or `existsi`.
To extract a witness `x` and proof `hx` from a hypothesis `h` that starts with \exists,
use `cases h with x hx`.

[Johan Commelin]

If possible, we should add similar explanations to other common constructs (like \forall, \and, \or, etc)

[Utensil Song]

Hi @Alcides Fonseca , I really like your post and tutorial, particularly the personal touch during the learning process.

I went through a similar learning experience with Agda, Idris and Coq (plus maybe HOL Light and Isabelle/HOL ). While I can bear the burden of recognition of grammars, they are just not the languages I would appreciate to write and read. I know Lean from the manifest on https://lean-forward.github.io/, particularly the critics regarding the existing tools, the pain points described feel so correct so I checked the solution provided by the ones who criticize, and it turns out to be a perfect foundation for the claimed solution.

As a mortal with my own limitations and my own motivations, my perception of Lean is a versatile language that corresponds to the versatile world of programming, reasoning, mathematics and real-world applications (all these for verifying), but it's also based on one core essence, namely the Curry–Howard correspondence, that unifies all different styles and blurs the boundary between coding and proving. So the foundation is simple enough and powerful enough, that's a good start and I mean this by "a perfect foundation".

Then comes the proofs written in this language and the world become diversified. There're different tutorials, games, documentation only presenting Lean as an incomplete projection, advocating one or two styles. And when one reads real code written in Lean such as mathlib, even one can tell there's certain control of style, as a group effort, it's still utilizing all aspects in Lean and thus not so accessible to someone who just learned some fragments of Lean. One of the things I struggled with when I start reading and writing Lean is that when to use which style and how are they properly combined in one proof and the supporting lemma of the proof and how can one wrap their mind around this hodgepodge.

Eventually, I reached the "Aha!" moment and posted in https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/4.20proof.20styles to share the moment(actually there's the 5th style, conv mode proof). With continuous efforts after the post, I found myself able to switch between different equivalent styles in more complicated proofs and the style choices in mathlib started to make sense for me and a mental model start growing on me.

During learning, it's so natural for one to pick a particular linear path, but there will be a point the general grasp of the tool becomes nonlinear and multidimensional. Namely, I hated the tactics mode for its readability but loved the tooling support when finding a way to prove and writing it. But it soon becomes merely the crutch and I realized that I always never needed such step-by-step guidance for common programming but my own mind that's capable of planning things out. The structural proof is something that resembles more of the elements of hand-written proof and it reads like a natural language. As learned in "How to write proofs: a quick guide" by Eugenia Cheng, proofs are found not only by working from the goal side (the backward proof using tactics) and not only by working form the hypothesis side ( the forward proof), but both ends like building a bridge to meet in the middle, and he emphasize that the completed proof should be better written in the forward style so other can be convinced following a natural time flow and convincing someone the correctness of the proof is the ultimate goal of proof, no matter it's backed by some computers. The structural proof also provided more hints than bare bone minimal that computer would accept as a formal proof, if well written, it would clearly reflect the whole planning process of the proof and the intermediate goals as stepping stones. It can be further enhanced with literate style syntax that's useless for computers but so helpful for readers. Besides these two major directions, term mode proof is actually more accessible to programmer, since it turns the proving process into a type filling game and it's succinct for some irreducible lemmas. My favorite style is the calc mode, since it feels doing math and greatly helps the reading to understand what's happening, but current implementation has not reached the full potential of this paradigm (like doing even crazier things with both side and the operation and goals) thus it can't write a full proof for a complicated proposition. The conv mode is like the tactics mode in the sense it also breaks things down but it provides more freedom during the process.

The above has only addressed one language of your three. I haven't dived into the details of the functional programming language and the meta-programming language yet. So far I feel the former is very limited and also it doesn't have a rich ecosystem to back it and the main users of Lean don't seem to have heavy use cases for it for now so it's not growing at its full speed, both for the language aspect and the library aspect(see Rust for such an evolving community focusing on making the language more ergonomic for common programming). But I do need it to be a complete functional programming language to implement efficient data structures and algorithms to verify against and Lean also haven't found a partner language to verify against. On the other hand, the meta-programming language is in an exactly opposite position: it's well established on the experience of do notation and has heavy use cases in tactics development which will drive its growth. The obvious missing piece I can see is the interoperability with other languages and ATP tools but it's possibly mostly due to what the former lacks.

Summarizing the above, Lean provides both a rich mindset and toolset for the users to explore with so it has great potential in all the programming paradigms it supports, but it's still in a not so mature stage so all aspects of its potentials are not evenly growing, and it suffers from its own weight as a versatile programming language for newcomers and the diversified audience it targets, varying from common programmers, mathematicians, undergraduate students, formalization experts and other mortals such as me who is driven by the dire of formalizing some particular programmable applications with the sound foundation in pure math, building a bridge from pure conceptual world to executable code for practical applications.

[Johan Commelin]

@Alcides Fonseca One little comment about your post: I think when you write "mathematician" you mean "type theorist". Almost all mathematicians that I know are extremely intimidated by even the most trivial bit of computer code...

[Johan Commelin]

There is a small minority that uses computer algebra syststems to do computations, and an even smaller minority that's playing with theorem provers. Of course this should change. And something like NNG is a very nice gateway drug.

[Bryan Gin-ge Chen]

Johan Commelin said:

@rest can we somehow make it possible that upon hovering over an \exists it says

To prove a goal that starts with \exists, use `use` or `existsi`.
To extract a witness `x` and proof `hx` from a hypothesis `h` that starts with \exists,
use `cases h with x hx`.

It looks like we can do it by adding a docstring here.

Edit: @Scott Morrison beat me to it: lean#296.

[Scott Morrison]

Let's add some more!

[Scott Morrison]

If this seems reasonable, I/we can go through all of logic.lean, and possibly other files, adding doc-strings. I really like the idea of writing the doc-strings specifically as hints for new users. That is, I would propose writing them like Johan's suggestion above, or my version in lean#296 --- they should be "to do X, use tactic Y".

[Scott Morrison]

Ok, I added and, or, and not to that PR.

[Scott Morrison]

I think heq deserves a "which tactics and lemmas are you meant to use" doc-string... I would still use that one. :-)

[Kevin Buzzard]

I think that the analogous docstring for heq should just say "please turn back, you made a mistake" ;-)

Over the weekend I watched a very early talk by Leo about Lean and he was enthusing about how cc could handle heq

[Jasmin Blanchette]

@Alcides Fonseca I use the hitchhiker's guide as a textbook for an MSc-level course. I believe Chapter 4 should correspond to "prov[ing] some simple properties about [functional] programs". It's the basic stuff: proving that the reverse of the reverse of a list is the original list, and such. You could skip Chapter 3, which not essential if you want to prove things using tactics.

[Patrick Massot]

@Alcides Fonseca , did you try to do the tutorials project? It supposes no math knowledge (although familiarity with the very basics of the theory of sequences of reals numbers certainly helps in the second half). The zeroth file explains the differences between terms and tactics and how to move between them, but then it's tactics everywhere. And of course it explain how to use quantifiers. It is totally independent of TPIL or other resources beyond the installation instructions.

I agree that we lack resources for people that know absolutely no maths, although I thought the Hitchhiker guide was targetting this audience. But I don't think that writing tutorials when you don't know how to use an assumption starting with exists is such a great idea. What really puzzles me is you seem to know about this Zulip chat and you didn't have the idea to ask here before writing this stuff.

[Alcides Fonseca]

Johan Commelin said:

Alcides Fonseca One little comment about your post: I think when you write "mathematician" you mean "type theorist". Almost all mathematicians that I know are extremely intimidated by even the most trivial bit of computer code...

During the tutorial, we had a very diverse audience. The programmers liked the "Lean style" much more than mathematicians (Not necessarily type theorists"). Mathematicians did not like that in Lean, you can omit several things that the elaborator can figure it out. It made the proof too magical for them. But they were the ones that got into lean the easiest, even without knowing the Curry-Howard correspondence.

But you might be write, Type Theorists are the ones who like the term-style more. The mathematicians I presented to agreed that the tactic style was much more understandable.

[Johan Commelin]

Funny that the mathematicians didn't like omitting things... because in practice we do that all the time. We write a * b without saying in which ring we are multiplying...

[Alcides Fonseca]

Utensil Song said:

Hi Alcides Fonseca , I really like your post and tutorial, particularly the personal touch during the learning process.
Then came the proofs written in this language and the world become diversified. There're different tutorials, games, documentation only presenting Lean as an incomplete projection, advocating one or two styles. And when one reads real code written in Lean such as mathlib, even one can tell there's certain control of style, as a group effort, it's still utilizing all aspects in Lean and thus not so accessible to someone who just learned some fragments of Lean. One of the things I struggled with when I start reading and writing Lean is that when to use which style and how are they properly combined in one proof and the supporting lemma of the proof and how can one wrap their mind around this hodgepodge.

I completely agree with this and it's the core of my post: Lean is very useful for different people out there, and the programming style and teaching style needs to be different for difference audiences.

For a non-CS audience, I can teach python/java without explaining what is Bytecode or Garbage Collection, but for CS I will teach what is a compiler and an interpreter, as well as how memory management works right from the bat.

Given my appreciation for Lean, I wanted to contribute with a smallish tutorial for people who I want to be able to use Lean without knowing how Lean works on the inside. Ofc, I want to understand it myself, so the materials that I produce are quite different than the ones I use.

[Alcides Fonseca]

Patrick Massot said:

I agree that we lack resources for people that know absolutely no maths, although I thought the Hitchhiker guide was targetting this audience. But I don't think that writing tutorials when you don't know how to use an assumption starting with exists is such a great idea. What really puzzles me is you seem to know about this Zulip chat and you didn't have the idea to ask here before writing this stuff.

The tutorial I gave (and wrote later in the day) had a very specific and narrow goal in mind: prove properties about very simple programs. In fact, for that purpose I only need intros, rw, induction, simp, left, right and exact. I don't feel I need to be a Lean expert to write a tutorial for this purpose. The tutorials project you mention is probably the closest thing in style, but requires too much mathematics (even in the first example). My tutorial apart from simplifying addition and proofs by induction requires no previous knowledge.

Having said this, my tutorial is not the right starting point for someone who wants to learn Lean including its workings. It was designed for someone who will be able to use Lean for a particular goal without learning the rest.

[Utensil Song]

Johan Commelin said:

Funny that the mathematicians didn't like omitting things... because in practice we do that all the time. We write a * b without saying in which ring we are multiplying...

Because mathematicians only like omitting things known to them but not something magical in code ("Almost all mathematicians that I know are extremely intimidated by even the most trivial bit of computer code")?

[Johan Commelin]

That's true

[Alcides Fonseca]

I can give a concrete example: they did not like rewrite (at least how I used it) because I didn't specify which occurrence of that function I wanted to rewrite.

[Jasmin Blanchette]

I would like to understand your point but I don't think I do. My students know hardly any math (the VU Amsterdam C.S. curriculum is very practice-oriented). Your examples are very similar to those I cover in Chapter 4. I agree there's much of Chapter 3 one can skip (although in your talk, you seemed to cover Curry-Howard?), but I fail to understand where the Hitchhiker's Guide "requires too much mathematics". The mathematical material is mostly in Chapters 11-13.

[Alcides Fonseca]

Chapter 4 by itself fits what I need. But the introduction for one to be able to read Chapter 4 is too complex on the Hitchhiker's Guide for our students (considering one or two weeks of content). My tutorial would work as a lighter pre-Chapter 4 introduction, that the first Chapters.

Of course for me, this book seems like the ideal read.

[Jasmin Blanchette]

I see.

[Alcides Fonseca]

I mentioned Programming Language Foundations in Agda, but if your book had the same type of proofs (typechecking, progress and preservation), it would be awesome! Just adding things to the wishlist :)

[Utensil Song]

Too bad https://github.com/Kha/electrolysis (mentioned at the end of the tutorial) is only for Lean 2 and not maintained since 2017. Libraries need a life longer and more sustainable than academic cycles.

[Jasmin Blanchette]

Type system are interesting but more advanced, I feel, that the semantics of WHILE. PL stuff only accounts for one of the four parts of the course, or three lectures. That's already three lectures more than in earlier editions of the course (from the 1990s until 2018).