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.