The Three Gap Theorem : Specification and Proof in Coq

Abstract : We present a specification and a proof in Coq of the three gap theorem, or initially Steinhaus conjecture whose result is the following: let N be the distribution of points placed consecutively around a circle by an angle of $\alpha{}$; then the points partition the circle into gaps of at most three different lengths. We start by making an axiomatization of the real numbers in Coq in order to use them in the development. Thereafter, we define all the mathematical tools necessary and some lemmas used in the proof. Finally we state the theorem.
Type de document :
Rapport
[Research Report] RR-3848, INRIA. 1999
Liste complète des métadonnées

https://hal.inria.fr/inria-00072808
Contributeur : Rapport de Recherche Inria <>
Soumis le : mercredi 24 mai 2006 - 10:59:58
Dernière modification le : vendredi 25 mai 2018 - 12:02:05
Document(s) archivé(s) le : dimanche 4 avril 2010 - 21:26:42

Fichiers

Identifiants

  • HAL Id : inria-00072808, version 1

Collections

Citation

Micaela Mayero. The Three Gap Theorem : Specification and Proof in Coq. [Research Report] RR-3848, INRIA. 1999. 〈inria-00072808〉

Partager

Métriques

Consultations de la notice

120

Téléchargements de fichiers

193