Zulip Chat Archive

Stream: general

Topic: Pretty proofs?


Martin Dvořák (Nov 10 2022 at 12:18):

[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 (Nov 10 2022 at 12:24):

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 (Nov 10 2022 at 12:26):

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 (Nov 11 2022 at 19:58):

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 (Nov 11 2022 at 20:02):

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 (Nov 11 2022 at 20:09):

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 (Nov 11 2022 at 20:17):

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 (Nov 11 2022 at 22:09):

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 (Nov 11 2022 at 22:09):

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

Pedro Sánchez Terraf (Nov 11 2022 at 23:37):

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 (Nov 11 2022 at 23:57):

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 (Nov 11 2022 at 23:59):

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

Scott Morrison (Nov 12 2022 at 02:15):

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 (Nov 12 2022 at 02:16):

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 (Nov 12 2022 at 13:58):

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 (Nov 12 2022 at 16:35):

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

Yaël Dillies (Nov 12 2022 at 19:08):

That unfortunately makes proofs longer and more brittle overall.

Scott Morrison (Nov 12 2022 at 21:49):

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 (Nov 12 2022 at 22:02):

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 (Nov 13 2022 at 10:30):

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 (Nov 13 2022 at 10:38):

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 (Nov 13 2022 at 10:42):

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 (Nov 13 2022 at 10:44):

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

Yaël Dillies (Nov 13 2022 at 10:44):

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 (Nov 13 2022 at 10:44):

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

Patrick Johnson (Nov 13 2022 at 10:51):

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 (Nov 13 2022 at 11:03):

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 (Nov 13 2022 at 11:26):

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 (Nov 15 2022 at 14:15):

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 (Nov 15 2022 at 14:17):

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 (Nov 15 2022 at 14:23):

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 (Nov 15 2022 at 14:25):

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 (Nov 15 2022 at 14:26):

It is obvious to me, yes.

Martin Dvořák (Nov 15 2022 at 14:27):

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 (Nov 15 2022 at 14:27):

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 (Nov 15 2022 at 14:32):

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 (Nov 15 2022 at 14:32):

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 (Nov 15 2022 at 14:32):

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

Eric Wieser (Nov 15 2022 at 14:32):

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 (Nov 15 2022 at 15:37):

Surely the rw make the proof more fragile?

Martin Dvořák (Nov 15 2022 at 15:41):

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

Eric Wieser (Nov 15 2022 at 15:43):

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


Last updated: Dec 20 2023 at 11:08 UTC