Developments in the field of formal geometry
Incremental Convex Hull Algorithm in 2D
Christophe Brun, Jean-François Dufourd et Nicolas Magaud formalized a incremental algorithm to compute convex hulls of points in the plane. They use hypermaps as their data structure to represent objects and carried out the proofs using the Coq proof assistant.
Formal development (in gallina)
Jean-François Dufourd and Yves Bertot proposed a formal
description of an algorithm to transform an arbitrary
triangulation into a Delaunay triangulation by successive flips.
It is available here and is
verifiable with Coq-8.2, extended with csdp for the psatz tactic.
A port of this development for Coq-8.5 is
Formalizing a Discrete Model of the Continuum in Coq from a Discrete Geometry Perspective
Nicolas Magaud, Agathe Chollet and Laurent Fuchs currently work on a formalization of the Harthong-Reeb line in Coq. The Coq definitions and proofs are available here. It is a work in progress and shall be updated when new results are obtained.
Hypermaps, Genus theorem and Euler formula
Jean François Dufourd proposed a Coq development about hypermaps and the formalization of the Genus theorem and the Euler formula. It is available as a user contributions of Coq.
Laurent Fuchs and Laurent Théry proposed a Coq
development for Geometric Algebras.
Ruler and Compass geometry
Jean Duprat developed an axiom system for ruler and compass geometry. It is available as a user contribution of Coq.
This library contains an axiomatization of the ruler and compass euclidian geometry. Files A1 to A6 contain the axioms and the basic constructions. The other files build the proof that this axiomatization induces the whole plane geometry except the continuity axiom. For that the proofs of the Hilbert's axioms conclude this work in the files E1 to E5.
Frédérique Guilhot proposed a Coq development about high-school geometry in Coq. It is available as a user contributions of Coq or on her page.
Julien Narboux proposed a Coq development about Tarski's geometry in Coq. It is available as a user contributions of Coq or on his page.
Nicolas Magaud, Julien Narboux and Pascal Schreck proposed a Coq development about projective geometry in Coq. It is available as a user contributions of Coq or on this page.
- A prototype for interactive proof in geometry based on GeoGebra