HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation

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.
Document type :
Complete list of metadata

Contributor : Rapport de Recherche Inria Connect in order to contact the contributor
Submitted on : Wednesday, May 24, 2006 - 10:59:58 AM
Last modification on : Thursday, February 3, 2022 - 11:17:02 AM
Long-term archiving on: : Sunday, April 4, 2010 - 9:26:42 PM


  • HAL Id : inria-00072808, version 1



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



Record views


Files downloads