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

José Grimm

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.

Keywords


Coq; Bourbaki; sets; integers; rational numbers; real numbers

Full Text:

PDF (English)

References


Sylvie Boldo, Catherine Lelay, and Guillaume Melquiond. Formalization of Real Analysis: A Survey of Proof Assistants and Libraries. Mathematical Structures in Computer Science, page 38, 2014. https://hal.inria.fr/hal-00806920.

N. Bourbaki. Elements of Mathematics, Theory of Sets. Springer, 1968. [Bou70] N. Bourbaki. Éléments de mathématiques, Théorie des ensembles. Diffusion CCLS, 1970.

N. Bourbaki. Elements of Mathematics, Algebra I. Springer, 1989.

N. Bourbaki. Elements of Mathematics, General Topology. Springer,

Translation of the 1966 French edition.

Georg Cantor. Contributions to the Founding of the Theory of Transfinite Numbers. Dover Publications Inc, 1897. Trans. P. Jourdain, 1955.

Cyril Cohen. Construction of real algebraic numbers in Coq. In Lennart Beringer and Amy Felty, editors, ITP - 3rd International Conference on Interactive Theorem Proving - 2012, Princeton, United States, August 2012. Springer. https://hal.inria.fr/hal-00671809.

Edsger W. Dijkstra. An exercise for Dr. R.M.Burstall. Available at http://www.cs.utexas.edu/users/EWD/ewd05xx/EWD570.PDF, May 1976.

Edsger W. Dijkstra. More about the function “fusc” (a sequel to EWD570). Available at

http://www.cs.utexas.edu/users/EWD/ewd05xx/EWD578.PDF, August 1976.

François Garillot, Georges Gonthier, Assia Mahboubi, and Laurence

Rideau. Packaging mathematical structures. In Theorem Proving in Higher Order Logics, Lecture Notes in Computer Science 5674, 2009. https://hal.inria.fr/inria-00368403.

Georges Gonthier and Assia Mahboubi. An introduction to small scale reflection in Coq. Journal of Formalized Reasoning, 3(2):95–152, 2010. https://jfr.unibo.it/article/view/1979.

José Grimm. Implementation of Bourbaki’s Elements of Mathematics in Coq: Part Two; Ordered Sets, Cardinals, Integers. Research Report RR-7150, INRIA, 2009. http://hal.inria.fr/inria-00440786/en/.

José Grimm. Implementation of Bourbaki’s Elements of Mathematics in Coq, part one theory of sets. Journal of Formalized Reasoning, 3(1):79–126, 2010.

José Grimm. Fibonacci numbers and the Stern-Brocot tree in Coq. Research Report RR-8654, Inria Sophia Antipolis, December 2014.

Milad Niqui and Yves Bertot. Qarith: Coq formalisation of lazy rational arithmetic. In Stefano Berardi, Mario Coppo, and Ferruccio Damiani, editors, Types for Proofs and Programs, volume 3085 of Lecture Notes in Computer Science, pages 309–323. Springer Berlin Heidelberg, 2004.

Milad Niqui. Exact arithmetic on the Stern-Brocot tree. Journal of Discrete Algorithms, 5(2), 2007.

Carlos Simpson. Computer theorem proving in math. Technical report, CNRS, Laboratoire J.A. Dieudonne, 2004. arXiv:math/0311260v2.

Carlos Simpson. Set-theorical mathematics in Coq. Technical report, CNRS, Laboratoire J.A. Dieudonne, 2004. arXiv:math/0402336v1.

Moritz Stern. Ueber eine zahlentheorische Funktion. Journal für die reine und angewandte Mathematik, 55:193–220, 1858.




DOI: 10.6092/issn.1972-5787/4771

Copyright (c) 2016 José Grimm

Creative Commons License
This work is licensed under a Creative Commons Attribution 3.0 International License.