Formalisation en Coq de la géométrie enseignée au lycée
Pour privilégier le raisonnement,
la formalisation choisie n'utilise pas le recours à la méthode
analytique.
Les définitions, théorèmes et démonstrations de ce
développement en Coq
"suivent" ceux donnés au lycée.
Les techniques de démonstration de géométrie employées au
lycée sont formalisées (calcul vectoriel, utilisation des
transformations, des nombres complexes etc.)
On trouvera expliquée en détail la démarche utilisée dans le
rapport de recherche : RR-4893
Ce développement propose une collection de
"chapitres" couvrant une large partie du programme de
géométrie du lycée en France.
Ces différents chapitres sont représentés dans le graphe de
dépendance ci-dessous.
On commence par des généralités sur la géométrie affine puis
la structure s'enrichit d'un produit scalaire, ce qui permet de
faire de la géométrie euclidienne dans le plan et l'espace et
on finit par démontrer des théorèmes classiques (voir un exemple)
et par les nombres complexes.
On trouvera le graphe de dépendance des fichiers Coq du développement en cliquant sur le bouton
Les sources de Coq sont disponibles à
l'adresse suivante :
ftp://ftp-sop.inria.fr/lemme/Frederique.Guilhot/geometrie.tar.gz (version 7.4)
ftp://ftp-sop.inria.fr/lemme/Frederique.Guilhot/geov8.tar.gz (version 8)
Exemple : le théorème du cercle des neuf points.
Ce théorème est un grand classique de la géométrie euclidienne plane démontré par Euler et Feuerbach.
Il montre que dans un triangle, le cercle circonscrit aux milieux des côtés du triangle ABC passe aussi par le pied des trois hauteurs et par les milieux des segments qui joignent les sommets à l'orthocentre du triangle. De plus, ce cercle a pour centre le milieu du segment joignant l'orthocentre au cercle circonscrit du triangle ABC.
figure générée par GeoView à partir du théorème du cercle des neuf points
Cette figure est dynamique
et interactive :
- les points en vert peuvent être déplacés à la souris
(bouton gauche),
- en maintenant le bouton droit enfoncé, on peut déplacer la
figure,
- en cliquant sur la figure et en utilisant les touches < et
>, on peut agrandir ou réduire la figure,
- en double-cliquant sur la figure, on obtient un menu : on peut
créer de nouveaux objets pour vérifier des conjectures par
exemple.
énoncé du théorème du cercle des neuf points tel qu'il apparait à l'écran avec Pcoq
La démonstration de ce théorème (formalisée en Coq) utilise des arguments très divers :