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
Type de document :
[Research Report] RR-8407, INRIA. 2013, pp.74
Liste complète des métadonnées

Littérature citée [30 références]  Voir  Masquer  Télécharger
Contributeur : José Grimm <>
Soumis le : vendredi 29 novembre 2013 - 16:33:00
Dernière modification le : jeudi 11 janvier 2018 - 16:24:43
Document(s) archivé(s) le : lundi 3 mars 2014 - 20:20:34


Fichiers produits par l'(les) auteur(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〉



Consultations de la notice


Téléchargements de fichiers