Mathlib style: generalizations and multiple proofs

Stream: mathlib4

[mdnestor]

In mathlib is it preferred to prove theorems via special cases of generalizations?

E.g. we have 1) Cantor's theorem for types proved at Function.cantor_surjective. However we could also 2) prove Lawvere's fixed point theorem in a general cartesian closed category and apply that to the category of types.

Is there a preference between these options? Do we keep both proofs?

[Violeta Hernández]

Note that Function.cantor_surjective is in Mathlib.Logic.Function.Basic, which is an extremely early import. The standard proof needs almost nothing other than the definition of surjectivity and the powerset Set α.

[Violeta Hernández]

I think having duplicate theorems is an issue to be avoided within Mathlib, but having multiple ways to prove them is an inevitability. Only when the new ways are simpler (in both conceptual terms and in terms of imports) should the old ones be replaced, though.

[Violeta Hernández]

Of course, even having duplicates in Mathlib is very difficult. Two very slightly different ways to state a result can sometimes take multiple lines of code for the conversion. So in that case the apparent duplication is fine.

[mdnestor]

That makes sense. Cantor's theorem for types is just a couple lines but proving it as a special case of Lawvere's theorem is much more involved.

I am working on formalizing a wellknown theorem with a short proof but I have also proved generalizations that depend on more abstractions. My current approach is to do both, 1) prove the theorem in the classic way and 2) prove the theorem using the generalization and append .proof2 to the name

[Yury G. Kudryashov]

When you're ready to PR, we can discuss which of the proofs should make it into the library.

[Yury G. Kudryashov]

E.g., lots of analysis is done in normed spaces, then specialized to dimension 1 as needed.