Spring 2024

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.

Provide feedback