This page describe a formalization of geometry using the Coq proof assistant. It contains both proofs about the foundations of geometry and high-level proofs in the same style as in high-school. About
ContentYou can browse the Coq files from the index of everything, or you can see some specific parts.
The axiom systemsThere are several ways to define the foundations of geomety:
- a synthetic approach
- Hilbert's axioms: points, lines, planes + geometric axioms
- Tarski's axioms: points + geometric axioms
- Euclid's axioms
- an analytic approach (starting from a given field 𝔽 (usually ℝ) and defining the plane as 𝔽n),
- mixed analytic/synthetic approaches assuming both a
field and some geometric axioms:
- area method: start field a field for measure signed distance and areas + geometric axioms
- Birkoff's style axiom system: start with a field for measuring distance and angles + geometric axioms
- approaches based on group of transformations (Erlangen progam)...
The formalization based on Tarski's axiomsWanda Szmielew and Alfred Tarski started the project of a treaty about the foundations of geometry. A systematic development of euclidean geometry based on Tarski's axioms was supposed to constitute the first part, but the early death of Wanda Szmielew put an end to this project. Finally, Wolfram Schwabhäuser continued the project of Wanda Szmielew and Alfred Tarski. He published the treaty in 1983 in German : Metamathematische Methoden in der Geometrie.
The main part of this development consists in the formalization of the first part of this book.
- Ch. 02 congruence properties
- Ch. 03 between properties
- Ch. 04 congruence between properties
- Ch. 04 collinearity
- Ch. 05 between transitivity le
- Ch. 06 out lines
- Ch. 07 midpoint
- Ch. 08 orthogonality
- Ch. 09 planes
- Ch. 10 line reflexivity 2D
- Ch. 10 line reflexivity
- Ch. 11 angles
- Ch. 12 parallelism
- Ch. 12 parallelism using intersection decidability
- Ch. 13 Synthetic proofs of the theorems of Pappus and Desargues.
- Ch. 13.1
- Ch. 13.2 length Length defined as an equivalence class using the Congruence predicate.
- Ch. 13.3 angles Angle measure defined as an equivalence class using the angle congruence predicate.
- Ch. 13.4 cos
- Ch. 13.5 Pappus-Pascal
- Ch. 13.6 Desargues Hessenberg's proof that Pappus implies Desargues.
- Ch. 14 Arithmetization of geometry
- Ch. 15 Lengths Definition of the length of a segment using coordinates, definition of length comparison using coordinates, proof that these definitions corresponds to their geometric counterparts,
- Ch. 16 Coordinates Proof of the formulas to characterize the congruence, betweeness, collinearity, and midpoint predicates using coordinates.
- Ch. 16 extension Instanciation of ordered field structures and connection to the
nsatztactic to obtain proof automatically using Gröbner basis.
Formalization of Euclid's Elements
- The first approach consists in formalizing Euclid's statement without trying to formalize the original proofs. Then we can try to minimize the assumptions. For example, we have formalized Gupta's proof that midpoint can be constructed without circle/circle continuity axioms, whereas the original proof by Euclid needs this assumption. We gather Euclid's statements formalized using this approach here. Export to html with GeoGebra figures is here.
- The second approach consists in trying to formalize the original proofs. This is not completly possible because Euclid's proofs contain some gaps, but it can be done to some extend by introducing the missing axioms and reordering some proofs. The formalization of first book of the Elements has been completed by Michael Beeson and then exported to Coq. The details are given in this paper. These proofs have also been exported to Hol-Light, see the webpage of this project. The Coq formalization consists of:
Connection with Hilbert's axiomsthis paper. We also proved that Tarski's axioms follow from Hilbert's axioms.
- Tarski to Hilbert A proof that Hilbert's axioms (without continuity) follows from Tarski's axioms.
- Hilbert to Tarski A proof that Tarski's axioms (without continuity) follows from Hilbert's axioms.
Variants of Tarski's axiom system
- Tarski to Makarios The formalization of a short paper by Makarios which shows that by slightly changing an axiom we can delete another axiom.
- Tarski to Beeson The proof that the constructive axiom system proposed by Beeson is classicaly equivalent to Tarski's axiom system.
Parallel postulatesWe prove the equivalence between several versions of the parallel postulate including the well known Playfair's postulate, and Euclid's 5th postulate. The details are in this paper.
- Definition of several versions of the parallel postulate.
- The equivalences theorems summarizing the results.
High level theoremsTo give a demonstration of the library and of the tactics, we prove some classical results of high-school geometry.
- Midpoints theorems
- Midpoint Thales theorem
- Varignon's theorem
- Quadrilaterals and Quadrilaterals with inter dec Definition of some quadrilaterals and their properties.
- Orthocenter theorem
- Circumcenter theorem
- Gravity center theorem
- Incenter theorem
- Euler line
ForumIf you seek help about GeoCoq please using the following forum:
LicenceThe code is released under the terms of the LGPL version 3.0.
How to installWe are working on a proper documentation, please contact us if you need help.
Manual installationTo use this library, first you need to install Coq. We tested GeoCoq 2.3.0 using Coq versions 8.5pl3, 8.6.1 and 8.7beta. The previous versions are not supported. Then download and unpack the files, it will create a GeoCoq directory. In this directory, type
maketo compile the files, it will create some
.vofiles. It takes a while to compile (> 30 minutes).
Using opam pacakage managerYou can install both Coq and GeoCoq using opam. See the instructions here.
opam repo add coq-released https://coq.inria.fr/opam/released opam install -j4 -v coq-geocoq