-
Notifications
You must be signed in to change notification settings - Fork 2
/
meta.yml
219 lines (183 loc) · 10.2 KB
/
meta.yml
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
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
---
fullname: High School Geometry
shortname: HighSchoolGeometry
opam_name: coq-high-school-geometry
organization: coq-community
community: true
action: true
synopsis: Geometry in Coq for French high school
description: |-
This Coq library is dedicated to high-shool geometry teaching. The
axiomatisation for affine Euclidean space is in a non analytic setting.
Includes a proof of Ptolemy's theorem.
publications:
- pub_url: https://hal.inria.fr/inria-00071689/
pub_title: Premiers pas vers un cours de géométrie en Coq pour le lycée
- pub_url: https://hal.inria.fr/inria-00585203/
pub_title: Similar Triangles and Orientation in Plane Elementary Geometry for Coq-based Proofs
pub_doi: 10.1145/1774088.1774358
authors:
- name: Frédérique Guilhot
initial: true
- name: Tuan-Minh Pham
maintainers:
- name: Laurent Théry
nickname: thery
opam-file-maintainer: palmskog@gmail.com
opam-file-version: dev
license:
fullname: GNU Lesser General Public License v2.1 or later
identifier: LGPL-2.1-or-later
supported_coq_versions:
text: 8.16 or later
opam: '{>= "8.16"}'
tested_coq_opam_versions:
- version: dev
- version: '8.19'
- version: '8.18'
- version: '8.17'
- version: '8.16'
namespace: HighSchoolGeometry
keywords:
- name: geometry
- name: teaching
- name: high school
- name: Ptolemy's theorem
categories:
- name: Mathematics/Geometry/General
documentation: |-
## Documentation in English
See also the [documentation in French](#Documentation-en-français) below.
This library consists in a collection of "chapters" spanning most of geometry taught
to French high-shool students. We do not even try to minimize the number of axioms but
rather to get as close as possible to informal definitions, theorems and proofs.
In order to focus on reasoning issues, we use a non analytic description of euclidean geometry.
The interested reader can find details about this work in Inria research report RR-4893:
[Premiers pas vers un cours de géométrie en Coq pour le lycée][report-link].
The first part "2-3 dimensional affine geometry" deals with formalising:
- points, vectors, barycenters, oriented lengths,
(Rutile.v, Field_affine.v, vecteur.v, barycentre.v, milieu.v, mesure_algebrique.v)
- collinearity, coplanarity, (alignement.v, coplanarite.v)
- parallelism and incidence of straight lines, (parallelisme_concours.v)
- proofs of Thales and Desargues theorems.(affine_classiques.v)
In the second part "3 dimensional affine geometry", we prove theorems about:
- relative positions of two straight lines in the space (Droite_espace.v)
- relative positions of a straight line and a plane (Droite_plan_espace.v)
- relative positions of two planes (Plans_paralleles.v)
- parallelism and incidence properties for several planes and straight lines
(Plan_espace.v)
The third part "2-3 dimensional euclidean geometry" deals with formalising:
- scalar product, orthogonal vectors, and unitary vectors
(produit_scalaire.v, orthogonalite.v, representant_unitaire.v)
- eulidean distance and orthogonal projection on a line
(distance_euclidienne.v, projection_orthogonale.v)
- proofs of Pythagorean theorem, median theorem (euclidien_classiques.v)
The fourth part "space orthogonality" deals with formalising:
- orthogonal line and plan (orthogonalite_espace.v)
We use these definitions to solve a high-school diploma (baccalaureat) exercise
in a formal way.(exercice_espace.v).
The fifth part "plane euclidean geometry" deals with formalising:
- affine coordinate system, orthogonal coordinate system, affine coordinates
(repere_plan.v, repere_ortho_plan.v)
- oriented angles (angles_vecteurs.v, angles_droites.v)
- trigonometry (trigo.v)
- proofs of Pythagorean theorem, median theorem, Al-Kashi and sine theorems
(metrique_triangle.v)
- perpendicular bisector, isocel triangle, orthocenter,
(mediatrice.v, isocele.v, orthocentre.v)
- circle, cocyclicity, tangency (line or circle tangent)
(cercle.v, cocyclicite.v, complements_cercle.v, contact.v)
- signed area, determinant (aire_signee.v, determinant.v)
- equations for straight lines and circles in plane geometry
(equations_droites.v, equations_cercles.v)
The sixth part "plane transformations", deals with formalising:
- translations, homothety
(dilatations.v, composee_dilatations.v, homothetie_plane.v)
- rotations, reflexions (rotation_plane.v, reflexion_plane.v)
- composition of these transformations.
(composee_reflexions.v, composee_translation_rotation.v, composee_transformations.v, similitudes_directes.v)
- conservation of tangency for these transformations. (transformations_contact.v)
In the seventh part "applications", we prove:
- Miquel's theorem, orthocenter theorem, Simson line
(applications_cocyclicite.v)
- circle power and plane inversion (puissance_cercle.v, inversion.v)
- Euler line theorem and nine point circle theorem
(droite_Euler.v, homoth_Euler.v).
The eighth part "complex numbers", deals with formalising:
- the field properties of complex numbers
(complexes.v, formes_complexes.v, operations_complexes.v, complexes_conjugaison.v)
- application to geometry of complex numbers
(complexes_dilations.v, complexes_similitudes.v, complexes_transformations.v, complexes_exercice.v,
complexes_inversion.v, complexes_analytique.v)
Tuan-Minh Pham introduced the concept of orientation and proved Ptolemy's theorem
(orientation.v, triangles_semblables.v, Ptolemee.v). This work is described in
a [separate paper][ptolemy-link].
## Documentation en français
Ce développement propose une collection de "chapitres" couvrant
une large partie du programme de géométrie du lycée en France.
Le but n'est pas d'avoir un nombre minimal d'axiomes mais de "coller au plus près"
des définitions, théorèmes et démonstrations donnés au lycée.
Pour privilégier le raisonnement, la formalisation choisie n'utilise pas
le recours à la méthode analytique.
On trouvera expliquée en détail la démarche utilisée dans le Inria rapport de recherche
RR-4893: [Premiers pas vers un cours de géométrie en Coq pour le lycée][report-link].
Dans la partie "géométrie affine (dimension 2 et 3)", sont formalisés
- les points, vecteurs, barycentres, mesures algébriques,
(Rutile.v, Field_affine.v, vecteur.v, barycentre.v, milieu.v, mesure_algebrique.v)
- les notions d'alignement et de coplanarité, (alignement.v, coplanarite.v)
- les notions de parallélisme et concours de droites, (parallelisme_concours.v)
- les preuves des théorèmes de Thalès et de Desargues. (affine_classiques.v)
Dans la partie "géométrie affine dans l'espace", ont été démontrés les théorèmes concernant:
- les positions relatives de deux droites dans l'espace (Droite_espace.v)
- les positions relatives d'une droite et d'un plan (Droite_plan_espace.v)
- les positions relatives de deux plans (Plans_paralleles.v)
- les propriétés d'incidence et de parallélisme de plusieurs droites et plans de l'espace.
(Plan_espace.v)
Dans la partie "géométrie euclidienne (dimension 2 et 3)", sont formalisés
- le produit scalaire, la notion d'orthogonalité de vecteurs et de vecteurs unitaires,
(produit_scalaire.v, orthogonalite.v, representant_unitaire.v)
- la distance euclidienne et la projection orthogonale sur une droite.
(distance_euclidienne.v, projection_orthogonale.v)
- les preuves des théorèmes de Pythagore, de la médiane et l'étude de ligne de niveau
(euclidien_classiques.v)
Dans la partie "orthogonalité dans l'espace", est formalisée
- la notion de droite et plan orthogonaux (orthogonalite_espace.v)
- un exercice donné au baccalauréat S est traité comme application (exercice_espace.v).
Dans la partie "géométrie euclidienne plane", sont formalisés
- les repères affines, les repère orthogonaux et la notion de coordonnées de points
(repere_plan.v, repere_ortho_plan.v)
- les angles orientés de vecteurs et de droites (angles_vecteurs.v, angles_droites.v)
- la trigonométrie (trigo.v)
- la trigonométrie du triangle rectangle et les théorèmes d'Al-Kashi et des sinus
(metrique_triangle.v)
- les notions de médiatrice, triangle isocèle, orthocentre
(mediatrice.v, isocele.v, orthocentre.v)
- les notions de cercle, cocyclicité, contact (tangente et cercles tangents)
(cercle.v, cocyclicite.v, complements_cercle.v, contact.v)
- les notions d'aires signées et de déterminant de vecteurs (aire_signee.v, determinant.v)
- une partie de géométrie analytique concernant les équations de droites et les équations de cercle
(equations_droites.v, equations_cercles.v)
Dans la partie "transformations planes", sont étudiées
- les translations, homothéties et leur composées
(dilatations.v, composee_dilatations.v, homothetie_plane.v)
- les rotations, symétries axiales (rotation_plane.v, reflexion_plane.v)
- les composées de ces transformations dont les similitudes directes.
(composee_reflexions.v, composee_translation_rotation.v, composee_transformations.v, similitudes_directes.v)
- les propriétés de conservation du contact par ces transformations (transformations_contact.v)
Dans la partie "applications", sont démontrés
- les théorèmes de Miquel, des symétriques de l'orthocentre, de la droite de Simson
(applications_cocyclicite.v)
- les notions de puissance d'un point par rapport à un cercle et d'inversion plane
(puissance_cercle.v, inversion.v)
- les théorèmes de la droite d'Euler et du cercle des neuf points
(droite_Euler.v et homoth_Euler.v).
Dans la partie "nombres complexes", sont démontrées
- les propriétés algébriques du corps des nombres complexes
(complexes.v, formes_complexes.v, operations_complexes.v, complexes_conjugaison.v)
- la caractérisation géométrique des transformations d'écriture complexe : z -> a z + b
(complexes_dilations.v, complexes_similitudes.v, complexes_transformations.v, complexes_exercice.v)
- l'écriture complexe de l'inversion (complexes_inversion.v)
- l'écriture analytique de toutes les transformations étudiées (complexes_analytique.v)
[report-link]: https://hal.inria.fr/inria-00071689/
[ptolemy-link]: https://hal.inria.fr/inria-00585203/
---