Logo
    GeoCoq GeoCoq

A formalization of foundations of geometry in Coq

View project on GitHub

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)...
We use here a synthetic approach but following Descartes and Tarski we prove that we can define coordinates.
Our main axiom system is the one of Tarski, but we define also Hilbert's axiom system and a version of Euclid's axioms sufficient to prove the propositions in Book 1 of the Elements. We prove that Tarski's axioms (except continuity) are equivalent to Hilbert's axioms (except continuity).

The formalization based on Tarski's axioms

Alfred Tarski 1968
Tarski
In the early 60s, Wanda 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.
SST Book

Formalization of Euclid's Elements

Euclid's Elements
Regarding the formalization of Euclid's Elements, GeoCoq contains two different approaches:
  • 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

Hilbert
Grundlagen der Geometrie
Most of the axioms of Hilbert are implicitely proved in the book, but we explicit all the proofs here. We define lines by couple of points... This work is described in this 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 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.

High level theorems

To give a demonstration of the library and of the tactics, we prove some classical results of high-school geometry.
Circumcenter theorem
Euler line

Contributors

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