Implementation of Bourbaki's Elements of Mathematics in Coq: Part One, Theory of Sets
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 ``Theory of Sets''. The code (including almost all exercises) is available on the Web, under http://www-sop.inria.fr/apics/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. There are small differences, marked in footnotes.
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/apics/gaia
Domaines
Logiciel mathématique [cs.MS]
Origine : Fichiers produits par l'(les) auteur(s)