Donald Sebastian Leung (Mar 01 2020 at 07:36):
I've been working on formalizing incidence geometry in Lean as an exercise and came across the following question: when we say that a set of points are collinear, do they necessarily have to be distinct?
Donald Sebastian Leung (Mar 01 2020 at 07:39):
Also, does it make sense to say that zero points or one point is/are (trivially) collinear?
Kevin Buzzard (Mar 01 2020 at 07:39):
That's all up to the person who is using those words.
Donald Sebastian Leung (Mar 01 2020 at 07:40):
Thanks, so I suppose it's fine either way?
Kevin Buzzard (Mar 01 2020 at 07:42):
I guess if I were using these words I would be clear about what I meant in these edge cases
Reid Barton (Mar 01 2020 at 15:17):
If you literally have a
set of points, then its members are distinct by definition
Patrick Massot (Mar 01 2020 at 15:18):
My usual message every time someone mentions that formalization project: if you are serious about it, you should have a look at https://geocoq.github.io/GeoCoq/
Reid Barton (Mar 01 2020 at 16:29):
And GeoCoq is also a cautionary example of how hard the kind of issues you are asking about are: their definition of orthocenter is wrong (a right triangle has no orthocenter according to their definition, while the orthocenter should be defined as the vertex at the right angle) because of a definition of orthogonality which excludes certain points from being equal.
Patrick Massot (Mar 01 2020 at 16:29):
Did you just noticed that issue?
Patrick Massot (Mar 01 2020 at 16:30):
Or was it discussed somewhere else?
Reid Barton (Mar 01 2020 at 16:33):
It was discussed before but possibly not on a public Zulip stream
Patrick Massot (Mar 01 2020 at 16:33):
Did you discuss it with the authors of GeoCoq?
Reid Barton (Mar 01 2020 at 16:33):
Patrick Massot (Mar 01 2020 at 16:35):
I think this story is surprising, I'd be curious to know what they think about it.
Patrick Massot (Mar 01 2020 at 16:36):
I'll tell Julien Narboux he should come here.
Julien Narboux (Mar 01 2020 at 17:28):
You are right our definition is wrong, because it does not include the case of the right triangle ! thank you for pointing this. It has to be noted that we even proved Lemma orthocenter_per : ∀ A B C H, Per A B C →is_orthocenter H A B C → H=B. without noticing that the hypotheses imply False !
The orthocenter is not used much in GeoCoq, I guess by using it more we would have detected this error.
Julien Narboux (Mar 01 2020 at 17:32):
Our are right that giving good definitions is not always as trivial as it looks. My favorite example of this is the definition of a point being inside an angle. if you say that a point P is inside an angle ABC if there are points X and Y such that P belongs to segment XY: this definition works nicely in euclidean geometry, but does not work in neutral geometry. This confusion led to a flawed proof by Legendre of the parallel postulate.
Julien Narboux (Mar 01 2020 at 17:35):
About collinearity, we have in GeoCoq, a predicate Col taking only three points as input, and Col A A B holds. Then we have a tactic to deal with pseudo-transitivity of collinearity: A<>B -> Col A B P -> Col A B Q -> Col A B R -> Col P Q R. I think it is convenient to allow in the definition of Col equal points because in many case you do not know if the point are distinct.
In education, and in the Elements, there is some kind of implicit assumptions that points are in general position, but when you do it in Coq, you have a lot of problems with degenerated cases.
Donald Sebastian Leung (Mar 02 2020 at 02:32):
Thanks @Reid Barton and @Julien Narboux for your input (and thanks @Patrick Massot for mentioning GeoCoq). On a note related to incorrectly formalizing definitions, I think I read somewhere that Andrew W. Appel formalized a predicative type system and proved its soundness (in Coq) and even published a paper on it that got accepted, but only later realized that he wanted an impredicative type system when trying to integrate it into part of a larger research project. It's interesting how one can trip up on definitions despite being well-trained in formal methods.
Patrick Massot (Mar 02 2020 at 08:09):
I have a question for Julien. I one hour, I'll be teaching my geometry class for future school teachers. I'll "prove" that every simple polygon can be triangulated without adding interior vertices (and then deduce the formula for the sum of angles of polygons). Each time I've explained this since I started formalized math I feel guilty (thinking I would have a very hard time formalizing this proof). Is this formalized in GeoCoq?
Julien Narboux (Mar 02 2020 at 08:22):
Patrick, no it is not formalized in GeoCoq. I think, Harrison has formalized the fact that simple polygon can be triangulated without adding interior vertices in HOL light for the proof of Pick's theorem. We worked on Pick's theorem in Coq a long time ago with a student but we never finished the formalization.
Julien Narboux (Mar 02 2020 at 08:23):
Moreover, it is funny because the proof that the sum of angles of a triangle is 180° is one of the examples I give to explain that proofs given in high-school and in textbooks, often "read facts from the figure". See https://dpt-info.u-strasbg.fr/~narboux/slides/slides_toulouse.pdf near slide 18.
Julien Narboux (Mar 02 2020 at 08:28):
The usual proof of the sum of angles of a just a triangle, is to consider the parallel line to one side going through the third vertex. And then, from the fact that we have alternate angles, we can conclude that the sum is 180°. But doing it formally requires some work , I wrote a short (unpublished) note about this a few years ago: https://www.overleaf.com/read/xxzrndcfycfy
Patrick Massot (Mar 02 2020 at 13:16):
I know the triangle case is already based on pure cheating. I learned that from Arsac's book a long time ago.
Patrick Massot (Mar 02 2020 at 13:18):
Your Toulouse slides are really nice. On Page 63 you can add "Orsay (Lean)" next to Nijmegen and Nice.
Last updated: May 18 2021 at 08:14 UTC