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.
Type de document :
Article dans une revue
Computational Geometry, Elsevier, 2012, Special Issue on geometric reasoning, 45 (8), pp.406-424. 〈10.1016/j.comgeo.2010.06.004〉
Liste complète des métadonnées

Littérature citée [22 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00432810
Contributeur : Julien Narboux <>
Soumis le : mardi 24 janvier 2012 - 16:33:50
Dernière modification le : jeudi 11 janvier 2018 - 06:22:39
Document(s) archivé(s) le : mercredi 25 avril 2012 - 02:46:16

Fichier

desargues-resubmitted.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

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〉

Partager

Métriques

Consultations de la notice

174

Téléchargements de fichiers

440