Skip to Main content Skip to Navigation
Conference papers

Des preuves formelles en Coq du théorème de Thalès pour les cercles

David Braun 1 Nicolas Magaud 1
1 IGG
ICube - Laboratoire des sciences de l'ingénieur, de l'informatique et de l'imagerie
Résumé : Le théorème de Thalès pour les cercles et sa réciproque (plus connue sous le nom de théorème du cercle circonscrit à un triangle rectangle) sont des propriétés de géométrie élémentaire enseignées dans les collèges français. Nous nous intéressons non seulement à différentes descriptions possibles de ces propriétés en Coq mais aussi aux preuves correspondantes. Nous étudions notamment comment le choix d’une représentation des objets géométriques contenus dans l’énoncé influencent les arguments de preuve. Nous présentons plusieurs approches, une basée sur des calculs d’angles, une autre basée sur la géométrie analytique et finalement deux démonstrations différentes dans l’axiomatique de Tarski en utilisant dans un cas le théorème de la droite des milieux et dans l’autre la notion de symétrie centrale et ses propriétés.
Document type :
Conference papers
Complete list of metadata

Cited literature [10 references]  Display  Hide  Download

https://hal.inria.fr/hal-01099132
Contributor : David Baelde <>
Submitted on : Wednesday, December 31, 2014 - 3:34:01 PM
Last modification on : Saturday, October 27, 2018 - 1:26:48 AM
Long-term archiving on: : Saturday, April 15, 2017 - 12:21:35 PM

File

jfla15_submission_19.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01099132, version 1

Citation

David Braun, Nicolas Magaud. Des preuves formelles en Coq du théorème de Thalès pour les cercles. Vingt-sixièmes Journées Francophones des Langages Applicatifs (JFLA 2015), Jan 2015, Le Val d'Ajol, France. ⟨hal-01099132⟩

Share

Metrics

Record views

182

Files downloads

1401