new Lean / mathlib tutorial

Stream: general

[Jeremy Avigad]

Kevin Buzzard, Rob Lewis, Patrick Massot, and I have started working on a new tutorial introduction to Lean and mathlib, with help from Gabriel Ebner. It is here: https://github.com/leanprover-community/mathematics_in_lean. The tutorial is meant to supplement other sources, like Kevin's Natural Number game, Patrick's tutorial, and TPIL. There is overlap. The goal is to provide as much useful learning material as possible for people looking to learn how to formalize mathematics and contribute to mathlib.

There is also an online version: https://leanprover-community.github.io/mathematics_in_lean/, but we recommend using the VS Code version. We hope to get some new chapters out quickly over the next few weeks.

In VS Code version, the examples and exercises are opened in an examples folder and you can save your work. Caveat: we don't yet have a good way of updating the tutorial without moving your files and resetting the repository or making a fresh copy. And the infrastructure may get additional bells and whistles. But in the meanwhile, the current version provides some fun exercises for people looking for things to do.

Enjoy!

[Jean-Philippe Burelle]

Hi, I have started this tutorial and I think it's great so far. I completed the natural numbers game a few days ago, and have no other experience with lean or any theorem proving software.
I think it would probably be good to say a few words in the first page about the VSCode interface. For instance, how to open the Goals window if you closed it by mistake, and perhaps how to split/switch tabs according to how you expect the user to interact with the tutorials.
I also found a typo in the first exercise of 2.2 : The theorem to prove says (a+b) + -b = 0.
Maybe it's good to leave it there though, it teaches readers that theorem provers can be useful to spot mistakes in theorem statements :laughing:

[Jeremy Avigad]

Thanks! I just corrected the exercise in the version I am working on, so it will be fixed next time we put new material online, hopefully within the next couple of days.

As to adding more information about VS Code, from my experience writing documentation, it is a bad idea to mix purposes. Information then become fragmented, outdated, etc. I think it makes more sense to have a stand-alone markdown document with information about the VS Code interface and FAQs in the mathlib documentation folder (https://github.com/leanprover-community/mathlib/tree/master/docs). Or maybe such a thing already exists somewhere? I'd be happy to link to it from the text if someone writes it.

[Jean-Philippe Burelle]

Another small typo : at the end of 2.2, in the "group theory" block, I suspect the one_mul theorem should be mul_one, since the other one is an axiom.

[Johan Commelin]

@Jean-Philippe Burelle one_mul : 1 * a = a, and mul_one : a * 1 = a.

[Johan Commelin]

Because for the first it is "one mul something" and for the other, "something mul one"

[Jean-Philippe Burelle]

Yes, exactly, that's what I think it should say, but not what it currently says

[Shing Tak Lam]

I think what @Jean-Philippe Burelle is saying is that the exercise

theorem one_mul (a : G) : 1 * a = a :=
sorry

should be

theorem mul_one (a : G) :  a * 1 = a :=
sorry

since one_mul is true by definition of a group

[Johan Commelin]

@Jean-Philippe Burelle sorry, I'm dense :oops:

[Jeremy Avigad]

Thanks! I just fixed in my copy. It will be online within the next day or two. Also, the name of the theorem after that should have been mul_right_inv. We have a tool that checks the snippets to make sure they compile, but we don't have a tool to check the exercises to make sure that they make sense.

[Kevin Buzzard]

Yeah we do, it's called Zulip :-)

[Kevin Buzzard]

It should be called "the authors" but one of them is far more concerned with marking right now :-/

[Johan Commelin]

@Jeremy Avigad and others, on my 12 inch laptop, the documentation opened on the right hand side of the split, and therefore hid the "Lean Goal" window. After clicking "Try it", I had to manually switch to the "Lean Goal" tab.
For people who don't know that the "Lean Goal" tab/window exists, you might want to mention it.

[Johan Commelin]

This sentence towards the end of the intro also seems slightly crippled:

But be forewarned: interactive theorem prover will challenge you to think about mathematics and mathematical reasoning in fundamentally new ways.

I guess making that "an interactive theorem prover" would already fix it.

[Reid Barton]

Or "proving"

[Johan Commelin]

@Jeremy Avigad Another note. calc in tactic mode is now refine calc, and not exact calc. Just a minor point, but you might want to be aware of it (-;

[Kevin Buzzard]

(deleted)

[Jeremy Avigad]

Thanks! We'll mention the tab, and also modify the statement about calc so that it is not outright false.

[Jean-Philippe Burelle]

In section 2.5 : The second "absorption" exercise has a typo (sup instead of inf).

I also have a very basic question, which perhaps should go in "new members", but since I'm working through the tutorial I thought the context would be clearer if I ask here. I was working on the distributivity exercises, and my goal was in the following state : a ⊓ c ⊔ c ⊓ b = a ⊓ c ⊔ b ⊓ c .
I want to rw inf_comm on the pair c ⊓ b, but the proposition inf_comm uses the curly braces "implicit variables" so I get an error if I write rw inf_comm c b. I can get around this by adding an intermediate goal "have c ⊓ b = b ⊓ c" but this can't be the right way to do it... How do I specify where to substitute when a proposition has variables in curly braces ? I didn't have this problem with add_comm.

[Patrick Massot]

https://leanprover.github.io/reference/expressions.html#implicit-arguments

[Johan Commelin]

@Jean-Philippe Burelle I think typo is already fixed. (But maybe not yet live)

[Patrick Massot]

So you can use rw @inf_comm _ _ c b,

[Patrick Massot]

This is a general answer, but not what is expected here

[Patrick Massot]

Another general trick is to use

  congr' 1,
  rw inf_comm ,

[Patrick Massot]

But again this is probably not what Jeremy had in mind at this stage

[Patrick Massot]

Ok, I've reread the context, and I can do the exercises using only the surrounding lemmas

[Patrick Massot]

So no need for my general tricks

[Patrick Massot]

But it's a bit unfortunate that the obvious proof hits this implicit argument issue

[Jean-Philippe Burelle]

Yes, especially since it seems inconsistent with the way the previous section on rings worked (where this issue didn't arise) and the text states things like : "mul_comm a matches any pattern of the form a * ? and rewrites it to ? * a"

[Patrick Massot]

I think the good answer is that inf_comm should have explicit arguments. Feel free to open your first mathlib PR! (Maybe first check that @Mario Carneiro wouldn't complain)

[Bryan Gin-ge Chen]

Indeed, it looks like a lot of identities in order.lattice should have explicit arguments.

[Jean-Philippe Burelle]

What is the general philosophy for having implicit vs explicit arguments ?

[Bryan Gin-ge Chen]

The rule I've always followed is that an argument should be implicit iff it can be inferred from later explicit arguments.

[Bryan Gin-ge Chen]

For instance, if you have a lemma that depends on a : nat and ha : a > 0, then a can be implicit, since Lean will be able to infer it when you provide ha.

[Bryan Gin-ge Chen]

I'm trying to remember where I learned this and I guess it must be from the discussion in 4.1 of TPiL.

[Patrick Massot]

We also tend to use implicit arguments for iff statements when an object appears on both sides.

[Mario Carneiro]

@Patrick Massot I'm okay with this change. There are a number of definitions in lattices and topology written by Johannes in 2017 that use too many implicits. I'm not sure if it is a difference of style or if it is simply because of the variables {a b : A} at the top of the file causing this to be the default.

[Jean-Philippe Burelle]

I finished the exercises now.
A few more issues that I noticed at the end of Chapter 2 :

• The first ordered ring exercise is a ≤ b ↔ 0 ≤ b - a, and I think this is the first time the reader is asked to prove an equivalence. I had to use the "split" and "intro" tactics which I learned from the NNG but were not introduced yet in the book.
• For a few proofs in this section I wanted to replace "a - b" with "a + (-b)" and even though it's mentioned that "refl" works for goals of this type (and that this is the definition of "-"), I don't know which tactic to use to just replace one with the other in a more complicated goal. I managed to avoid having to do it in all cases but it's frustrating to know it's the right thing and not be able to do it.
• The mul_nonneg lemma in ordered_ring.lean is stated in terms of ≥ instead of ≤ for some reason, which does not match the book.

[Kevin Buzzard]

Many thanks for this!

[Reid Barton]

For your own information, you can achieve the second item using the change or show tactics, which are mostly overlapping in functionality.

[Bhavik Mehta]

I find change much easier to use in practice than show - in particular if I've made a type error in my new goal show will just say failed, but change gives me a more useful error message

[Reid Barton]

Oh interesting---I only ever use change really. I guess show's goal selection functionality prevents it from giving good error messages.

[Kevin Buzzard]

I tell students to use change because it works on hypotheses too

[Jeremy Avigad]

Oh! I thought show was syntactic sugar for change. In the early chapters, should I rely exclusively on change, or show readers both?

[Jeremy Avigad]

@Jean-Philippe Burelle You can rewrite a - b to a + -b with sub_eq_add_neg.

[Jeremy Avigad]

We'll fix the ring exercise. We are thinking of renaming the first chapter "Equality and Order" or something like that (because "basic skills" is so vague). Any thoughts there?

[Bhavik Mehta]

I personally don't see the advantage of show - change has the additional advantage of being able to modify subexpressions as well

[Jeremy Avigad]

O.k., Iets go with change.

[Sebastien Gouezel]

show is useful to treat the goals in any order. If you have a tactic that will spit several goals in an unpredictable order, it is really useful.

[Jeremy Avigad]

Yeah, I know. I'll go back and take a look at the text. Maybe we'll introduce them both at once, or maybe we'll start with change and use show later, when it is useful.

[Bhavik Mehta]

Sebastien Gouezel said:

show is useful to treat the goals in any order. If you have a tactic that will spit several goals in an unpredictable order, it is really useful.

Good to know, thanks!

[Mario Carneiro]

I think you can also use show to change the type to a defeq type like change. It would be nice if when it fails it gives the error for the first goal though, so that you get something more informative like change

[Bhavik Mehta]

Yeah, with show (even with one goal) if I give a badly-formed type I think the error message is 'failed' which is the same as if I give a well-formed type which isn't defeq to the goal

[Kevin Buzzard]

Yes. If I get failed with show then I usually change it to let foo := ... to see if what I wrote actually made syntactic sense and typechecked

[Reid Barton]

You should probably just change it to change instead though?

[Reid Barton]

assuming it's the current goal you want to change

[Aniruddh Agarwal]

Found a typo in section 2.1:

In response to the command #check mul_comm a b, Lean reports that mul_comm a b is a proof of the fact a + b = b + a.

should be

In response to the command #check mul_comm a b, Lean reports that mul_comm a b is a proof of the fact a * b = b * a.

[Jeremy Avigad]

@Jean-Philippe Burelle Thanks very much for the feedback. I left show in Chapter 2 but we mention changein the next chapter. We don't say much about either, but it's hard to decide what it is most important to convey early on, without subjecting the reader to information overload. We'll probably end up cycling back and saying more as they come up in more examples. I also fixed the exercise you mentioned, replacing the "iff" with two implications.

A draft of the next chapter is here: https://avigad.github.io/mathematics_in_lean/. We'll add sections on "not", "or", "and", and "iff" before the "convergent sequences" section, and hopefully have it out within a week or so.

@Aniruddh Agarwal Thanks for the correction! I just fixed it in the draft, so it will hopefully go online soon.

[Aniruddh Agarwal]

I'm not sure if this is a typo or not, but in the code block right at the beginning of section 2.2 supposed to begin with:

variables (R : Type*) [ring R]

Right now, it begins with

variables (R : Type*) [comm_ring R]

but the discussion around it is about non-necessarily commutative rings.

[Jean-Philippe Burelle]

@Patrick Massot I made a new fork and tried turning all the identities in lattices.lean to explicit variables, but this breaks a lot of things in mathlib. What's the best way when making such a change to track everything that broke in an organized way ?
In particular, after making the change, when trying to open some files (like things in topology/metric spaces) in VSCode I would get "ran out of memory" errors, I assume because so many things couldn't compile. This isn't very helpful to finding where the lemmas that I changed were used.

[Johan Commelin]

If you have the energy for this, that would be awesome!

[Johan Commelin]

Run leanpkg build in a terminal, and hit Ctrl-C as soon as you see the first error message

[Johan Commelin]

See which file it complains about, and open it in VScode.

[Patrick Massot]

There is a better way, hold on.

[Johan Commelin]

Fix it. Close the project in VScode.

[Johan Commelin]

Ooh, ok

[Johan Commelin]

/me is curious, about to learn how I should have done my refactors in the past.

[Jeremy Avigad]

@Aniruddh Agarwal Indeed, it should be ring. I'll fix it. Thanks!

[Patrick Massot]

@Jean-Philippe Burelle sorry for disappearing. I'm ready to answer questions now. Which declarations did you change?

[Patrick Massot]

Using leancrawler, you can type things like:

In [28]: [(name, lib[name].filename, lib[name].line_nb) for name in G.successors('inf_comm')]
Out[28]:
[('compl_inf_eq_bot',
  '/home/pmassot/lean/mathlib/src/order/boolean_algebra.lean',
  33),
 ('inf_infi',
  '/home/pmassot/lean/mathlib/src/order/complete_lattice.lean',
  476),
 ('mem_closure_iff_ultrafilter',
  '/home/pmassot/lean/mathlib/src/topology/basic.lean',
  533),
 ('Sup_inf_eq',
  '/home/pmassot/lean/mathlib/src/order/complete_boolean_algebra.lean',
  43),
 ('compact.image_of_continuous_on',
  '/home/pmassot/lean/mathlib/src/topology/subset_properties.lean',
  391),
 ('inf_left_comm', '/home/pmassot/lean/mathlib/src/order/lattice.lean', 265),
 ('multiset.inter_comm',
  '/home/pmassot/lean/mathlib/src/data/multiset.lean',
  1290),
 ('inf_sup_right', '/home/pmassot/lean/mathlib/src/order/lattice.lean', 363),
 ('inf_is_commutative',
  '/home/pmassot/lean/mathlib/src/order/lattice.lean',
  252),
 ('power_series.order_add_of_order_eq',
  '/home/pmassot/lean/mathlib/src/ring_theory/power_series.lean',
  1369),
 ('is_compl.symm',
  '/home/pmassot/lean/mathlib/src/order/bounded_lattice.lean',
  861),
 ('compact_of_finite_subfamily_closed',
  '/home/pmassot/lean/mathlib/src/topology/subset_properties.lean',
  199),
 ("filter.push_pull'",
  '/home/pmassot/lean/mathlib/src/order/filter/basic.lean',
  1424),
 ('disjoint.comm',
  '/home/pmassot/lean/mathlib/src/order/bounded_lattice.lean',
  817),
 ("filter.prod_comm'",
  '/home/pmassot/lean/mathlib/src/order/filter/basic.lean',
  1836),
 ('inf_eq_bot_iff_le_compl',
  '/home/pmassot/lean/mathlib/src/order/bounded_lattice.lean',
  279),
 ('cauchy_prod',
  '/home/pmassot/lean/mathlib/src/topology/uniform_space/cauchy.lean',
  202),
 ('nhds_order_unbounded',
  '/home/pmassot/lean/mathlib/src/topology/algebra/ordered.lean',
  404),
 ('filter.inf_ne_bot_iff_frequently_right',
  '/home/pmassot/lean/mathlib/src/order/filter/basic.lean',
  964),
 ('compact.inter_right',
  '/home/pmassot/lean/mathlib/src/topology/subset_properties.lean',
  43)]

[Jean-Philippe Burelle]

That seems useful! I changed all identities that had implicit variables to explicit, so le_sup_left, le_sup_right, sup_idem, sup_comm, and all their inf counterparts.

[Patrick Massot]

Enjoy https://gist.github.com/PatrickMassot/4e2cefb6be685dedfceb5653a0a4330d

[Patrick Massot]

You can also download https://www.imo.universite-paris-saclay.fr/~pmassot/mathlib.yaml and start playing from there (see the leancrawler README)

[Jeremy Avigad]

The next chapter of the new Lean / mathlib tutorial is now live:
https://leanprover-community.github.io/mathematics_in_lean/

[Yury G. Kudryashov]

Where is the source?

[Yury G. Kudryashov]

Found https://github.com/leanprover-community/mathematics_in_lean

[Patrick Massot]

no

[Jeremy Avigad]

It's here: https://github.com/avigad/mathematics_in_lean_source.

[Patrick Massot]

https://github.com/avigad/mathematics_in_lean_source/

[Patrick Massot]

Jeremy was quicker

[Jeremy Avigad]

We use mathematics_in_lean for the repository that users can fetch for the local VS Code version. But we also deploy the online version there, so we have the nicer url.