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

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 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.

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).

- sset1.v: Set theory
- sset2.v: Correspondences
- sset3.v: Union, Intersection, Products
- sset4.v: Equivalence relations
- ssete1.v: Exercises

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.

- sset5.v: Order relations
- sset6.v: Well-ordered sets
- sset7.v: Equipotent sets. Cardinals
- sset8.v: Natural integers. Finite sets
- sset9.v: Properties of integers
- sset10.v: Infinite sets
- ssete2.v: Exercises
- ssete3.v: Exercises (part 2)
- ssete4.v: Exercises (part 3)
- ssete5.v: Exercises (part 4)
- ssete6.v: Exercises (part 5)
- ssete10.v: Link between sset14 and ssete9

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

- ssetz.v: Rational integers
- ssetq1.v: Rational numbers (part 1)
- ssetq2.v: Rational numbers (part 2)
- ssetr.v: Real numbers
- ssetc.v: Compatibility with the Coq structures

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

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

- gaia_src_oct_18.tar.gz: copy of all the source files (October 2018)
- src_nov17.tar.gz: copy of all the source files (nov 2017)
- gaia_mar_15.tar.gz: copy of all the source files (march 2015)
- set5.v, set6.v, set7.v, set8.v, set9.v, set10.v, set11.v, sete2.v (same files as above, using standard Coq)
- sset15.v: Ordinal numbers (part 5)
- set1.v, set2.v set3.v,set4.v, sete1.v (same files as above, using standard Coq)
- algebra1.v, algebra2.v, algebra3.v, algebra4.v: algebraic structures

HTML version of the code, formatted by Coqdoc

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

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

- gaia sources (mars 2015)
- gaia sources (july 2016)
- gaia sources (november 2017)compiles with coq8.4pl6, ssreflect1.5.0 and math-comp-1.5.0 .
- gaia sources (october 2018) coimpiles with coq 8.8.1 mathcomp 1.7.
- jset.v: Definition of sets by Carlos Simpson
- jfunc.v: Definition of functions by Carlos Simpson
- Version 2 of RR 7150
- Version 3 of RR 7150
- Version 7 of RR 7150
- Version 4 of RR 6999