Where should I look for good code?

Stream: new members

[Simone De Rivo]

Hello,
I'm walking my path through Functional Programming in Lean 4, with some sporadic looks at the excellent Mathematics in Lean 4. I'm wondering what to do once I've finished these.

I'm certainly planning to look at Metaprogramming in Lean 4 eventually, but I'm not sure if I'll dive into it right away as I'm growing thirsty for math to formalize. But first, I'd like to see some high-quality code to learn how experts structure and write their proofs and programs.

Where should I look specifically? Should I first look at parts of the implementation of Batteries, Lean itself or even Mathlib, using the documentation as a reference? Or is there perhaps another project I might not know about that would be better to study first?

[Kenny Lau]

mathlib is good code, but the jump might be a bit big, it's best if you use it as a reference while you gradually adopt to mathlib style (the main thing is using term mode rather than tactic mode)

[Simone De Rivo]

Thanks for the advice. I'm limiting my use of tactics to the bare minimum as I gradually become more capable of working without them.

You're probably right in saying that Mathlib is a bit too much for a novice like me. At the same time, I understand that the language is still very young and the codebase isn't too large yet, so there's not much I can do except keep practicing and use the library code as a reference.

Allow me to ask one more question: why Mathlib instead of, say, Batteries, though? Is it just personal preference? Should I shy away from other standard of fairly standard codebases, or am I reading too much into your comment?

[Kenny Lau]

Mathlib has close to 7000 files now.

[Jireh Loreaux]

Kenny Lau said:

mathlib is good code, but the jump might be a bit big, it's best if you use it as a reference while you gradually adopt to mathlib style (the main thing is using term mode rather than tactic mode)

:thumbs_down: there's no reason to significantly prefer terms to tactics (outside of definitions). Mathlib has a history of over-golfing (of which I myself have been guilty at times). The focus should be on readability, reusability, maintainability and performance.

[Philippe Duchon]

Jireh Loreaux said:

:thumbs_down: there's no reason to significantly prefer terms to tactics (outside of `def`initions). Mathlib has a history of over-golfing (of which I myself have been guilty at times). The focus should be on readability, reusability, maintainability and performance.

On this topic of Mathlib code being often hard to read: I assume that, at some point, a good portion of it was written in a less expert way, possibly even with tactics as a help(!). Would it be a good idea to keep some version of this as comments? Each time I look at the source code to see how things are done, at best I get the names of other lemmas that were used to prove a given lemma, but mostly I have no idea how I could write a tactic proof, or prove a variant of the result in a similar setting - something that is often conveyed in informal proofs.

My understanding of the reasons why the Mathlib source code is often golfed beyond recognition is that it helps shorten compilation; are there other important reasons for this?

[Ruben Van de Velde]

Just to clarify, it is not mathlib policy to golf proofs beyond recognition, certainly not for theorems with mathematical content

[Ruben Van de Velde]

But if the proof is nothing more than one lemma applied to a few arguments, expanding it out to five lines when it could go in one often doesn't really help with readability either, perhaps once you've gotten a little more comfortable with term mode

[Ruben Van de Velde]

To learn about term mode, you could take one that you run into and try to expand it out to an equivalent tactic proof - that's often no more work than replacing f ha hb hc by something like

refine f ?_ ?_ ?_
· exact ha
· exact hb
· exact hc

and then you can walk through it

[Ruben Van de Velde]

And you can do that recursively while your intermediate states are still non-trivial

[Kevin Buzzard]

Philippe Duchon said:

I assume that, at some point, a good portion of it was written in a less expert way, possibly even with tactics as a help(!).

This is not correct. The philosophy of "if it's something which a mathematics lecturer would regard as trivial and which their students should be able to do just by following their nose, then destroy it in a one-liner" has been there since the start, and at the start 99% of the results in mathlib had this property.

Furthermore, in the early days there were far fewer tactics so one was forced to be even more creative in these one-liners.

[Ruben Van de Velde]

But it's also the case that mathlib skews fairly heavily towards writing little lemmas for steps that you might not even bother to justify in informal mathematics. So it may happen that rather than a single 10- or 15-line proof gets reduced down to ten lemmas, each with a proof that's simple enough to write it in term mode, and then your final theorem ends up being a small tactic proof using all those lemmas

[suhr]

Jireh Loreaux said:

there's no reason to significantly prefer terms to tactics

Except terms are both shorter and easier to read.

I believe popular Lean tutorials do a disservice by teaching tactics first. As a result, people do not understand how things work under the hood and find terms scary.

[Philippe Duchon]

OK, so I stand corrected. But the majority of my attempts are for things that should be trivial, and yet getting Lean to accept my proofs is still some work - so I don't get much help from the Mathlib one-liners.

[Ruben Van de Velde]

suhr said:

Jireh Loreaux said:

there's no reason to significantly prefer terms to tactics

Except terms are both shorter and easier to read.

I believe popular Lean tutorials do a disservice by teaching tactics first. As a result, people do not understand how things work under the hood and find terms scary.

I don't know that this position is shared by many people

[Damiano Testa]

I don't share it: proof terms may be simple in the simplest proofs, when the corresponding tactics proof are also simple. Anything more advanced becomes completely illegible in term-mode.

[suhr]

Philippe Duchon said:

But the majority of my attempts are for things that should be trivial, and yet getting Lean to accept my proofs is still some work - so I don't get much help from the Mathlib one-liners.

This is a hint though: often the reason why a statement is hard to prove is because you didn't soak it with enough lemmas.

Damiano Testa said:

Anything more advanced becomes completely illegible in term-mode.

I doubt it since in term mode you also have let and have, suffices, calc and rewriting (via triangle). And you have type annotations as well.

[Yaël Dillies]

@suhr, have you ever tried running show_term on linarith or ring?

[suhr]

Fair enough, sometimes you want some automation instead of writing tedious proofs by hand. It is not used that often though, for example https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/MeasureTheory/Measure/Stieltjes.lean mentions linarith only twice and ring only once.

simp is a stronger argument in favor of tactics: it is used everywhere and can in principle do a lot of rewriting.

[metakuntyyy]

suhr said:

Jireh Loreaux said:

there's no reason to significantly prefer terms to tactics

Except terms are both shorter and easier to read.

I believe popular Lean tutorials do a disservice by teaching tactics first. As a result, people do not understand how things work under the hood and find terms scary.

The thing is that tactics are way way way more intuitive to start. I started with the Natural numbers game and it was fairly straightforward since the tactics did the reasoning and steps for you. Also I don't think we have a really good tutorial on forward reasoning, or atleast I didn't find one.

[Kenny Lau]

Philippe Duchon said:

Each time I look at the source code to see how things are done, at best I get the names of other lemmas that were used to prove a given lemma, but mostly I have no idea how I could write a tactic proof, or prove a variant of the result in a similar setting - something that is often conveyed in informal proofs.

Are you looking at the source code in github? Have you tried looking at the source code in VSCode so you can see the goal at each step?

[Kenny Lau]

and also do you have an example? I could explain it to you

[Yaël Dillies]

suhr said:

sometimes you want some automation instead of writing tedious proofs by hand. It is not used that often though

Then we are not using Lean the same way :wink:

[suhr]

Well, that phrasing was awkward. Everyone use simp, but not everyone needs to use linarith (and a lot of places in Mathlib do not use it).

I also do not argue against automation. While it's possible to write a readable proof of trivial calculations by hand, nobody would like to read it.

Fortunately, Lean allows you to throw some by grind inside a term.

[suhr]

(I also should stop arguing about tastes, but it amuses me every time when people claim that Agda style proofs are completely illegible but Rocq style proofs are supposedly perfectly readable)

[Philippe Duchon]

Kenny Lau said:

Are you looking at the source code in github? Have you tried looking at the source code in VSCode so you can see the goal at each step?

I try to do both, but when the source code is in term mode you don't have intermediate goals (unless you change the code).

[Kenny Lau]

@Philippe Duchon that's not true. the intermediate goal is in the "expected type".

[Kenny Lau]

the one that live lean automatically collapses

[Kenny Lau]

theorem one_pos : 0 < 1 := by decide
theorem one_lt_two : 1 < 2 := by decide

theorem two_pos : 0 < 2 :=
  Nat.lt_trans one_pos one_lt_two

image.png

image.png

[Kenny Lau]

screenshots taken on Lean 4 Web (click the button on the top right corner when you hover over the code I posted)

[Philippe Duchon]

Thanks for the tip, I definitely don't pay enough attention to the "expected type" indication - I tend to see it as a nuisance that makes the current goal less visible.

[Klaus Gy]

suhr said:

I believe popular Lean tutorials do a disservice by teaching tactics
first. As a result, people do not understand how things work under the
hood and find terms scary.

Especially since there are so many tactics, as a newbie I often finish a proof using no tactics or one of the handful tactics I know, but then worry if I could improve it significantly if I knew all the available tactics out of my head.

[Kenny Lau]

Philippe Duchon said:

Thanks for the tip, I definitely don't pay enough attention to the "expected type" indication - I tend to see it as a nuisance that makes the current goal less visible.

yes, in tactic mode you want to look at the goal, but in term mode you want to look at the expected type.

[Kenny Lau]

Klaus Gy said:

suhr said:

I believe popular Lean tutorials do a disservice by teaching tactics
first. As a result, people do not understand how things work under the
hood and find terms scary.

Especially since there are so many tactics, as a newbie I often finish a proof using no tactics or one of the handful tactics I know, but then worry if I could improve it significantly if I knew all the available tactics out of my head.

you learn by making mistakes (and getting corrected)

[Kenny Lau]

someone (i.e. me) will eventually come and look at your code and say here's a tactic that can just do that

[metakuntyyy]

Klaus Gy said:

suhr said:

I believe popular Lean tutorials do a disservice by teaching tactics
first. As a result, people do not understand how things work under the
hood and find terms scary.

Especially since there are so many tactics, as a newbie I often finish a proof using no tactics or one of the handful tactics I know, but then worry if I could improve it significantly if I knew all the available tactics out of my head.

As a new user myself, here's the tactics that I use. have, intro, use, refine, exact, rw, simp, ring, norm_num, apply, and then conv mode if needed.

[metakuntyyy]

Ah contrapose! and by_contra are also occasionally useful to me. revert if I want to do some fancier stuff.

[Kenny Lau]

might i recommend to all of you aesop when "the goal is obvious"

[Kenny Lau]

and also omega and linarith, two very powerful tools

[Michael Rothgang]

Have you seen "tactic cheat sheets" such as this one? https://github.com/fpvandoorn/LeanCourse24/blob/master/lean-tactics.pdf

[Jireh Loreaux]

suhr said:

Jireh Loreaux said:

there's no reason to significantly prefer terms to tactics

Except terms are both shorter and easier to read.

I believe popular Lean tutorials do a disservice by teaching tactics first. As a result, people do not understand how things work under the hood and find terms scary.

@suhr I think you should do an experiment. Complete all the exercises in the Mechanics of Proof book twice, once with terms only and once with tactics (note: Heather specifically designed that book so that the exercises can be done almost entirely with tactics). Then go ask 100 people to choose which they find easier to read.