Formalizing Desargues' theorem in Coq using ranks in Coq

Abstract : Formalizing geometry theorems in a proof assistant like Coq is challenging. As emphasized in the literature, the non-degeneracy conditions leads 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 paper, 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. It allows to carry out proofs in a more systematic way. To validate this approach, we formalize in Coq (using only ranks) one of the fundamental theorems of the projective space, namely Desargues' theorem.
Type de document :
Communication dans un congrès
24th Annual ACM Symposium on Applied Computing, Mar 2009, Honolulu, United States. ACM, pp.1110-1115, 2009, Proceedings of SAC 2009. 〈10.1145/1529282.1529527〉
Liste complète des métadonnées

https://hal.inria.fr/inria-00335719
Contributeur : Julien Narboux <>
Soumis le : jeudi 30 octobre 2008 - 14:24:03
Dernière modification le : jeudi 11 janvier 2018 - 06:20:29
Document(s) archivé(s) le : lundi 7 juin 2010 - 18:56:01

Fichier

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

Identifiants

Collections

Citation

Nicolas Magaud, Julien Narboux, Pascal Schreck. Formalizing Desargues' theorem in Coq using ranks in Coq. 24th Annual ACM Symposium on Applied Computing, Mar 2009, Honolulu, United States. ACM, pp.1110-1115, 2009, Proceedings of SAC 2009. 〈10.1145/1529282.1529527〉. 〈inria-00335719〉

Partager

Métriques

Consultations de la notice

114

Téléchargements de fichiers

79