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

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

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.

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

Algebraic structures

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

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

Previous version

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

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