Zulip Chat Archive

Stream: general

Topic: Beautiful proof


Jacques Carette (Aug 17 2020 at 13:22):

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 (Aug 17 2020 at 13:44):

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

Ruben Van de Velde (Aug 17 2020 at 13:44):

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 (Aug 17 2020 at 13:47):

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 (Aug 17 2020 at 14:43):

@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 (Aug 17 2020 at 14:53):

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

Reid Barton (Aug 17 2020 at 14:55):

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 (Aug 18 2020 at 13:26):

@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.


Last updated: Dec 20 2023 at 11:08 UTC