Home page of the Gaia software

Gaia stands for: Geometry, Algebra, Informatics and Applications. It is an implementation of the Theory of Sets (following Bournaki) in coq.

The people

José Grimm (Marelle Team)

with the help Alban Quadrat (Disco Team)

José Grimm died in August 2019. Members of the Coq community are collaboratively maintaining a version of this source archive on GitHub. This maintained version works with more recent versions of Coq, compared to the last version developed by José.

The Gaia software

The software consists in a set of Coq files that implement sets, groups, rings, etc. The objective is to implement the "Elements of Mathematics" by N. Bourbaki. The files were originally written for Standard Coq; they are converted to ssreflect. The current source compiles with coq 8.8.1 mathcomp 1.7. It is available under a MIT License.

Theory of sets

This corresponds to the chapter "Theory of sets" from the book "Theory of sets" of Bourbaki. The first file introduces the axioms (choice, excluded middle, extensionality, replacement, etc).

Ordered Sets, Cardinals, Integers

This corresponds to the chapter "Ordered Sets, Cardinals, Integers" from the book "Theory of sets" of Bourbaki. Some exercises are not yet done. Cardinal numbers are implemented via von Neumann ordinals.

Algebraic structures

This is an implementation of Z, Q and R, based on the previous files.

Ordinal and cardinal numbers

Some properties of ordinal numbers

Other files

These files are independent of the previous ones.

Previous version

HTML

HTML version of the code, formatted by Coqdoc

HTML version of the code, formatted by Coqdoc (ssreflect version 1.4)

Documentation

Jfr1 Implementation of Bourbaki's Elements of Mathematics in Coq, part one Theory of Sets, the first paper publised by the Journal of Formalized Reasoning,

jfr2 Implementation of Bourbaki's Elements of Mathematics in Coq: Part two, from natural numbers to real numbers , the second paper publised by the Journal of Formal ized Reasoning, 9(2):1–52, 2016.

RR6999 (version 6) Implementation of Bourbaki's Elements of Mathematics in Coq: Part One, Theory of Sets, the Research Report describing files sset1, sset2, sset3, sset4 and ssete1.

RR 7150 (version 9). Implementation of Bourbaki's Elements of Mathematics in Coq, Part Two ; Ordered Sets, Cardinals, Integers. The Research Report describing files sset5, sset6, sset7, sset8, sset9, sset10, sset11, sset12, sset13, sset14, sset15, sset16, sset17, ssetz, ssetq1, sset2, ssetr, ssetc, ssete2, ssete3, ssete4, ssete5, ssete6, and ssete10.

RR8407. Implementation of three types of ordinals in Coq The Research Report describing the file ssete9.

RR8654. Fibonacci numbers aand the Stern-Brocot tree in Coq The Research Report describing the files fibm and stern,.

XML version of RR6999 version 3, translated by Tralics

XML version of RR7150 version 2, translated by Tralics


Archives

Valid XHTML 1.0 Strict © INRIA 2009-2018 Last modified $Date: 2018/10/19 $