Implementation of Bourbaki's Elements of Mathematics in Coq: Part Two, From Natural Numbers to Real Numbers
DOI:
https://doi.org/10.6092/issn.1972-5787/4771Keywords:
Coq, Bourbaki, sets, integers, rational numbers, real numbersAbstract
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.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.
Downloads
Published
How to Cite
Issue
Section
License
Copyright (c) 2016 José Grimm
Copyrights and publishing rights of all the texts on this journal belong to the respective authors without restrictions.
This journal is licensed under a Creative Commons Attribution 3.0 Unported License (full legal code).
See also our Open Access policy
