# 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

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

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

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.

- 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
`nsatz`

tactic to obtain proof automatically using GrÃ¶bner basis.

## Formalization of 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

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