Long proofs

Stream: new members

[Antoine Chambert-Loir]

I need style advice about writing long proofs.
Imagine there is a case disjunction, should one write each of them as a separate lemma?
Passing all needed variables (but not more), although sometimes that could make a lot of them?
In mathlib, it seems that a lot of the initial lemmas have 1-line proofs, but more complicated stuff has rarely more than 20 lines.
(The proof I'm in already makes more than 100 lines…)

[Kevin Buzzard]

Long proofs are rubbish because after you've written 100 lines, you have to wait 5 seconds for the orange bars to go every time you press a key. I tend to factor out as much as possible because of this. An alternative is to finish a subgoal proof, and then comment out the proof and replace it with sorry and then just unsorry everything at the end.

[Eric Taucher]

Antoine Chambert-Loir said:

I need style advice about writing long proofs.

The latest community blog talks about such.

[Eric Wieser]

If you extract a lemma from a long proof, you should spend some time trying to generalize that lemma; after thinking about the generalization, often you find mathlib already has that more general form

[Yaël Dillies]

Eric Taucher said:

The latest community blog talks about such.

Ahah! I can now preemptively answer questions.

[Sebastien Gouezel]

Working with long proofs is perfectly fine if you sorry out long subproofs once they are completed, to keep a reasonable compile time. After the fact, you can try to factor out some lemmas if it makes sense, or if the proof takes too long to compile. I've definitely written proofs of more than 200 lines in mathlib.

[Kyle Miller]

Kevin Buzzard said:

Long proofs are rubbish because after you've written 100 lines, you have to wait 5 seconds for the orange bars to go every time you press a key. I tend to factor out as much as possible because of this.

I like how this technical limitation incentivizes doing things "right." It's very rare that there's some large proof that can't be meaningfully subdivided into useful pieces. Though, I don't like how it makes it harder to write the proof the "wrong" way as a prototype (sorry and comment is a good trick -- maybe that should be an editor command where you can select text and have it toggle between text and sorry/-text-/).

It would be nice if Lean could remember tactic state for each line of a file so that, when you make a change, it continues from the last unchanged line's state. It seems complicated to implement, but not impossible.

[Alex J. Best]

The easiest way I've found is not to comment lines at all, hopefully if your proof is in { .. } blocks already you can just do

sorry; { rw blah,
  HUGE PROOF }

and only have to edit one line at a time

[Eric Wieser]

That's a great trick

[Eric Rodriguez]

can you explain what you mean with a fuller example? I don;'t think I get this

[Eric Wieser]

If you have a { foo, bar, baz} that is really slow, add sorry; before it to temporarily skip it so you can work on the rest of the proof more quickly

[Eric Rodriguez]

oh my god, because the ; applies to all created subgoals. that's brilliant

[Eric Wieser]

Right; and sorry creates no subgoals.

[Jujian Zhang]

(deleted)