Coding style – splitting long proofs

Stream: new members

[Martin Dvořák]

Soft question (coding style):

Do you split long proofs into several lemmata just because the proof is too long? Even if they aren't logically independent pieces by using only a small subset of the propositions that are present inside the proof?

[Jireh Loreaux]

For mathlib, I would say "generally not." However, unless the proof is about a deep result, there is often a way to split it up into pieces, even if it means a major rewrite, or using other parts of the library better. That being said, there can always be exceptions to both statements above.

[Mario Carneiro]

One reason to split up a large proof is if it improves compile times

[Mario Carneiro]

lemmas are processed in parallel, and additionally a long proof can involve a large local context which makes all other tactics slower

[Mario Carneiro]

it's also just easier to work with when you are writing the proof since the response time is smaller

[Mario Carneiro]

that last reason is probably the most direct reason to split a long proof, it just gets too annoying to write otherwise

[Martin Dvořák]

I think I made a mistake that I was taking only the logical structure into account but not the length of the respective parts. I made a few levels of decomposition, after which I basically stopped breaking things apart. As a result, I have a proof that consists of 36 lemmata; many of them are under 10 lines, but some of them are longer, and one of them is a monstrous lemma with a proof of 1100 lines.

The response time cries in Lean was really annoying.

[Jireh Loreaux]

A proof of 1100 lines is certainly a good enough reason to split it. Are you sure that lemma can't be deconstructed further? It seems very surprising to me. We have a few long proofs in mathlib, but I'm not sure I know of any that are over say, 200 lines [other community members please insert links to counterexamples here].

[Mario Carneiro]

I think there are counterexamples, but I generally associate ultra-long proofs with folks who haven't quite learned the coding style yet

[Mario Carneiro]

It would be nice if someone could do some statistics on mathlib proof length distribution and outliers

[Mario Carneiro]

unfortunately environment.decl_pos only has the start position and not the end

[Martin Dvořák]

Jireh Loreaux said:

A proof of 1100 lines is certainly a good enough reason to split it. Are you sure that lemma can't be deconstructed further? It seems very surprising to me. We have a few long proofs in mathlib, but I'm not sure I know of any that are over say, 200 lines [other community members please insert links to counterexamples here].

It can be. I just made a mistake that I stopped after a few levels of decomposition.

[Martin Dvořák]

After which I was splitting things only if they were using only a small subset of propositions in the place where they were used.

[Martin Dvořák]

Mario Carneiro said:

(...) folks who haven't quite learned the coding style yet

Yep, this is me!

[Jireh Loreaux]

@Mario Carneiro As a first approximation, you could just subtract successive environment.decl_pos values. It wouldn't be accurate because of variable declarations, section headings, but I think only really long docstrings would feed into the outliers, and these might be small enough in number to discard manually.

[Mario Carneiro]

I just wrote a fix for lean so that the .ast.json stores command ends correctly, so if we update lean and run it on mathlib we can get accurate data here

[Mario Carneiro]

lean#756