Improving the mathlib style guide

Stream: general

[Violeta Hernández]

There's a handful of things in mathlib where there's more than one way to write something down, and the style guide gives preference to neither option. I'd like to put these to vote to then update the style guide. It would be nice if as many people as possible voted.

[Violeta Hernández]

Number 1: Trailing commas at the end of code blocks.

example (n : ℕ) : n + 1 = 1 + n + 0 :=
begin
  rw nat.add_comm,
  refl, -- the comma here
end

[Violeta Hernández]

/poll Should these trailing commas be allowed?

• They should be mandatory.
• There shouldn't be a guideline for this.
• They should be disallowed.

[Violeta Hernández]

Number 2: Spacing in infixes

import data.nat.basic

-- No spacing
example (m n : ℕ) : (m+n)^2 = m^2+2*m*n+n^2 := sorry

-- All spacing
example (m n : ℕ) : (m + n) ^ 2 = m ^ 2 + 2 * m * n + n ^ 2 := sorry

[Violeta Hernández]

/poll Should spaces in infixes be allowed?

• They should be mandatory.
• There shouldn't be a guideline for this.
• They should be disallowed.

[Yakov Pechersky]

I think there's a difference between a style and it being mandatory

[Yakov Pechersky]

A style allows for not having to go and change everything. It also allows for flexibility when something calls for the opposite of a guideline

[Violeta Hernández]

By mandatory, I mean "part of the style guide". Perhaps I should have worded this more clearly.

[Yakov Pechersky]

Encouraged and discouraged?

[Violeta Hernández]

Yeah, that's it.

[Yakov Pechersky]

Perennial discussion, but a "black" style tool would be great. But likely only really feasible and useful lean4

[Violeta Hernández]

Number 3: spacing between ← and theorem in rw

-- no spacing
example (m n k : ℕ) : m + n + k = k + (n + m) :=
by rw [←nat.add_comm, ←nat.add_comm m]

-- with spacing
example (m n k : ℕ) : m + n + k = k + (n + m) :=
by rw [← nat.add_comm, ← nat.add_comm m]

[Violeta Hernández]

/poll Opinion on the spacing of ← in rw?

• They should be encouraged.
• There shouldn't be a guideline for this.
• They should be discouraged.

[Violeta Hernández]

I think that's all I'll put up to vote for now.

[Moritz Doll]

I think a discussion we should have (especially for mathlib4) is whether we want to have (a) more structured proofs, i.e., less refine and more have (b) encouraging proofs to be sufficiently commented so that it is possible to actually understand the proofs without looking in the literature. obviously this is only for proofs that are mathematically nontrivial.
I guess @Kevin Buzzard has some thoughts in that direction as well.

[Violeta Hernández]

My personal opinion is that it's not worth commenting proofs less than 10 or so lines long no matter how clever they are

[Violeta Hernández]

Because inspecting them usually makes them speak for itself

[Violeta Hernández]

Longer proofs, particularly public-facing proofs like in the archive, can usually benefit from comments

[Stuart Presnell]

I get the impression that the philosophy of mathlib is that the library of code is primarily there to teach things to the computer, and making things easier for human readers to understand is useful only to the extent that it serves that primary goal. That, as I understand it, is why we optimise for practical considerations like speed and brevity rather than readability, and hence why we don’t tend to explain the steps of a proof with comments.

[Filippo A. E. Nuccio]

I think this is a place to express once more my concern about the idea that "short proofs do not deserve comment" (with the indirect but related attitude of having very short proofs). I understand that short proofs are easier to maintain, but
1) They are really a nighmare to decipher if one is not already used to mahtlib. Since we talk a lot about getting more people onboard and the effect of lean/mathlib on teaching, I believe we should tackle this seriously.
2) The choice of spliting big results in small lemmas (which is, on its own, a reasonable choice), makes most proof very shorts. This does not mean that they are easy, it just means we are hiding everything under the rug because we decompose things so much that everything is locally trivial.
3) One may want to learn by looking at the code, and some math-trivial proofs are not lean-trivial. So they might deserve some comment.

[Mario Carneiro]

2) The choice of spliting big results in small lemmas (which is, on its own, a reasonable choice), makes most proof very shorts. This does not mean that they are easy, it just means we are hiding everything under the rug because we decompose things so much that everything is locally trivial.

Isn't "locally trivial" exactly the property you want of a good proof? If a theorem has been broken down like this then the theorem statements are all you need to understand the proof

[Mario Carneiro]

I don't see this as hiding everything under the rug at all, rather the opposite. Hiding everything under the rug is using by magic heavy tactics

[Mario Carneiro]

3) One may want to learn by looking at the code, and some math-trivial proofs are not lean-trivial. So they might deserve some comment.

In a broken-down proof, it's possible to make all of these doc comments instead of simply code comments. There is nothing saying that you can't put comments on theorems (even trivial ones), in fact I wish we did so more often and more systematically. And these get added to doc-gen and shown in hovers and so on which makes reading broken down proofs a lot easier

[Andrew Yang]

There are parts of mathlib where the proofs are all "locally trivial", but the amount of small lemmas is overwhelming and it is tedious to read through them all. Sometimes there is a long comment before the whole section outlining the proof strategy and highlighting the mathematically nontrivial lemmas from the other QoL/API lemmas, which I find very helpful when trying to reuse the intermediate lemmas. I think this kind of comments should nonetheless be encouraged.

[Stuart Presnell]

Part of the difficulty of reading mathlib proofs is that we often do things like inlining the proofs of some conditions to a lemma. For example, if lemma foo takes a condition 0 < n then we might end up writing a line like

rw foo (pos_of_bar_of_dvd_pow hd hn_bar ⟨k, h3 hk⟩)

rather than building things up step by step with have h_dvd_pow : ... and have hn_pos : .... This makes the proof shorter, but harder to unpick what's going on — and there's no way to "step into" the line to see what each part does.

[Mario Carneiro]

you can put your cursor in the middle of the line to get expected type info

[Mario Carneiro]

which is basically "stepping into" the line

[Mario Carneiro]

I think you can also use the widget view to click through the proof

[Eric Wieser]

I think this thread has departed from the original topic, which was about making decisions about trivial style choices regarding where individual characters go so that we have clearer style rulings to apply in review

[Filippo A. E. Nuccio]

Mario Carneiro said:

I don't see this as hiding everything under the rug at all, rather the opposite. Hiding everything under the rug is using by magic heavy tactics

OK, may be I should make it clearer what I mean by "hiding everything under the rug". I mean that the novice's path is by no means easy, but we pretend it to be. The fact that a big theorem needs 50 lemmas (say) shows that the theorem is somewhat deep. Of these 50, some will be crucial and some will be minor; some will be specific to this theorem, some will reveal some deep property; and some will be "technical results". If you decide to keep the long proof, you will be forced to explain it, and to underpin the contribution of every step. If they become 50 lemmas on an equal footing, there will be no communication at all about what is "really" happening. This was my (admittedly, too concise ;-) ) idea when I spoke about the rug.

[Eric Wieser]

In an alternate universe I guess we could use lemma vs theorem to distinguish crucial vs minor

[Michael Stoll]

Maybe another aspect is that it can be difficult to fix a proof that breaks because of some changes to mathlib when it is hard to understand how precisely the proof works. A less condensed style and comments can be helpful in such cases.

[Anatole Dedecker]

Let me just say that I really don’t think we are in a position of discouraging comments. I agree that for programming, clean code with clear names often removes the need for comments, but I think the situation is different here, because while programmers expect only other programmers to read their code, I think we should target having mathlib being as readable as possible for mathematicians. Besides, I think tactic mode has an intrinsic readability limitation : even with nicely structured proof, it is still nearly impossible for me to predict the tactic state after, e.g, a call to field_simp. And even if we decided that some comments are superfluous, mathlib is so under documented at the moment that making any rules on this matter would probably discourage way more useful comments than useless ones.

[Anatole Dedecker]

(I have nothing against field_simp, this is the first tactic that I thought of which is not predictable and is often used in a non-terminal way)

[Sebastien Gouezel]

A rule which makes things much more readable, and in my opinion we should advocate for proofs longer than 10 lines, say, is the following: It is forbidden to act on the main goal. So, no apply, no rw and so on. Instead, a sequence of have or suffices whose proofs may use the tactics you like -- unless the proof of such a subgoal is more than 10 lines, in which case the above rule should apply.

I know that I am in the minority here, and that most people prefer shorter but harder to read proofs. But I am still convinced it would be a very very good move!

[Filippo A. E. Nuccio]

Wow, this is radical but makes a lot of sense to me!

[Anatole Dedecker]

I agree with this, but I would put an asterisk for computational proofs, where rewriting is soooo efficient

[Sebastien Gouezel]

calc blocks would be allowed for computational proofs, of course. You can do it a 3 steps calc block, and use a lot of rewriting between two successive steps. And of course this has to be taken with a grain of salt.

[Kyle Miller]

Isn't forwards reasoning vs backwards reasoning one of those "holy wars" in proof assistants, like emacs vs vim?

That said, I like replacing golfed backwards proofs with calc blocks when possible.

[Junyan Xu]

suffices is still backward reasoning right? I think the main point is to write down intermediate statements? But you can also copy and paste the goal after an apply, for example.

[Anatole Dedecker]

I think the advantage/problem with backwards reasoning is that we have to put way less indications. When doing forward reasoning, you are essentially forced to announce what you do, whereas you can do a full backwards proof without any structure. But that doesn’t mean that backward style is less readable, we just have to force ourselves to use suffices because Lean won’t ask for it

[Junyan Xu]

By the way, why is suffices singular but all other (verb) tactics plural ... (any counterexamples?)
Update: I think the answer is that we say "it suffices" but "we have", "we apply".

[Sebastien Gouezel]

Yes, backward reasoning is still possible, but using suffices. Just like one would to in a paper proof!

[Anatole Dedecker]

I have to say that backwards reasoning is really what of the thing that Lean stuck in my head when doing maths in general, so I will never be able to evaluate how natural it is for mathematicians

[Stuart Presnell]

I’d suggest that the important distinction notion isn’t (always) “forward” vs “backward”, but simpler vs more complicated. Often it’s useful to act on the goal to simplify it, whereas building up lots of material with have can be complicated and confusing when the reader can’t see where we’re heading.

[Stuart Presnell]

For example, when we’re proving an equation of the form a + … x … + g = h + … x … + k, the simpler approach is to bring out the common term x and cancel it.

[Eric Rodriguez]

I find that length doesn't conflate with unreadability; I find most backwards reasoing proofs very legible now, and mostly I have no problem reading and understanding them, but one that really confuses me a lot is docs#disjoint.disjoint_sup_left_of_disjoint_sup_right, which wouldn't meet your "10 lines" rule and therefore would be okay.

[Ruben Van de Velde]

Also, by ring is more readable than any manual calculation I might do on paper

[Violeta Hernández]

Eric Wieser said:

In an alternate universe I guess we could use lemma vs theorem to distinguish crucial vs minor

This is something else I wanted to bring up but thought it would be too nitpicky for anyone to care

[Violeta Hernández]

Regarding the comments thing: I absolutely don't oppose good doc comments and module comments. I agree with Mario that ideally, all proofs should be locally trivial, and hence these comments should be enough to get the hang of a file. And in the few cases where that isn't possible, we should have good comments within the proof to make it easier to follow.

I fear that we'll end up with trivial comments that just clutter up the code while not making it any clearer, but I also agree that at the current moment, this is a total non-issue.

[Arthur Paulino]

From the standpoint of an inept mathematician like me, something I struggle a lot when reading mathematical sources is that things are built in a bottom-up fashion whereas my reasoning happens in top-down. I find out the smaller lemmas I need to prove in the process of proving my bigger lemmas. And when I read mathematical sources I see a big pile of theorems that I have no idea what they're for and I end up lost pretty quickly.

The type of documentation I usually miss is one that would say "this result is used in <bla> because <ble>". This way I would be able to put the pieces together as I go through the lemmas instead of having to stack things in my dynamic memory without a major structure. And stacking things in my memory is hard because I am a bad computer.

Of course lemmas, once stated (and proved, preferably), become objects with generic purposes. But still, I can't help but say that knowing why things are there would help me (and maybe others?) a lot

[Mario Carneiro]

@Arthur Paulino One trick that I use when reading math proofs, especially when I have an eye toward formalizing them, is to skim them in forward order so I don't get totally lost, but look for the result I'm interested in. Once I find the interesting theorem (e.g. the main theorem), I read that part carefully and then read the dependencies of that theorem, and then those dependencies and so on in reverse order. That way, I'm always reading a theorem with the knowledge of why it would be used (which also sometimes provides additional structure or even hypotheses you can put on the dependencies, e.g. this theorem is only ever applied when a is prime even though it only says a is odd in the theorem statement.

[Mario Carneiro]

You can do exactly the same thing when reading a formal proof. Start at the end, and the first time you see a theorem being referenced that isn't obviously true, jump to that and read it instead, and keep doing that until you hit obvious things. That way you never have to read trivialities and you go straight to the interesting part

[Mario Carneiro]

Forward ordering is a necessity dictacted by wanting a dag structure on proofs but it is a lot less clear IMO if the author just keeps on introducing things without it being clear why we should care about them. But even if the author pays a lot of attention to this aspect the explanation is only useful for people in the author's general headspace already. So it's up to the reader to provide their own motivation via the DFS method.

When formalizing I often read papers that are mathematically out of my league and what usually happens is that everything feels unmotivated and the explanation of the motivation is completely useless to me because it connects to other things I have never heard of. So I just skip all that and read only the stuff that is relevant to the proof.

[Winston Yin]

As a novice in proof assistants trying to learn different parts of mathlib, I found that many of my frustrations would be much relieved if there were more verbose documentation. For example, certain lemmas could have been tagged with "useful for constructing/proving this other thing" or "useful in combination with this other lemma" to save me the trouble of searching in what are sometimes overwhelmingly long documents.

There should also be more justification for the long strings of typeclasses, e.g. why [comm_ring R] is needed instead of just [semiring R]. These stronger typeclasses are sometimes introduced because a single step of the construction/proof requires it, but this wouldn't be obvious to anyone stumbling on this theorem later, who is wondering if a generalisation could be made.

If mathlib is going to become a useful tool in a mathematician's (or undergraduate's) toolbox, there needs to be examples of how an API is used, as a sort of tutorial. Conveniently, other theorems in mathlib that build upon an API are precisely such examples, but they would be less useful if not accompanied by suitable wordy explanations.

[Mario Carneiro]

There should also be more justification for the long strings of typeclasses, e.g. why [comm_ring R] is needed instead of just [semiring R]. These stronger typeclasses are sometimes introduced because a single step of the construction/proof requires it, but this wouldn't be obvious to anyone stumbling on this theorem later, who is wondering if a generalisation could be made.

Note that making the typeclasses more "optimal" often makes them even less understandable

[Mario Carneiro]

"useful for constructing/proving this other thing" or "useful in combination with this other lemma"

Maybe this can be done in some cases, but it's really hard to have a lemma point to some specific other application since it may be used in many different applications (and this is the common case, not the exception)

[Mario Carneiro]

Besides the general topical similarity you get from lemmas existing in the same file I don't really see how to make those cross links work except in the really obvious case where a lemma is only extracted from a proof to break it up and it is only intended to have one use

[Arthur Paulino]

@Mario Carneiro should we break this into a new thread?

Does it make sense to think of a button in the page generated by doc-gen that can show usages?

It's not as simple as a syntactical search because of simp lemmas, so maybe it would require a post-processing step to gather such information