-
Notifications
You must be signed in to change notification settings - Fork 26
/
Changelog
134 lines (110 loc) · 7.79 KB
/
Changelog
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
Release 2.5.0
==========================
- 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.
Release 2.4.1
==========================
- This release is compatible with Coq 8.7.0-8.11.2. Some files depends on mathcomp field library (1.6.4 <= version < 1.11.0).
- 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 cut axiom.
- Proof that Cantor's nested intervals axiom implies Archimedes' axiom.
- Definition of a reflexive tactic for Cong : CongR.
Release 2.4.0
==========================
- This release is compatible with Coq 8.6.1, 8.7.2, 8.8. Some files depends on mathcomp field library (version >=1.6.4).
Mathcomp is used only 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 development.
- 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.
Release 2.3.0
==========================
- This release is compatible with Coq 8.5, 8.6 and trunk.
- Definition of the sum of segments and related proofs.
- 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.
- Definitions of an axiom system to prove Propositions of Euclid's Elements and some links with Tarski's axiom system.
- 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.
- 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 cut 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 cut axiom.
- Add a new version of the parallel postulate and the equivalence proofs.
- Add definitions of predicates to express that a point is inside, on and outside a circle, and associated lemmas.
- Add some properties about tangency.
- Add some results about half of angles.
Release 2.2.1
==========================
- Add compatibility with Coq 8.6.
- Add SSA theorem (Side Side Angle) for right triangles.
- Add the fact that in a isosceles triangle ABC with AB = AC,
the altitude from vertex A is also the angle bisector from vertex A and the median from vertex A.
Release 2.2.0
==========================
- Add compatibility with Coq 8.5.
- Definition of Archimedes' axiom (its geometric version).
- Definition of Archimedes' axiom for angles.
- Archimedes' axiom implies Aristotle's axiom.
- Proof of Legendre's theorems.
- The TS Predicate (Two Sides) was 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.
Release 2.1.1 (2016-05-25)
==========================
- A few statements equivalent to the parallel postulate are renamed.
Release 2.1.0 (2016-05-09)
==========================
- Proof that Tarski's axioms follow from Hilbert's.
- Definition of new statements equivalent to the parallel postulate and related proofs.
Release 2.0.0 (2016-03-03)
==========================
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 were renamed.
Release 1.1.1 (2015-12-03)
==========================
- Definition of new statements equivalent to the parallel postulate and related proofs.
- Algebraic 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.
Release 1.1.0 (2015-10-27)
==========================
- Reorganization of files into directories.
- Creation of a ./configure.
- Formalization of Chapter 16 of SST:
definition of coordinates and characterization of Cong and Bet using coordinates.
- Algebraic 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.
- Definition of a weak geometric version of Archimedes' axiom: Aristotle's axiom.
- Proofs about the parallel postulate:
assuming Aristotle's axiom,
the fact that the angles of a triangle sum to exactly two right angles implies Playfair's postulate.
- Proofs of the decidability of the predicates from Chapter 11, assuming point equality decidability.
Release 1.0.1 (2015-07-16)
==========================
- Add -R . GeoCoq to fix compilation for the release as an opam package.
Release 1.0.0 (2015-07-15)
==========================
- First release under LGPL 3.0 available on Github.
- Website available here: https://geocoq.github.io/GeoCoq/.