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 http://www-sop.inria.fr/marelle/gaia
Document type :
Reports
Complete list of metadatas

Cited literature [30 references]  Display  Hide  Download

https://hal.inria.fr/hal-00911710
Contributor : José Grimm <>
Submitted on : Friday, November 29, 2013 - 4:33:00 PM
Last modification on : Thursday, January 11, 2018 - 4:24:43 PM
Long-term archiving on : Monday, March 3, 2014 - 8:20:34 PM

File

RR8407.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-00911710, version 1

Collections

Citation

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

Share

Metrics

Record views

607

Files downloads

463