Gaia stands for: Geometry, Algebra, Informatics and Applications. This Web page describes the Project and the Software associated to it.

The people

José Grimm (Marelle Team)

with the help Alban Quadrat (Disco Team)

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 (version 1.3); the files have been compiled by Coq version 8.3pl1.

Theory of sets

This corresponds to the E.II (the chapter "Theory of sets" from the book "Theory of sets")

sset1.v: Set theory
sset2.v: Correspondences
sset3.v: Union, Intersection, Products
sset4.v: Equivalence relations
ssete1.v: Exercises for E.II
set1.v, set2.v set3.v, set4.v, sete1.v (same files as above, using standard Coq)

Ordered Sets, Cardinals, Integers

This corresponds to the E.III (the chapter "Ordered Sets, Cardinals, Integers" from the book "Theory of sets")

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
sset11.v: Ordinal numbers
sset12.v: Ordinal numbers (part 2)
sset13.v: Ordinal numbers (part 3)
ssete5.v: Order Types
ssete2.v: Exercises for E.III
ssete3.v: Exercises for E.III (part 2)
ssete4.v: Exercises for E.III (part 3)
set5.v, set6.v, set7.v, set8.v, set9.v, set10.v, set11.v, sete2.v (same files as above, using standard Coq)

Algebra
This corresponds to the book Algebra. (standard Coq)
algebra1.v: Z
algebra2.v: Q
algebra3.v: group/ring/modules definitions
algebra4.v: Bourbaki, Algebra I-1

HTML

HTML version of the code, formatted by Coqdoc

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

Documentation

RR6999 (version 4) The Research Report describes E.II (the Theory of Sets).

XML version of the previous document, translated by Tralics

RR 7150 (version 3). The Research Report describes E.III (Ordered sets, Cardinals, Integers).