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

The people

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

• sset11.v: Addition, multiplication, division, etc.
• sset12.v: Normal functions, internally closed collections of ordinals, derivation, the Veblen hierarchy, definition by transfinite induction, exponentiation.
• sset13.v: Cantor Normal Form
• sset14.v: Epsilon numbers, derivation of sum and product, Schutte phi and psi, Aleph, cofinality
• sset15.v: Infinite sums and products of cardinals, inaccessible cardinal, the generalised continuum hypothesis
• sset16.v: On an exercise of Bourbaki
• sset17.v: Theory of models
• sset18.v: Structures
• sset19.v: Direct and Inverse Limits

Other files

These files are independent of the previous ones.

• ssete7.v: Combinatory (positive integers)
• ssete8.v: Combinatory (positive and negative integers)
• ssete9.v: More ordinals (Schutte and Ackermann)
• fibm.v: Some properties of Fibonacci numbers
• stern.v: The Stern diatomic sequence

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