Pretty proofs?

Stream: general

[Martin Dvořák]

[soft question]
A friend of mine asked me:
"Isn't the whole point of computer proofs that they aren't pretty, and it's just the result that matters?"

I know that mathlib has pretty high standards regarding what proofs are added to mathlib. I could probably generate a few answers why. However, I don't know what is really important. So I thought it would be better to forward the question to you guys.

Why do we care about how proofs in Lean are written?

[Yaël Dillies]

One argument is that we're basically writing a giant textbook and readability is thus important. Another is maintainability. A badly written proof is much harder to understand, hence to fix. Your friend seems to be thinking about one-time proofs, which you can just throw away once you're done. This is not the case in mathlib, where definitions change and we concretely have to keep everything coherent.

[Yaël Dillies]

Note that this doesn't actually argue for pretty proofs, but rather for short and simple proofs. They are quite correlated though.

[Pedro Sánchez Terraf]

Yaël Dillies said:

Note that this doesn't actually argue for pretty proofs, but rather for short and simple proofs. They are quite correlated though.

I think I disagree with the correlation. Before continuing, full disclosure: I'm new to Lean and I come from the Isabelle camp, but from rare corner of if (not a user of HOL).

[Pedro Sánchez Terraf]

There, I used to write in an extremely verbose way, in such a way that in the ideal situation you wouldn't need to look at the Infoview/proof state to understand what is going on

[Pedro Sánchez Terraf]

So, my (perhaps repeated) question is whether here in mathlib we are going against the “giant textbook” approach by golfing proofs.

The extreme opposite would be to have proofs written in a style similar to that used in the tutorials. I really do not know if there are some technical limitations (such as speed of processing the code) that make this prohibitive.

I understand that this will result in proofs that are very long , but (again, using the “textbook“ analogy), perhaps someone could learn the math underlying some mathlib proof by reading just the code.

[Eric Rodriguez]

In some ways the hope is that you do have access to the info view, and there's been tooling developed to help with this such as Alectryon.

[Scott Morrison]

I really disagree with the characterisation that we're writing a giant textbook and consider readability important. Only a handful of proofs in all of mathlib even approach readability.

[Scott Morrison]

(I'm not saying I think we're doing the right thing, by ignoring readability.)

[Pedro Sánchez Terraf]

Scott Morrison said:

(I'm not saying I think we're doing the right thing, by ignoring readability.)

It is very reassuring that people at least give some thought to the matter. On the other hand, writing readable proofs is extremely, painfully slower.

[Matt Diamond]

I really disagree with the characterisation that we're writing a giant textbook and consider readability important.

I think src#Set.powerset is a good example of how terse it can get

[Matt Diamond]

on the other hand, it's nice to find the most elegant solution

[Scott Morrison]

I think a good/realistic target would be: any proof less than 10 lines with no "mathematical content" (i.e. that you would never find yourself explaining to a human) can be golfed to the point of abscurity. Any proof longer than that should either be split (after which the first rule applies!) or it should have human readable comments explaining the proof structure in informal text, at least every few lines.

[Scott Morrison]

I like this as a compromise as it gives authors considerable leeway in how they structure their work, but avoids the monolithic impenetrable proofs that we know can't be maintained.

[Kyle Miller]

Adding to this, I think mathlib proofs aim to be at a higher level than just what comes after the :=, and instead it's in the statements of all the lemmas. It reminds me somewhat of the rising sea metaphor.

[Martin Dvořák]

If we want mathlib proofs to be readable (using infoview) we should use more rw and less simp IMO.

[Yaël Dillies]

That unfortunately makes proofs longer and more brittle overall.

[Scott Morrison]

I'm not certain about this. I feel like long rw chains are superficially more brittle (i.e. a little change will break them, in an easily fixed way), but a big simp can be traumatic to fix: it's robust to small changes, but then once it breaks you have little idea of how it was meant to be working.

[Jireh Loreaux]

That should be less true of simp if we had a way to distinguish among simp lemmas vs. non-simp lemmas within the braces (i.e., with coloring) as we had discussed in the other thread, along with code folding (so that all simps could be simp only under the hood).

[Martin Dvořák]

Yaël Dillies said:

That unfortunately makes proofs longer and more brittle overall.

Is the consensus that length and robustness are more important than readability then?

[Martin Dvořák]

When I read simp only [foo, bar, baz], I have no idea what happened (some magic probably).
If someone writes rw [foo, bar, foo, baz, foo], instead, I click my mouse after each comma and see the transformation step by step.

[Michael Stoll]

To bring in another aspect: is there any expected difference in efficiency between rw [foo, bar, foo, baz, foo] and simp only [foo, bar, baz]? (I assume simp [foo, bar, baz] would be less efficient, since it has to find the relevant lemmas first?)

[Martin Dvořák]

My intuition says rw [foo, bar, foo, baz, foo], must be more efficient, but my intuition has been wrong many times.

[Yaël Dillies]

Yes and no, because simp calls are much shorter, so take less parsing time. This is quite noticeable in very long lists of rewrite.

[Eric Wieser]

Sometimes you don't get the choice; rw foo works sometimes where simp only [foo] doesn't, and vice versa

[Patrick Johnson]

Martin Dvořák said:

When I read simp only [foo, bar, baz], I have no idea what happened (some magic probably).

set_option trace.simplify.rewrite true can be helpful.

[Patrick Johnson]

Hm.. Seems like there is always 0 in the simp rewrite list numbering. For example:

import tactic
open nat set
set_option trace.simplify.rewrite true
example : 0 ∈ {0} ∪ range succ ↔ 0 ∈ @univ ℕ := by simp

Produces:

0. [simplify.rewrite] [nat.range_succ]: range succ ==> {i : ℕ | 0 < i}
0. [simplify.rewrite] [set.singleton_union]: {0} ∪ set_of (has_lt.lt 0) ==> insert 0 (set_of (has_lt.lt 0))
0. [simplify.rewrite] [set.mem_set_of_eq]: 0 ∈ set_of (has_lt.lt 0) ==> 0 < 0
0. [simplify.rewrite] [nat.not_lt_zero]: 0 < 0 ==> false
0. [simplify.rewrite] [set.mem_insert_iff]: 0 ∈ insert 0 (set_of (has_lt.lt 0)) ==> 0 = 0 ∨ 0 ∈ set_of (has_lt.lt 0)
0. [simplify.rewrite] [eq_self_iff_true]: 0 = 0 ==> true
0. [simplify.rewrite] [or_false]: true ∨ false ==> true
0. [simplify.rewrite] [set.mem_univ]: 0 ∈ univ ==> true
0. [simplify.rewrite] [iff_self]: true ↔ true ==> true

Shouldn't it be 1. 2. 3. ... instead of 0. 0. 0. ...? Or do these 0s stand for something else?

[Kyle Miller]

Here's where that trace message is generated: https://github.com/leanprover-community/lean/blob/master/src/library/tactic/simplify.cpp#L523

If I understand things correctly, the number before the . gives the "depth" of the trace message, which keeps track of how deeply nested of a context the trace message comes from. So for simplify.rewrite there's no nesting of this type. https://github.com/leanprover-community/lean/blob/master/src/library/trace.cpp#L170

[Martin Dvořák]

Do you think I use too much rws?
https://github.com/leanprover-community/mathlib/pull/17554/files
Many people would probably prove these two lemmata by simps.

[Riccardo Brasca]

Are a lot of declaration used in rw tagged simp? I mean, if just simp [foo] is enough then it's probably better, but I don't see any problem with rw.

[Martin Dvořák]

I think they are all simp lemmas. Both proofs can be replaced by:

begin
  induction L,
  { simp },
  { simp [L_ih] },
end

Do you think it is better to PR it with these simps instead?

[Riccardo Brasca]

Is the lemma obvious? Then simp is a pretty proof. You can probably just do

lemma append_join_append (L : list (list α)) (x : list α) :
  x ++ (list.map (λ l, l ++ x) L).join = (list.map (λ l, x ++ l) L).join ++ x :=
by { induction L; simp }

[Martin Dvořák]

It is obvious to me, yes.

[Martin Dvořák]

Riccardo Brasca said:

Is the lemma obvious? Then simp is a pretty proof. You can probably just do

lemma append_join_append (L : list (list α)) (x : list α) :
  x ++ (list.map (λ l, l ++ x) L).join = (list.map (λ l, x ++ l) L).join ++ x :=
by { induction L; simp }

Your code doesn't pass the induction hypothesis into the simp does it?

[Riccardo Brasca]

The idea is that we don't care about readability of obvious results (meaning that no human will ever want to see the proof.

[Riccardo Brasca]

Martin Dvořák said:

Riccardo Brasca said:

Is the lemma obvious? Then simp is a pretty proof. You can probably just do

lemma append_join_append (L : list (list α)) (x : list α) :
  x ++ (list.map (λ l, l ++ x) L).join = (list.map (λ l, x ++ l) L).join ++ x :=
by { induction L; simp }

Your code doesn't pass the induction hypothesis into the simp does it?

Ops: by { induction L; simp * }

[Eric Wieser]

I think the rws are good here, as they make it obvious what the API is, and they make the proof less fragile

[Eric Wieser]

If you've gone to the effort of finding the rewrites you may as well commit them

[Eric Wieser]

It's a lot more annoying to move proofs between (or within) files if you don't know what lemmas the proof uses

[Yaël Dillies]

Surely the rw make the proof more fragile?

[Martin Dvořák]

I think rw makes it more likely to need a fix but easier to fix it when it happens.

[Eric Wieser]

rws are also good at informing if the result you're looking for might already exist somewhere else