GeoCoq/GeoCoq v2.3.0

Euclid's Elements Release

on GitHub

This new release of GeoCoq (2.3.0) mainly brings formalizations of Euclid's Elements and proofs about continuity properties.

GeoCoq contains two different approaches for the formalization of Euclid's Elements:

1. The first approach consists in formalizing Euclid's statements without trying to formalize the original proofs. In this approach we 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 continuity assumption because it is based on the construction of the perpendicular bisector. Based on all the proofs developed in previous versions of GeoCoq and also new proofs by Gabriel Braun, we gathered Euclid's statements formalized using this approach in the directory

   Elements/Statements

2. The second approach consists in trying to formalize the original proofs of Euclid. This is not completely 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 by Julien Narboux. The details are given in this paper. These proofs have also been exported to Hol-Light, see the webpage of this project.
   The code is availble in the directory

   Elements/OriginalProofs

Some links between different continuity properties have been obtained. We study the circle/circle, circle/line, Dedekind cuts, first-order Dedekind cuts, and Archimedes' axiom. This work is described (in french) in the internship report of Charly Gries.

Changelog:

• This release is compatible with Coq 8.5, 8.6 and trunk.
• Coq translation of Michael Beeson's formalization of the 48 propositions of Book 1 of Euclid's Elements, those proofs try to mimic Euclid's proofs as much as possible but are based on a richer axiom system than Tarski's.
• An axiom system for Euclid's Elements proofs and some links with Tarski's axiom system.
• Files grouping Euclid's Elements Propositions for which we have a proof based on Tarski's axioms: Book I Prop 1-34 and 46-47, Book III Prop 2-14 17-18
• Definition of the sum of segments and related proofs.
• Definition of elementary continuity properties: segment-circle, line-circle, circle-circle continuity properties.
• Definition of first-order Dedekind cut axiom, and Dedekind cut axiom.
• Proof that Archimedes axiom can be derived from Dedekind axiom.
• Proof of the equivalence between different variants of circle-circle continuity.
• Proof of the equivalence between different variants of line-circle, and segment-circle continuity.
• Proof that line-circle continuity can be derived from circle-circle continuity.
• Proof that circle-circle continuity can be derived from first-order Dedekind cuts.
• Add a new version of the parallel postulate and the equivalence proofs.
• Add definitions of predicate to express that a point is inside, on and outside a circle, and associated lemmas.
• Add some properties about tangents.
• Add some results about half of angles.