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

José Grimm 1
1 MARELLE - Mathematical, Reasoning and Software
CRISAM - Inria Sophia Antipolis - Méditerranée
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 .
Document type :
Reports
Liste complète des métadonnées

https://hal.inria.fr/inria-00440786
Contributor : José Grimm <>
Submitted on : Wednesday, December 5, 2018 - 5:28:31 PM
Last modification on : Thursday, February 7, 2019 - 4:56:23 PM
Document(s) archivé(s) le : Wednesday, March 6, 2019 - 3:46:43 PM

File

RR-7150-v10.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : inria-00440786, version 10

Collections

Citation

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⟩

Share

Metrics

Record views

53

Files downloads

124