research-article

Formalizing Desargues' theorem in Coq using ranks

Authors:

Nicolas Magaud,

Julien Narboux,

Pascal SchreckAuthors Info & Claims

SAC '09: Proceedings of the 2009 ACM symposium on Applied Computing

Pages 1110 - 1115

https://doi.org/10.1145/1529282.1529527

Published: 08 March 2009 Publication History

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.

References

[1]

Y. Bertot and P. Castéran. Interactive Theorem Proving and Program Development, Coq'Art: The Calculus of Inductive Constructions. Springer, 2004.

Digital Library

[2]

M. Bezem and D. Hendriks. On the Mechanization of the Proof of Hessenberg's Theorem in Coherent Logic. J. of Automated Reasoning, 40(1): 61--85, 2008.

Digital Library

[3]

J. Brandt and K. Schneider. Using three-valued logic to specify and verify algorithms of computational geometry. In ICFEM, volume 3785 of LNCS, pages 405--420. Springer-Verlag, 2005.

Digital Library

[4]

F. Buekenhout, editor. Handbook of Incidence Geometry. North Holland, 1995.

[5]

S.-C. Chou, X.-S. Gao, and J.-Z. Zhang. Machine Proofs in Geometry. World Scientific, 1994.

[6]

Coq development team. The Coq Proof Assistant Reference Manual, Version 8.2. LogiCal Project, 2008.

[7]

H. S. M. Coxeter. Projective Geometry. Springer, 1987.

[8]

C. Dehlinger, J.-F. Dufourd, and P. Schreck. Higher-Order Intuitionistic Formalization and Proofs in Hilbert's Elementary Geometry. In ADG'00, volume 2061 of LNAI, pages 306--324. Springer-Verlag, 2000.

Digital Library

[9]

J.-C. Filliâtre and P. Letouzey. Functors for Proofs and Programs. In ESOP'2004, volume 2986 of LNCS, pages 370--384. Springer-Verlag, 2004.

[10]

F. Guilhot. Formalisation en Coq et visualisation d'un cours de géométrie pour le lycée. TSI, 24: 1113--1138, 2005. In french.

[11]

C. M. Hoffmann and R. Joan-Arinyo. Handbook of Computer Aided Geometric Design, chapter Parametric Modeling, pages 519--541. Elsevier, 2002.

[12]

C. Jermann, G. Trombettoni, B. Neveu, and P. Mathis. Decomposition of geometric constraint systems: a survey. International J. of Computational Geometry and Application, 16(5--6): 379--414, 2006.

[13]

E. Kusak. Desargues theorem in projective 3-space. J. of Formalized Mathematics, 2, 1990.

[14]

N. Magaud, J. Narboux, and P. Schreck. Formalizing Projective Plane Geometry in Coq. accepted for presentation at ADG'08, September 2008.

Digital Library

[15]

L. Meikle and J. Fleuriot. Formalizing Hilbert's Grundlagen in Isabelle/Isar. In Theorem Proving in Higher Order Logics, pages 319--334, 2003.

[16]

D. Michelucci, S. Foufou, L. Lamarque, and P. Schreck. Geometric constraints solving: some tracks. In SPM '06, pages 185--196. ACM Press, 2006.

Digital Library

[17]

D. Michelucci and P. Schreck. Incidence Constraints: a Combinatorial Approach. International J. of Computational Geometry and Application, 16(5--6): 443--460, 2006.

[18]

J. Narboux. A decision procedure for geometry in Coq. In TPHOLs'04, volume 3223 of LNCS, pages 225--240. Springer-Verlag, 2004.

[19]

J. Narboux. Mechanical theorem proving in Tarski's geometry. In ADG'06, volume 4869 of LNAI, pages 139--156. Springer-Verlag, 2007.

Digital Library

[20]

P. Schreck. Robustness in CAD Geometric Construction. In IV'01, pages 111--116, London, 2001.

Digital Library

Cited By

Braun DMagaud NSchreck P(2019)Two cryptomorphic formalizations of projective incidence geometryAnnals of Mathematics and Artificial Intelligence10.1007/s10472-018-9604-z85:2-4(193-212)Online publication date: 1-Apr-2019
https://dl.acm.org/doi/10.1007/s10472-018-9604-z
Quaresma P(2017)Towards an Intelligent and Dynamic Geometry BookMathematics in Computer Science10.1007/s11786-017-0302-811:3-4(427-437)Online publication date: 25-Apr-2017
https://doi.org/10.1007/s11786-017-0302-8
Haftmann FKaliszyk CNeuper W(2010)CTP-based programming languages?ACM Communications in Computer Algebra10.1145/1838599.183862144:1/2(27-41)Online publication date: 29-Jul-2010
https://dl.acm.org/doi/10.1145/1838599.1838621
Show More Cited By

Index Terms

Formalizing Desargues' theorem in Coq using ranks

Recommendations

A case study in formalizing projective geometry in Coq: Desargues theorem

Formalizing geometry theorems in a proof assistant like Coq is challenging. As emphasized in the literature, the non-degeneracy conditions lead to long technical proofs. In addition, when considering higher-dimensions, the amount of incidence relations (...
Formalizing projective plane geometry in Coq
ADG'08: Proceedings of the 7th international conference on Automated deduction in geometry

We investigate how projective plane geometry can be formalized in a proof assistant such as Coq. Such a formalization increases the reliability of textbook proofs whose details and particular cases are often overlooked and left to the reader as ...
Completeness and decidability of converse PDL in the constructive type theory of Coq
CPP 2018: Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs

The completeness proofs for Propositional Dynamic Logic (PDL) in the literature are non-constructive and usually presented in an informal manner. We obtain a formal and constructive completeness proof for Converse PDL by recasting a completeness proof ...

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences

SAC '09: Proceedings of the 2009 ACM symposium on Applied Computing

March 2009

2347 pages

ISBN:9781605581668

DOI:10.1145/1529282

Conference Chairs:
Sung Y. Shin
South Dakota State University, United States
,
Sascha Ossowski
University Rey Juan Carlos, Spain

Copyright © 2009 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

SIGAPP: ACM Special Interest Group on Applied Computing

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 08 March 2009

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

SAC09

Sponsor:

SIGAPP

SAC09: The 2009 ACM Symposium on Applied Computing

March 8, 2009 - March 12, 2008

Hawaii, Honolulu

Acceptance Rates

Overall Acceptance Rate 1,650 of 6,669 submissions, 25%

Upcoming Conference

SAC '25

Sponsor:
sigapp

The 40th ACM/SIGAPP Symposium on Applied Computing

March 31 - April 4, 2025

Catania , Italy

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

9
Total Citations
View Citations
108
Total Downloads

Downloads (Last 12 months)1
Downloads (Last 6 weeks)0

Reflects downloads up to 03 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

Braun DMagaud NSchreck P(2019)Two cryptomorphic formalizations of projective incidence geometryAnnals of Mathematics and Artificial Intelligence10.1007/s10472-018-9604-z85:2-4(193-212)Online publication date: 1-Apr-2019
https://dl.acm.org/doi/10.1007/s10472-018-9604-z
Quaresma P(2017)Towards an Intelligent and Dynamic Geometry BookMathematics in Computer Science10.1007/s11786-017-0302-811:3-4(427-437)Online publication date: 25-Apr-2017
https://doi.org/10.1007/s11786-017-0302-8
Haftmann FKaliszyk CNeuper W(2010)CTP-based programming languages?ACM Communications in Computer Algebra10.1145/1838599.183862144:1/2(27-41)Online publication date: 29-Jul-2010
https://dl.acm.org/doi/10.1145/1838599.1838621
Janičić PNarboux JQuaresma P(2010)The Area MethodJournal of Automated Reasoning10.1007/s10817-010-9209-748:4(489-532)Online publication date: 16-Nov-2010
https://doi.org/10.1007/s10817-010-9209-7
Michelucci D(2010)Some lemmas to hopefully enable search methods to find short and human readable proofs for incidence theorems of projective geometryProceedings of the 8th international conference on Automated Deduction in Geometry10.1007/978-3-642-25070-5_7(118-131)Online publication date: 22-Jul-2010
https://dl.acm.org/doi/10.1007/978-3-642-25070-5_7
Fuchs LThéry L(2010)A formalization of grassmann-cayley algebra in COQ and its application to theorem proving in projective geometryProceedings of the 8th international conference on Automated Deduction in Geometry10.1007/978-3-642-25070-5_3(51-67)Online publication date: 22-Jul-2010
https://dl.acm.org/doi/10.1007/978-3-642-25070-5_3
Stojanović SPavlović VJaničić P(2010)A coherent logic based geometry theorem prover capable of producing formal and readable proofsProceedings of the 8th international conference on Automated Deduction in Geometry10.1007/978-3-642-25070-5_12(201-220)Online publication date: 22-Jul-2010
https://dl.acm.org/doi/10.1007/978-3-642-25070-5_12
Scott PFleuriot J(2010)An investigation of hilbert's implicit reasoning through proof discovery in idle-timeProceedings of the 8th international conference on Automated Deduction in Geometry10.1007/978-3-642-25070-5_11(182-200)Online publication date: 22-Jul-2010
https://dl.acm.org/doi/10.1007/978-3-642-25070-5_11
Magaud NNarboux JSchreck P(2008)Formalizing projective plane geometry in CoqProceedings of the 7th international conference on Automated deduction in geometry10.5555/2008257.2008265(141-162)Online publication date: 22-Sep-2008
https://dl.acm.org/doi/10.5555/2008257.2008265

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Figures

Tables

Media

View Table of Conten