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

https://hal.inria.fr/inria-00335719
Contributor : Julien Narboux <>
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

File

desargues.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

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⟩

Share

Metrics

Record views

401

Files downloads

808