GeoCoq About
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.Content
You can browse the Coq files from the index of everything, or you can see some specific parts.The axiom systems
There 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
- Birkhoff'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 axioms
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. 14.1 Sum Geometric definition of the sum.
- Ch. 14.2 Product Geometric definition of the product.
- Ch. 14.3 Ordered. field All proofs necessary to obtain an ordered field.
- 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,
Pythagoras theorem,
Thales theorem. - 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 extent 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 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 postulates
We 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 theorems
To 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
Contributors
- Michael Beeson
- Pierre Boutry
- Gabriel Braun
- Roland Coghetto
- Charly Gries
- Julien Narboux
- Dan Song
Forum
If you seek help about GeoCoq please using the following forum:GeoCoq Group
Licence
The code is released under the terms of the LGPL version 3.0.How to install
We are working on a proper documentation, please contact us if you need help.Manual installation
To 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./configure and make to compile the
files, it will create some .vo files. It takes a while to compile (> 30 minutes).
Using opam pacakage manager
You 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
Related papers
Related work
- Larry Wos and Michael Beeson have studied Tarskian Geometry using Otter: An amazing approach to plane geometry and Finding Proofs in Tarskian Geometry.