Collinear in incidence geometry

Stream: maths

[Donald Sebastian Leung]

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]

Also, does it make sense to say that zero points or one point is/are (trivially) collinear?

[Kevin Buzzard]

That's all up to the person who is using those words.

[Donald Sebastian Leung]

Thanks, so I suppose it's fine either way?

[Kevin Buzzard]

I guess if I were using these words I would be clear about what I meant in these edge cases

[Reid Barton]

If you literally have a set of points, then its members are distinct by definition

[Patrick Massot]

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]

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]

Did you just noticed that issue?

[Patrick Massot]

Or was it discussed somewhere else?

[Reid Barton]

It was discussed before but possibly not on a public Zulip stream

[Patrick Massot]

Did you discuss it with the authors of GeoCoq?

[Reid Barton]

No

[Patrick Massot]

I think this story is surprising, I'd be curious to know what they think about it.

[Patrick Massot]

I'll tell Julien Narboux he should come here.

[Julien Narboux]

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]

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]

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]

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]

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]

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]

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]

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]

I know the triangle case is already based on pure cheating. I learned that from Arsac's book a long time ago.

[Patrick Massot]

Your Toulouse slides are really nice. On Page 63 you can add "Orsay (Lean)" next to Nijmegen and Nice.