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
  • 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)...
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. 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

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.

Euclid's postulate

The version of Euclid's postulate as given in the book is not intuitive. We prove the equivalence between several versions of Euclid's 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 the development using Coq version 8.4pl6, 8.5pl3 and 8.6. The <=8.3 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.

Using opam pacakage manager

You can install both Coq and GeoCoq using opam. See the instructions here.
opam install -j4 -v coq-geocoq

Related papers

Related work