Formalizing Desargues' theorem in Coq using ranks

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Formalizing Desargues' theorem in Coq using ranks

Full text

Pdf (5.48 MB)

Source

Symposium on Applied Computing archive
Proceedings of the 2009 ACM symposium on Applied Computing table of contents

Honolulu, Hawaii

SESSION: Geometric constraints and reasoning track table of contents

Pages 1110-1115

Year of Publication: 2009

ISBN:978-1-60558-166-8

Authors

Nicolas Magaud	Université de Strasbourg
Julien Narboux	Université de Strasbourg
Pascal Schreck	Université de Strasbourg

Sponsor

SIGAPP: ACM Special Interest Group on Applied Computing

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 8, Downloads (12 Months): 24, Citation Count: 0

Additional Information:

abstract references index terms collaborative colleagues

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/1529282.1529527 What is a DOI?

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

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	Yves Bertot , Pierre Casteran, Interactive Theorem Proving and Program Development, SpringerVerlag, 2004
	2	Marc Bezem , Dimitri Hendriks, On the Mechanization of the Proof of Hessenberg's Theorem in Coherent Logic, Journal of Automated Reasoning, v.40 n.1, p.61-85, January 2008 [doi>10.1007/s10817-007-9086-x]
	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.
	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	Christophe Dehlinger , Jean-François Dufourd , Pascal Schreck, Higher-Order Intuitionistic Formalization and Proofs in Hilbert's Elementary Geometry, Revised Papers from the Third International Workshop on Automated Deduction in Geometry, p.306-324, September 25-27, 2000
	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.
	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	Dominique Michelucci , Sebti Foufou , Loic Lamarque , Pascal Schreck, Geometric constraints solving: some tracks, Proceedings of the 2006 ACM symposium on Solid and physical modeling, June 06-08, 2006, Cardiff, Wales, United Kingdom [doi>10.1145/1128888.1128915]
	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.
	20	Robustness in CAD Geometric Constructions, Proceedings of the Fifth International Conference on Information Visualisation, p.111, July 25-27, 2001