Implementation of Bourbaki's Elements of Mathematics in Coq: Part Two; Ordered Sets, Cardinals, Integers - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Rapport (Rapport De Recherche) Année : 2013

Implementation of Bourbaki's Elements of Mathematics in Coq: Part Two; Ordered Sets, Cardinals, Integers

Résumé

We believe that it is possible to put the whole work of Bourbaki into a computer. One of the objectives of the Gaia project concerns homological algebra (theory as well as algorithms); in a first step we want to implement all nine chapters of the book Algebra. But this requires a theory of sets (with axiom of choice, etc.) more powerful than what is provided by Ensembles; we have chosen the work of Carlos Simpson as basis. This reports lists and comments all definitions and theorems of the Chapter ''Ordered Sets, Cardinals, Integers''. Version 3 is based on the Coq ssreflect library. Version 5 implements many properties of ordinal numbers and infinite cardinal numbers. Version 6 includes the Veblen hierarchy of ordinals, the Schütte function psi, and a bit of theory of models. The code (including some exercises) is available on the Web, under http://www-sop.inria.fr/apics/gaia .
Fichier principal
Vignette du fichier
RR7150-v6.pdf (3.27 Mo) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)

Dates et versions

inria-00440786 , version 1 (11-12-2009)
inria-00440786 , version 2 (01-04-2010)
inria-00440786 , version 3 (02-12-2010)
inria-00440786 , version 4 (21-12-2011)
inria-00440786 , version 5 (22-12-2011)
inria-00440786 , version 6 (29-11-2013)
inria-00440786 , version 7 (16-01-2015)
inria-00440786 , version 8 (09-12-2016)
inria-00440786 , version 9 (29-11-2017)
inria-00440786 , version 10 (05-12-2018)

Identifiants

  • HAL Id : inria-00440786 , version 6

Citer

José Grimm. Implementation of Bourbaki's Elements of Mathematics in Coq: Part Two; Ordered Sets, Cardinals, Integers. [Research Report] RR-7150, 2013, pp.604. ⟨inria-00440786v6⟩
1012 Consultations
1354 Téléchargements

Partager

Gmail Facebook X LinkedIn More