Implementation of Bourbaki's Elements of Mathematics in Coq: Part Two; Ordered Sets, Cardinals, Integers
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
Origin : Files produced by the author(s)