Loading...
Please wait, while we are loading the content...
Similar Documents
The Three Gap Theorem : Specification and Proof in Coq
| Content Provider | Hyper Articles en Ligne (HAL) |
|---|---|
| Author | Mayero, Micaela |
| 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. |
| File Format | |
| Language | English |
| Publisher Date | 1999-01-01 |
| Publisher Institution | INRIA |
| Access Restriction | Open |
| Subject Keyword | THREE GAP THEOREM PROOF THEOREM SPECIFICATION COQ REAL NUMBERS info Computer Science [cs] Other [cs.OH] |
| Content Type | Text |
| Resource Type | Article |
