Beautiful proof

Stream: general

[Jacques Carette]

I was leafing through the category_theory library, when I ran across this absolutely beautiful proof:
https://github.com/leanprover-community/mathlib/blob/2a8d7f3e1e79646b2cc914c477f060123d871a25/src/category_theory/equivalence.lean#L126-L134

Question: why isn't this equational style used more often?

[Kevin Buzzard]

because most proofs can't be written in this manner? :-(

[Ruben Van de Velde]

It's really nice - when it works, and the justifications for each step fit on a single line; it's somewhat less pretty otherwise. I suspect that may have something to do with it as well

[Reid Barton]

Interestingly this particular definition used to be written in a more compact style: https://github.com/leanprover-community/mathlib/commit/5e5298b9273b44aa06e3b30aa064cf866cd8152a
It was changed to add explicit unitor isomorphisms to reduce the dependence on definitional equality, and at the same time changed to calc style.

[Jacques Carette]

@Kevin Buzzard I'm currently (and for many months now) formalizing category theory, where pretty much all proofs are of this kind, because they are all diagram chases. There are a couple hundred such proofs in agda-categories. Some of my other work on generalized folds also can have all the proofs written that way.

This isn't a contradiction to your statement. Just that I expected so see more of that in category_theory.

Also, in Agda, because of dependent pattern matching, most proofs by cases / induction, are done "on the left", so that the right hand side frequently can become equational. It's interesting how the underlying features enable different proof styles.

@Reid Barton definitional equality is very interesting. Inside proofs, I likewise avoid relying on it. But you can't get away with that for various theorem statements. We've had to adjust various definitions in agda-categories so that various constructions were such that "op op" was definitionally nothing (a 'no-op'...). Various theorems in CT became awful monsters without that; still true, just a lot more convoluted.

[Reid Barton]

For proofs the rw/simp style is a lot more concise, and can potentially be automated completely.

[Reid Barton]

most proofs by cases / induction, are done "on the left", so that the right hand side frequently can become equational

What do you mean by this?

[Jacques Carette]

@Reid Barton I mean that a case proof in Lean usually ends up being done by a (dependent) pattern-match in Agda, where you get a new case for your proof-function. Because the dependent pattern-match has exposed a lot of new information (in exactly the same way that case does), the rhs proof is much simpler. In constructive settings, I've found that after a bit of reduction, a lot of the proofs that I need to do are then equational in nature. This is by no means a universal!

I guess I have been proving a whole lot of "X is equivalent to Y" type of theorems, so that surely has coloured my perception. [I did not realize that until now, so I'm happy that I have done so because of your question.]

Hmm, the vast majority of theorems in category theory boil down to "X is equivalent to Y". Even celebrated things like Yoneda and the Grothendieck construction first require a straightforward construction, and then some very thorny proof obligations that express that the construction really works, and really behaves nicely. All of which are diagram chases, i.e. 2D equations.