Coq

En una entrada anterior comentamos el proyecto de formalización del libro Elements of Mathematics: Theory of Sets de N. Bourbaki en Coq.

En dicha entrada comentamos el primer paso del proyecto consistente en la formalización de la teoría de conjuntos correspondiente al capítulo II del libro de Bourbaki (páginas 65-130).

La formalización del capítulo III (páginas 131-256) constituye el contenido del segundo paso. Dicha formalización ha sido publicada por José Grimm en el artículo Implementation of Bourbaki’s Elements of Mathematics in Coq: Part Two; Ordered Sets, Cardinals, Integers. Su resumen es el siguiente

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. It implements some properties on ordinal numbers. The code (including some exercises) is available on the Web, under http://www-sop.inria.fr/apics/gaia.

Una de las tareas del razonamiento formalizado consiste en la formalización de textos matemáticos. Un ejemplo es el artículo Implementation of Bourbaki’s Elements of Mathematics in Coq: Part One, Theory of Sets.

El autor del artículo es José Grimm (del INRIA Sophia-Antipolis Méditerranée) y se ha publicado en el Journal of Formalized Reasoning.

El trabajo se enmarca en el proyecto GAIA (Geometry, Algebra, Informatics and Applications), cuyos objetivos son la formalización de las demostraciones del la HDR (Habilitation à diriger des recherches) de A. Quadrat, de las del libro Basic Homological Algebra (de M. Scott Osborne) y la demostración de la corrección de la implementación de estos teoremas como algoritmos en el sistema OreModules.

Dentro del proyecto GAIA, el contenido del artículo es el primer paso y, esencialmente consiste en la formalización en Coq de teoremas del libro Elements of Mathematics: Theory of Sets de N. Bourbaki. La formalización se basa en la realizada por Carlos Simpson y publicada en Set-theoretical mathematics in Coq.

El resumen del artículo es el siguiente

This paper presents a formalization of the first book of the series Elements of Mathematics” by Nicolas Bourbaki, using the Coq proof assistant.

It discusses formalization of mathematics, and explains in which sense a computer proof of a statement corresponds to a proof in the Bourbaki sense, given that the Coq quantifiers are not defined in terms of Hilbert’s epsilon function. The list of axioms and axiom schemes of Bourbaki is compared to the more usual Zermelo-Fraenkel theory, and to those proposed by Carlos Simpson, which form the basis of the Gaia software. Some basic constructions (union, intersection, product, function, equivalence and order relation) are described, as well as some properties; this corresponds to Sections 1 to 6 of Chapter II, and the first two sections of Chapter III. A commented proof of Zermelo’s theorem is also given. The code (including almost all exercises) is available on the Web, under http://www-sop.inria.fr/apics/gaia.