Implementation of Bourbaki's Elements of Mathematics in Coq: Part Two; Ordered Sets, Cardinals, Integers - Archive ouverte HAL Access content directly
Reports (Research Report) Year : 2018

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

(1)
1

Abstract

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.Version 7 includes rational and real numbers. Versions 8 and 9 include more theorems about ordinal numbers. Version 9 includes Sperner's theorem, and corrects a mistake in the size of one. The code (including some exercises) is available on the Web, under http://www-sop.inria.fr/marelle/gaia .
Nous pensons qu’il est possible de mettre dans un ordinateur l’ensemble de l’œuvre de Bourbaki. L’un des objectifs du projet Gaia concerne l’algèbre homologique (théorie et algorithmes); dans une première étape nous voulons implémenter les neuf chapitres du livre Algèbre. Au préalable, il faut implémenter la théorie des ensembles. Nous utilisons l’Assistant de Preuve Coq; les choix fondamentaux et axiomes sont ceux proposés par Carlos Simpson. Ce rapport liste et commente toutes les définitions et théorèmes du Chapitre “Ensembles ordonnés, cardinaux, nombres entiers”. La version 9 de ce document décrit la bibliothèque à la fin de l'année 2017. Une partie des exercises a été résolue. Le code est disponible sur le site Web http://www-sop.inria.fr/marelle/gaia
Fichier principal
Vignette du fichier
RR-7150-v10.pdf (3.14 Mo) Télécharger le fichier
Origin : Files produced by the author(s)

Dates and 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)

Identifiers

  • HAL Id : inria-00440786 , version 10

Cite

José Grimm. Implementation of Bourbaki's Elements of Mathematics in Coq: Part Two; Ordered Sets, Cardinals, Integers. [Research Report] RR-7150, Inria Sophia Antipolis; INRIA. 2018, pp.826. ⟨inria-00440786v10⟩
919 View
1242 Download

Share

Gmail Facebook Twitter LinkedIn More