Implementation of Bourbaki's Elements of Mathematics in Coq: Part One, Theory of Sets - Archive ouverte HAL Access content directly
Reports (Research Report) Year : 2013

Implementation of Bourbaki's Elements of Mathematics in Coq: Part One, Theory of Sets

(1)
1
José Grimm
  • Function : Author
  • PersonId : 830414

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 ''Theory of Sets''. The code (including almost all exercises) is available on the Web, under http://www-sop.inria.fr/marelle/gaia . Version one was released in July 2009, version 2 in December 2009, version 3 in March 2010. Version 4 is based on the Coq ssreflect library. In version 5, released in December 2011, the ''iff_eq'' axiom has been withdraw, and the axiom of choice modified. Version 6 was released in October 2013. Version 7 was released in December 2018
Nous pensons qu'il est possible de mettre dans un ordinateur l'ensemble de l'oeuvre 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ées par Carlos Simpson. Ce rapport liste et commente toutes les définitions et théorèmes du Chapitre théorie des ensembles. Presque tous les exercices ont été résolus. Le code est disponible sur le site Web http://www-sop.inria.fr/marelle/gaia
Fichier principal
Vignette du fichier
RR-6999-v7.pdf (1.14 Mo) Télécharger le fichier
Origin : Files produced by the author(s)

Dates and versions

inria-00408143 , version 1 (29-07-2009)
inria-00408143 , version 2 (08-12-2009)
inria-00408143 , version 3 (30-03-2010)
inria-00408143 , version 4 (02-12-2010)
inria-00408143 , version 5 (14-12-2011)
inria-00408143 , version 6 (31-10-2013)
inria-00408143 , version 7 (04-12-2018)

Identifiers

  • HAL Id : inria-00408143 , version 7

Cite

José Grimm. Implementation of Bourbaki's Elements of Mathematics in Coq: Part One, Theory of Sets. [Research Report] RR-6999, INRIA. 2013, pp.213. ⟨inria-00408143v7⟩
605 View
2552 Download

Share

Gmail Facebook Twitter LinkedIn More