Implementation of Bourbaki's Elements of Mathematics in Coq: Part Two, From Natural Numbers to Real Numbers

José Grimm 1
1 MARELLE - Mathematical, Reasoning and Software
CRISAM - Inria Sophia Antipolis - Méditerranée
Abstract : This paper describes a formalization of the first book of the series ``Elements of Mathematics'' by Nicolas Bourbaki, using the Coq proof assistant. In a first paper published in this journal, we presented the axioms and basic constructions (corresponding to a part of the first two chapters of book I, theory of sets). We discuss here the set of integers (third chapter of book I, theory of set), the sets Z and Q (first chapter of book II, Algebra) and the set of real numbers (Chapter 4 of book III, General topology). We start with a comparison of the Bourbaki approach, the Coq standard library, and the Ssreflect library, then present our implementation.
Document type :
Journal articles
Complete list of metadatas

Cited literature [15 references]  Display  Hide  Download

https://hal.inria.fr/hal-01415375
Contributor : José Grimm <>
Submitted on : Monday, December 19, 2016 - 2:53:05 PM
Last modification on : Friday, January 12, 2018 - 1:48:57 AM
Long-term archiving on : Tuesday, March 21, 2017 - 9:46:10 AM

File

jfra2-v2.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

José Grimm. Implementation of Bourbaki's Elements of Mathematics in Coq: Part Two, From Natural Numbers to Real Numbers. Journal of Formalized Reasoning, ASDD-AlmaDL, 2016, 9 (2), pp.52. ⟨https://jfr.unibo.it/article/view/4771⟩. ⟨10.6092/issn.1972-5787/4771⟩. ⟨hal-01415375⟩

Share

Metrics

Record views

346

Files downloads

107