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

Journal of Formalized Reasoning

José Grimm¹ 

[1] INRIA, Marelle Team

关键词: Coq;    Bourbaki;    sets;    integers;    rational numbers;    real numbers;   

DOI  :  

学科分类：计算机科学（综合）

来源: Universita degli Studi di Bologna

【 摘 要 】

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.

【 授权许可】

Unknown