• This release is compatible, at the moment of the release, with Coq 8.10.0-8.19.1. Some files depends on mathcomp field library (1.11.0 <= version <= 1.19.0).
• Reorganization of files into directories that match the various subpackages of GeoCoq.
• Add the possibility to build with dune. This requires dune >= 3.8 so it is only compatible with Coq > 8.13.
• While the compilation time of the library decreased thanks to some performance improvements made by Coq, we also made GeoCoq compile faster.
• We formalized ten out of the eleven counter-models for planar geometry present in Gupta's thesis. For a few of them we did not yet mechanize the proof that the continuity axiom holds.
• We defined an alternative axiom system that, we believe, allows to obtain the arithmetization of n-dimensional geometry without relying on decidability properties.
• We formalized counter-models for this system, either by generalizing Gupta's ones or by inventing new ones. Up to the mechanization of the proofs that the proposed dimensional axioms hold in some counter-models, we have the same results as for planar geometry.

• Add compatibility with Coq 8.10-11.
• Proof that Greenberg's axiom implies Aristotle's axiom.
• Proof that the conjunction of Archimedes' axiom and Cantor's nested intervals axiom implies Dedekind's cut axiom.
• Proof that Cantor's nested intervals axiom implies Archimedes' axiom.
• Definition of a reflexive tactic for Cong : CongR.

This new release of GeoCoq contains the pieces of formalization described in Pierre Boutry's PhD thesis and in the paper "Proof Checking Euclid" by Beeson, Narboux and Wiedijk. It also contains some proofs related to continuity axioms presented in Charly Gries' master's thesis.
Many files have been generalized to make no assumption on the upper dimension of the space.

• This release is compatible with Coq 8.6.1, 8.7.2, 8.8. Some files depend on the Mathematical Components Library (version >=1.6.4). Mathcomp is only used to build a model of the axioms, it is not essential for using the library.
• Introduction of several packages: "coinc" includes some useful tactics we developed, "axioms" all our axiom systems, "elements" the formalization of Euclid's proofs, "pof" the plane over a real closed field modeling Tarski's axioms, and "main" the rest of the developement.
• Reorganization of the type classes to allow more different contexts.
• Definition of Hilbert's line completeness axiom and two versions of Hilbert's completeness axiom.
• Proof that Hilbert's line completeness axiom implies Hilbert's completeness axiom.
• Proof that Dedekind cut axiom implies Hilbert's line completeness axiom.
• Add two versions of the circle-circle continuity and the equivalence proofs.
• Most of the development in neutral geometry is now dimensionless, including the equivalence of the different versions of the parallel postulate.
• Add some definitions and properties about planes.
• Definition of five equivalent versions of the upper 3-dimensional axiom and related proofs.
• The fixed axioms of Euclid's Elements is modified to be closer to Euclid's. Proofs for Book I are updated accordingly.
• Add constructions for parallelogram and rhombus (by R. Coghetto)
• Model of Tarski's axioms: a cartesian plane over a real closed field; this part of the development depends on the Mathematical Components Library.

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.

• Add compatibility with Coq 8.6.
• Add Side-Side-Angle theorem for right triangles.
• Add the fact that, in a triangle isosceles in A, the altitude in A is also the bisector of the angle in A and median in A.

This new release brings mainly:

• some results about Archimedes' postulates contributed by Charly Gries,
• equivalences between about 30 versions of the parallel postulate by Charly Gries and Pierre Boutry,
• a study of the bisector and incenter contributed by Dan Song,
• a justification of the area method axioms contributed by Julien Narboux

Changelog:

• Add compatibility with Coq 8.5.
• Definition of Archimedes' postulate (geometric version).
• Definition of Archimedes' postulate for angles.
• Archimedes' postulate implies Aristotle's postulate.
• Legendre's theorems.
• Szmielew's theorem about parallel postulates: every proposition which is true in Euclidean geometry and not in Hyperbolic geometry is equivalent to the parallel postulate.
• Predicate TS (Two Sides) cleared of a redundant condition.
• Definition of the interior bisector and related properties.
• Proof of the existence of the incenter of a triangle.
• Proof of the existence of an equilateral triangle build on a given base without any continuity axiom (in any Pythagorean field).
• Justification of the axioms of the area method.

• Proof that Tarski's axioms follow from Hilbert's axioms
• Definition of new statements equivalent to the parallel postulate and related proofs.

This version does not bring many new results but we cleaned up the names of the definitions.

• Definition of new statements equivalent to the parallel postulate and related proofs.
• Many predicates renamed.

• Definition of new statements equivalent to the parallel postulate and related proofs.
• Characterization of right triangle, parallelism and perpendicularity using coordinates.
• The Gröbner basis method can now be used to prove statements within Tarski's system of geometry.

• Formalization of Chapter 16 of SST (this completes the formalization of part one of the book in 2D!) :
  definition of coordinates and characterization of Cong and Bet using coordinates.
• Reorganization of files into directories
• Creation of a ./configure
• Characterization of Midpoint and Col using coordinates.
• Proof of the equivalence between upper-dimension axiom and the fact that all points are coplanar.
• Proof of the pseudo-transitivity and permutation properties of the generalized con-cyclic predicate.
• Definition of the sum of angles and related proofs.
• Proofs about the parallel postulate: assuming a weak geometric version of Archimedes axiom,
  the fact that the sum of angles of a triangle is two rights implies Playfair's postulate.
• Proofs of the decidability of Chapter 11 predicates, assuming points equality decidability.