Skip to Main content Skip to Navigation

Implementation of three types of ordinals in Coq

José Grimm 1
1 MARELLE - Mathematical, Reasoning and Software
CRISAM - Inria Sophia Antipolis - Méditerranée
Abstract : One can define an inductive type T in Coq by the rules: zero is in T, and 'cons a n b' is in T when a, b are in T and n is an integer. One can embed this type with an ordering, and show that the subset of ''normal'' elements is well-ordered, thus corresponds to some ordinal, namely epsilon-zero, the least epsilon-ordinal of Cantor. The same construction can be applied to the case where cons take one more argument of type T; in this case we get the Feferman-Schütte ordinal Gamma-zero. These two type were implemented by Castéran in Coq. In these paper we present an implementation using the ssreflect library. One can consider the case where cons takes four arguments of type T and use the ordering function proposed by Ackermann. This gives some large ordinal. The proof in Coq that it is a well-ordering matches exactly that of Ackermann. Every limit ordinal in this type is (constructively) the supremum of a strictly increasing function. Finally, we show how these types are related to ordinals defined in an implementation of the theory of sets of Bourbaki (a variant of Zermelo-Fraenkel). The code is available on the Web, under
Document type :
Complete list of metadata

Cited literature [30 references]  Display  Hide  Download
Contributor : José Grimm Connect in order to contact the contributor
Submitted on : Friday, November 29, 2013 - 4:33:00 PM
Last modification on : Thursday, January 7, 2021 - 3:40:05 PM
Long-term archiving on: : Monday, March 3, 2014 - 8:20:34 PM


Files produced by the author(s)


  • HAL Id : hal-00911710, version 1



José Grimm. Implementation of three types of ordinals in Coq. [Research Report] RR-8407, INRIA. 2013, pp.74. ⟨hal-00911710⟩



Record views


Files downloads