Skip to Main content Skip to Navigation
Conference papers

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.
Document type :
Conference papers
Complete list of metadata
Contributor : Julien Narboux Connect in order to contact the contributor
Submitted on : Thursday, October 30, 2008 - 2:24:03 PM
Last modification on : Tuesday, December 8, 2020 - 9:51:07 AM
Long-term archiving on: : Monday, June 7, 2010 - 6:56:01 PM


Files produced by the author(s)




Nicolas Magaud, Julien Narboux, Pascal Schreck. Formalizing Desargues' theorem in Coq using ranks in Coq. 24th Annual ACM Symposium on Applied Computing, Xiao-Shan Gao, Robert Joan-Arinyo, Dominique Michelucci, Mar 2009, Honolulu, United States. pp.1110-1115, ⟨10.1145/1529282.1529527⟩. ⟨inria-00335719⟩



Record views


Files downloads