Skip to Main content Skip to Navigation
Journal articles

A Case Study in Formalizing Projective Geometry in Coq: Desargues Theorem

Abstract : Formalizing geometry theorems in a proof assistant like Coq is challenging. As emphasized in the literature, the non-degeneracy conditions lead to technical proofs. In addition, when considering higher-dimensions, the amount of incidence relations (e.g. point-line, point-plane, line-plane) induce numerous technical lemmas. In this article, we investigate formalizing projective plane geometry as well as projective space geometry. We mainly focus on one of the fundamental properties of the projective space, namely Desargues property. We formally prove it is independent of projective plane geometry axioms but can be derived from Pappus property in a two-dimensional setting. Regarding at least three dimensional projective geometry, we present an original approach based on the notion of rank which allows to describe incidence and non-incidence relations such as equality, collinearity and coplanarity homogeneously. This approach allows to carry out proofs in a more systematic way and was successfully used to formalize fairly easily Desargues theorem in Coq. This illustrates the power and efficiency of our approach (using only ranks) to prove properties of the projective space.
Document type :
Journal articles
Complete list of metadata

Cited literature [22 references]  Display  Hide  Download
Contributor : Julien Narboux Connect in order to contact the contributor
Submitted on : Tuesday, January 24, 2012 - 4:33:50 PM
Last modification on : Tuesday, December 8, 2020 - 10:16:47 AM
Long-term archiving on: : Wednesday, April 25, 2012 - 2:46:16 AM


Files produced by the author(s)




Nicolas Magaud, Julien Narboux, Pascal Schreck. A Case Study in Formalizing Projective Geometry in Coq: Desargues Theorem. Computational Geometry, Elsevier, 2012, Special Issue on geometric reasoning, 45 (8), pp.406-424. ⟨10.1016/j.comgeo.2010.06.004⟩. ⟨inria-00432810v2⟩



Record views


Files downloads