José Grimm
email: jose.grimm@inria.fr

Implementation of Bourbaki's Elements of Mathematics in Coq: Part Two, From Natural Numbers to Real Numbers

This paper describes a formalization of the first book of the series "Elements of Mathematics" by Nicolas Bourbaki, using the Coq proof assistant. In a first paper published in this journal, we presented the axioms and basic constructions (corresponding to a part of the first two chapters of book I, Theory of sets). We discuss here the set of integers (third chapter of book I, theory of set), the sets Z and Q (first chapter of book II, Algebra) and the set of real numbers (Chapter 4 of book III, General topology). We start with a comparison of the Bourbaki approach, the Coq standard library, and the Ssreflect library, then present our implementation.

INTRODUCTION 1.1 The Number Sets

This paper is the second in a series that explains our work on a project (named Gaia), whose aim is to formalize, on a computer, the fundamental notions of mathematics. We have chosen the "Elements of Mathematics" of Bourbaki as our guideline, the Coq proof assistant as tool, and ssreflect as proof language. As explained in the first paper [START_REF] Grimm | Implementation of Bourbaki's Elements of Mathematics in Coq, part one theory of sets[END_REF], our implementation relies on the theory of sets, rather than a theory of types.

In this paper we focus on the construction of some sets of numbers. Starting with the set of integers N (which is an additive monoid), one can define Z as its group of differences (this is a ring), then Q as its field of fractions (this is naturally a topological space), then R, the topological completion (that happens to be an Archimedean field); next comes the algebraic closure C of R. In this presentation, each set has a structure (group, ring, topology, order, etc), and the next set in the series is the unique (modulo isomorphism) extension satisfying some property.

There are many different implementations of these number sets in many proof assistants [START_REF] Boldo | Formalization of Real Analysis: A Survey of Proof Assistants and Libraries[END_REF]; we shall consider here only the Coq system, that uses a higherorder type theory and an intuitionist logic (the axioms of Excluded Middle and Choice are not taken for granted). We shall compare our implementation with two libraries: the Coq standard library and the Mathematical Components library 1 (see discussion in subsection 1.4). In Coq the set of natural integers comes for • José Grimm free; a typically untyped notion is that of an ordinal (hence that of a cardinal)2 . In a theory of sets, the set of finite ordinals is the natural candidate for N. From N one gets Z and Q in a straightforward way (the only question being: should a fraction be in lowest terms3 ). The case of real numbers is more interesting: one can define the set of classical reals R as the set of classes of Cauchy sequences, for some equivalence relation; there are alternative presentations, in any case the Axiom of Choice is required. This set is however larger than the set of constructive real numbers. The set R is defined by an axiom in the standard library, not implemented in MathComp.

One possible implementation could be to follow Bourbaki (see discussion in subsection 1.3): Book I describes the theory of sets, introduces the order structure, and studies the set of natural numbers N; Book II defines and studies algebraic structures (monoid, group, ring, field, algebraic closure, etc) and defines Z and Q; Book III considers general topology and defines R and C. Implementing the whole of these three books is a challenge. Our ambition is more modest: provide a setting in which formulas of the form 2 n ≤i<2 n+1 1/(s i s i+1 ) = 1 can be expressed and proved correct [Here s n is a sequence of integers defined by induction, see equation ( 9) below].

Our starting point is an implementation of Book I of Bourbaki (Theory of Sets, [START_REF] Bourbaki | Elements of Mathematics, Theory of Sets[END_REF]) with axioms designed by Carlos Simpson [START_REF] Simpson | Computer theorem proving in math[END_REF][START_REF] Simpson | Set-theorical mathematics in Coq[END_REF]; the implementation of Chapter 1 and 2 ("Description of formal mathematics", and "Theory of sets") has been presented in [START_REF] Grimm | Implementation of Bourbaki's Elements of Mathematics in Coq, part one theory of sets[END_REF], and a brief summary will be given below in subsection 1.5. Note that section 2 describes N and covers almost the whole of Chapter 3 ("Ordered sets, cardinals, integers") of Bourbaki. The next three sections describe Z, Q and R and some of their properties, using ideas from various sources. In the conclusion, we shall compare our implementation with the two Coqlibraries, and discuss further work on this subject.

Structures

We mentioned above that all the number sets had a structure; this means that, associated to the set, are operations with specific properties. For instance, in a set E, one can consider an addition + and a comparison ≤; if some property of + holds, then E is called a group, if some property of ≤ holds, then E is called an ordered set, if some additional property of + and ≤ holds, then E is called an ordered group. Every ordered group is both a group and an ordered set (the converse may be false). Once a property has been proved for a given structure (say a group), it can be applied to all sets endowed with that structure. If two sets E, F are endowed with the same structure, a function f : E → F compatible with the operations is called a morphism (when bijective, it is an isomorphism). For instance the canonical injection Z → Q is a ring morphism. In the special case where E ⊂ F and f is the canonical injection, then the structure of E is said to be induced by Theory of Sets / From natural numbers to real numbers • 3 that of F (more simply one says that E is a subgroup of F ); for instance, the image of the canonical injection Z → Q is a subring of Q, ring-isomorphic to Z. So, the question becomes: what is a structure, a sub-strucrure, a morphism, and how can these notions be implemented in computer.

Bourbaki has a whole Chapter of Book I that deals with structures. Its definitions are so far from the common use that nobody (even Bourbaki himself) uses them; an implementation of these ideas in Gaia has started. Carlos Simpson [START_REF] Simpson | Computer theorem proving in math[END_REF][START_REF] Simpson | Set-theorical mathematics in Coq[END_REF] (who designed the axioms used in Gaia) explains a possible design for structures. For instance an ordered group is a record 4 with three fields: the underlying set, the graph of the addition, the graph of the comparison, together with an axiom (that asserts some facts of the fields of the record). This idea seems nice and effective but only partially implemented in Gaia for lack of time.

In a higher-order type theory, like Coq, one can consider + as a notation for a function add of type E → E → E (provided that the set E is type), hence define an ordered group structure as the record formed by: the set E, the function add, the function associated to ≤, the unit, and the axioms. The standard library of Coq provides some structures (ring, semi-ring, field), and a way to register instances of these structures, in order to be used by specialized tactics such as ring, field, nsatz, etc, (see the Coq reference manual).

In what follows, we consider the ssreflect library; an example of a commutative group is given in the tutorial [START_REF] Gonthier | An introduction to small scale reflection in Coq[END_REF]; details about effective implementation in ssreflect can be found in [START_REF] Garillot | Packaging mathematical structures[END_REF], for instance, it is explained how a commutative unit ring can be considered either as a commutative ring or as a unit ring (i.e., a ring in which some elements, called units, have a multiplicative inverse). Thanks to the mechanism of coercions and canonical structures, one can write expressions of the form '1:int_comRing' or '(1 / ((1+1):rat_Ring)) <= 1)%R'. In the second expression, the %R marker tells Coq to interpret some notations (here 1, +, /, ≤) in the ring scope. In both expressions, what follows the colon is not a type but an instance of a structure (Z as a commutative ring, or Q as a ring). The coercion mechanism now says that what precedes the colon has as type the carrier of the structure. The first example is equivalent to '1:int' and denotes 1 Z . The second example is more complicated. The denominator belongs to the carrier of the ring structure of Q, the quotient belongs to the carrier of rat_unitRing, the unit ring structure of Q (this is the smallest structure in which it makes sense). The whole expression belongs to the carrier of rat_numDomainType (this is the smallest structure on Q that has a comparison). After that, Coq finds that each 1 is the unit of the underlying ring of the structure (i.e., something that simplifies to 1 Q ). The important point here is that, not only Coq finds an interpretation of all notations, but the expression is trivially true.

A typical use of structures is the following: assume that E is a set, + a law of composition on E, that is associative and commutative, if a, b, c, d are four elements of E, then (a + b)

+ (c + d) = (a + c) + (b + d). This is called addrACA • José Grimm
in the case of a Z-module5 (or a ring), mulrACA in the case of a commutative ring (when + is replaced by multiplication). Other examples are addnACA, minnACA, setUACA (addition on N, minimum on N, union of finite sets). It is transparent to the user whether these lemmas are an instance of the general lemma mulmACA or a particular case. (In Gaia, there is no generic structures, but we provides lemmas of this form in each particular case).

The library provides a generic sum i∈I x i where the index belongs to a finite set (a list, an interval I n , or a more general interval [n, m[). The only assumption is that the operator has a unit (this means that one cannot take the minimum of a list of integers; but one can consider finite unions and intersections). This is a very powerful tool; again this is not implemented in Gaia. In the other hand, Gaia handles infinite sums (of cardinals, ordinals, etc), and one could define a sum over an infinite index, provided that all but a finite number of values are equal to the unit.

Constructing the real numbers in Bourbaki

We explain in this section how the sets N, Z, Q, and R with their algebraic structures are defined in Bourbaki.

1.3.1

The set of natural numbers. Bourbaki [Bou68] defines the cardinal Card(X) of a set X to be a representative of the equivalence class of X for the relation "there exists a bijection of X onto Y ", denoted Eq(X, Y ), and written "X and Y are equipotent". This equivalence class is not a set, so that the actual definition is τ Z (Eq(X, Z)). Here τ is the Bourbaki's equivalent of Hilbert's epsilon operator; the definition implies that Card(X) is equipotent to X, and that Eq(X, Y ) is equivalent to Card(X) = Card(Y ). These are the characteristic properties of the cardinal operator. The cardinals of the sets ∅, {∅} and {∅, {∅}} are denoted by 0, 1 and 2. Note that 0 = ∅, and this is the only case where the cardinal of a set can be explicitly computed.

The cardinal of the disjoint union S or cartesian product P of a family of cardinals (A i ) i∈I (i.e., the set of all (x, i), where i ∈ I and x ∈ A i , or the set of all functional graphs x with domain I such that x i ∈ A i ) is called the cardinal sum or cardinal product of the family, denoted i∈I A i or i∈I A i . Replacing A i by an equipotent set replaces S or P by an equipotent set, thus leaves the cardinal unchanged. Addition and multiplication are associative and commutative; in particular, the sum and product of two cardinals is a cardinal, denoted X + Y and X • Y . The cardinal of the set Q of mappings B → A is denoted A B (this is commonly called "A to the power of B", but for Bourbaki, the power of a set is its cardinal, so that "the power of the continuum" is the cardinal of R). Replacing A or B by equipotent sets replaces Q by an equipotent set, and leaves the cardinal unchanged.

The relation "X and Y are cardinals and X is equipotent to a subset of Y " (i.e., there is an injection f : X → Y ), denoted X ≤ Y , is a well-ordering of the collection of cardinals, thanks to Zermelo's theorem. Every cardinal x has a successor x + such Theory of Sets / From natural numbers to real numbers • 5 that x < x + , and for no y do we have x < y < x + . Obviously x + 1 ≤ x + ≤ 2 x . An integer is a cardinal x such that x = x + 1. In this case, x + 1 is the successor of x (the Generalized Continuum Hypothesis asserts that, if x is not an integer, then

x + = 2 x ).
There is a principle of induction: if p holds for zero and if for every integer n, p(n) ⇒ p(n + 1), then p holds for every integer. By the Axiom of Infinity, there is a set formed of all integers, denoted N. This set is well-ordered by ≤, is stable by addition, multiplication; functions can be defined by induction on N.

1.3.2 Rational integers. Bourbaki defines the set of rational integers in [START_REF] Bourbaki | Elements of Mathematics, Algebra I[END_REF] (Algebra, Chapter I, section 2, paragraph 5) as the group of differences of N. This is the least (in some sense) superset of N for which addition induces a group. More precisely: "The elements of Z are by definition the equivalence classes determined in N × N by the relation between (m 1 , n 1 ) and (m 2 , n 2 ) which is written m 1 + n 2 = m 2 + n 1 ; an element m of N is identified with the class consisting of the elements (m + n, n), where n ∈ N; it admits as negative in Z the class of elements (n, m + n). Every element (p, q) of N × N may be written in the form (m + n, n) if p ≥ q or in the form (n, m + n) if p ≤ q; it follows that Z is the union of N and the set of negatives of the elements of N."

Let φ + (m) be the first class mentioned above, and φ -(m) the second, so that φ -(m) = -φ + (m). The last statement of Bourbaki can be written as: Z is the union of the images of φ + and φ -; moreover, these two functions are injective, and the intersection of the two images is the singleton {0}; the Coq standard library makes zero exceptional; the ssreflect library shifts φ -, and Gaia disregards φ -(0).

Addition is characterized by φ

+ (a)+φ + (b) = φ + (a+b), φ -(a)+φ -(b) = φ -(a+b), φ -(a) + φ + (b) = φ + (b) + φ -(a) and φ + (a) + φ -(b) is either φ + (a -b) when a ≥ b or φ -(b -a) otherwise. The relation y -x ∈ φ + N , denoted x ≤ y,
is a total order relation on Z which extends the order relation ≤ on N (i.e., φ + is an order isomorphism on its image). This order is invariant under translation (i.e., x ≤ y if and only if x + z ≤ y + z).

Multiplication is defined in Bourbaki in paragraph 6. He says that, if E is a monoid, and x ∈ E, there is a unique homomorphism f : N → E such that f (1) = x. This is denoted in ssreflect by x *+ n or x ^+ n in the case of a ring (that can be considered a monoid for both operations). Moreover, if x is invertible, there is a unique homomorphism g : Z → E such that g(1) = x, it coincides with f on N. The ssreflect library provides x *-n and x ^-n for the case of negative numbers, and x *~n for rational integers. Multiplication on Z can be defined by taking (Z, +) for E.

Rational numbers.

In section 8, paragraph 11 of [START_REF] Bourbaki | Elements of Mathematics, Algebra I[END_REF], Bourbaki notices that Z is a principal ideal domain, thus defines gcd and lcm. In section 9, paragraph 4, he defines Q as the field of fractions of Z. "Every rational number is thus of the form a/b where a and b are rational integers with b = 0 (and we may even take b > 0). Q + is used to denote the set of rational numbers of the form a/b with a ∈ N and b ∈ N * ." This set is stable by addition and multiplication; the

• José Grimm union of Q + and the set of opposites of Q + is Q, the intersection being {0}; finally Q + ∩ Z = N ("Obviously N ⊂ Z and N ⊂ Q + . Conversely, if x belongs to Z ∩ Q + ,
it is a rational integer; there exist two rational integers a and b with a ≥ 0, b > 0 and x = a/b, whence a = bx; if x ∈ N, then -x > 0, whence -a = b(-x) > 0 and consequently a < 0 contrary to the hypothesis"). These relations are numbered from (1) to (5) by Bourbaki.

[Note: the proof of Q + ∩ Z = N lacks the legendary rigor of Bourbaki. First it makes sense only if one identifies N as a subset of Z and Z as a subset of Q. So, how should x = a/b and a = bx be interpreted, and why are these statements equivalent? Is a proof by contradiction needed, knowing that b > 0 and bx ≥ 0 in Z implies x ≥ 0? ] "Given two rational numbers x and y, we write x ≤ y if y -x ∈ Q + . It is easily deduced from (1), (3) and (4) that x ≤ y is a total ordering on Q, from (5) that this relation induces the usual order relation on Z. Finally from (1), it follows that the relations x ≤ y and x ≤ y imply x + x ≤ y + y and from (2) that the relation x ≤ y implies xz ≤ yz for all z ≥ 0 and xz ≥ yz for all z ≤ 0 (cf. VI, §2, no. 1)." (Chapter 6 of the Book of Algebra deals with ordered groups and fields). Bourbaki concludes this short presentation by defining the sign and absolute value of a rational number. 1.3.4 Real numbers. Real numbers are defined in Chapter 4 on the Book of Topology [START_REF] Bourbaki | Elements of Mathematics, General Topology[END_REF]. The first claim is that there is a unique topology on Q, compatible with the additive structure such that a fundamental system of neighborhoods of zero is the set of intervals ]-a, a[. This is a discrete Hausdorff topology; its completion is the set of real numbers, addition and multiplication being the continuous function extensions of those of Q, the ordering is defined by the set of positive numbers (the adherence of the set of positive rational numbers). This is a short introduction to real numbers; a whole book is dedicated to the study of functions of a real variable.

Real numbers in Coq

We shall explain how integers, rational and real numbers are implemented, both in the standard Coq library and in ssreflect6 . To begin with, the natural numbers are defined by There is an induction principle, that allows one to define functions by induction, for instance addition, subtraction, multiplication, etc. We give the definition of comparison and maximum of the standard library (note that max is recursive in its first argument). The ssreflect library provides a file ssrnat.v, that states arithmetic properties about natural numbers, using the same operations as above. However, boolean equality is preferred. For instance, we give the statement that a product of two naturals is equal to 1 if and only if both factors are equal to 1. Comparison is redefined by m ≤ n when m -n is zero; this allows a simple definition of the maximum. Note: most functions of the standard library with two arguments call them n and m; the ssreflect library uses alphabetic order (m and n) and is generally more systematic regarding naming conventions. The name of arguments is irrelevant, except for implicit arguments, when the function is not fully applied. For instance 'leq_trans' takes 5 arguments, three natural numbers n, m, p, and proofs of m ≤ n, n ≤ p and returns a proof of m ≤ p. The first three arguments can be deduced from the type of arguments 4 and 5, hence are implicit. You can however say '@leq_trans 3'; this is the same as '(leq_trans (n:=3))'. Logically, n is the second argument; it is placed first in the list since m and p can be deduced from the conclusion m ≤ p.

A positive number corresponds to a non-zero natural number written in base two: each digit is represented by xO or xI, but the leading digit one is represented by xH. A member of N is zero or positive. The ssreflect library does not use these two datatypes, but provides bijections between nat and N, and proofs that addition, multiplication, and exponentiation are morphisms.

The standard library defines Z as the disjoint union of two copies of positive, (sometimes called pos and neg), together with a zero, and defines all usual operations (we give opposite as an example). All properties of an ordered ring are satisfied. Moreover, Coq provides a nice concrete syntax (for instance, 17 can be parsed as a nat, a positive, an N, or a Z).

Note: notations can be overloaded, so that 0 may represent O, N0, Z0, or the zero of a ring; moreover, a function f (for instance the canonical injection N → Z) may be declared as a coercion, so that f (x) can be input as x. Each notation is defined in a scope (in the example above, le is defined together with its notation in the scope of natural numbers). Some notations may be ambiguous: for instance, if A and B are two types, with a coercion f , two operations g A and g B with the same • José Grimm notation g, then g(x) : B may stand for f (g(x)) or g(f (x)). For this reason there is a way to indicate in which scope should some notations be resolved. The ssreflect library defines (in ssrint.v) a datatype int, formed of two copies of nat; one corresponds to the injection N → Z, the second associates to n the opposite of n + 1. We show here the definition of the opposite function. [Here %N says that the argument before it should be in parsed in the scope whose name is N; it is not necessary here as 'n.+1' is a non-overloaded notation for 'S n'. The trouble is that the standard and ssreflect libraries use the same N for different scopes.] Note that the datatype is CoInductive, thus lacks a principle of induction, but one is provided explicitly as: in order for P (z) to hold for all z ∈ Z, it suffices that P (0) holds, and for every natural number n, P (n) implies P (n + 1) and P (-n) implies P (-(n + 1)). This is for instance used to show associativity of addition. This datatype is embedded with a number of structures (Z-module, ring, real domain, etc). In particular there is an order and a norm, compatible with the ring operations, and satisfying the triangular inequality |x + y| ≤ |x| + |y|. Every group is a Z-module (one can define x n when x is in the group and n ∈ Z, and this operation satisfies the usual properties). On a ring R, two operations are defined: x.n and x n , where x is in the ring and n ∈ Z, such that x.2 = x + x and x 2 = x • x (the second operation is most useful when x is a unit, so that x • x -1 = 1; this is the case when x is a non-zero element of a field). On a real field, these operations satisfy some monotonicity properties (for instance: if x ≥ 0, y ≥ 0 and n = 0, then x n = y n is equivalent to x = y). On every real domain, one can define a sign function s(x) whose value is -1, 0, or 1 depending on whether x < 0, x = 0 and x > 0 (in fact, there are two such functions, with value in the domain or in Z). Among other properties, s(a

• b) = s(a) • s(b). In the case of Z, if a(x) is the absolute value of x, we have x = a(x) • s(x) and a(x) = x • s(x).
In summary: the library defines many algebraic structures, some are classic like group, ring, field, other are a bit involved like real field or Archimedean field, and Z is an example of these structures.

The standard library defines Q and a relation Qeq denoted here x ∼ y:

• 9 Record Q : Set := Qmake {Qnum : Z; Qden : positive}. Notation QDen p := (Zpos (Qden p)). Definition Qeq (p q : Q) := (Qnum p * QDen q)%Z = (Qnum q * QDen p)%Z.

The relation is an equivalence and Q is called a setoid. All operations, like addition, as well as comparison, are compatible with ∼. Addition is associative modulo ∼. The standard library has a bunch of functions that allow rewrite to replace x + (y + z) by (x + y) + z in situations where this is allowed. On the other hand, one can reduce fractions x into x by extracting gcds (the definition here is strange, as it must cope with the fact that numerator and denominator have different types, notations are sometimes a bit folkloric), in such a way that x ∼ x, and x ∼ y implies x = ȳ. Note that x = x if and only if the numerator and denominator of x are coprime; thus, if y is x, we have ȳ = y.

Definition Qred (q:Q) := let (q1,q2) := q in let (r1,r2) := snd (Z.ggcd q1 ('q2)) in r1#(Z.to_pos r2). Lemma Qred_correct : forall q, (Qred q) == q. Lemma Qred_complete : forall p q, p==q -> Qred p = Qred q. Lemma Qred_involutive : forall q:Q, Qred (Qred q) = Qred q.

An extension to QArith.v is the following definition:

Record Qc : Set := Qcmake { this :> Q ; canon : Qred this = this }.

A element X of type Qc is a fraction X v and a proof X p of X v = X v . The nontrivial point with this definition is to prove that

X v ∼ Y v implies X = Y (that X v = Y v is obvious, so that Y p becomes a second proof of X v = X v ,
a non-trivial result says that two proofs of equality for a type A are equal if equality is decidable for this type, which is the case here). Since Qred is involutive, if x is a rational number, there is X (denote it q(x)) such that X v = x. Then x, y → q(x + y) defines an addition on Qc. Subtraction, multiplication, division are similarly defined; the result is a ring and a field (in the sense of the ring and field tactics).

The ssreflect library defines (in file rat.v) the set of rational numbers similarly to Qc, where both numerator and denominator have the same type int; the condition "x = x" is replaced by a boolean condition. Almost every ssreflect datatype is an instance of eqType (the mechanism of Canonical Structures makes this transparent to the user); this means that there is a boolean equality x == y (not to be confused with the == used above as notation for Qeq) such that x == y ⇔ x = y. The boolean equality of int obviously induces a boolean equality on rat.

• José Grimm _ : (0 < valq.2) && coprime '|valq.1| '|valq.2| }. Lemma rat_eqE x y : (x == y) = (numq x == numq y) && (denq x == denq y).

Assume x ∼ y; this means x = (a, b), y = (c, d) and ad = bc. Since b is coprime with a, it divides d; similarly, d divides b. Since these two quantities are > 0, it follows b = d, thus x = y. This is expressed in the next lemma, using boolean equality. One deduces a function fracq (the equivalent of Qred) that converts a pair of integers into an element of Q by extracting gcds. This is the identity when applied to an element of Q, and produces equal values when applied to equivalent pairs.

Lemma rat_eq x y : (x == y) = (numq x * denq y == numq y * denq x). Fact valqK x : fracq (valq x) = x. Fact fracq_eq x y :

x.2 != 0 -> y.2 != 0 -> (fracq x == fracq y) = (x.1 * y.2 == y.1 * x.2).
All usual operations on Q are defined via fracq, and Q is a field. Now fracq becomes useless as 'fracq x' it is equal to N (x)/D(x), where N (x) and D(x) are the numerator and denominator of x, coerced from Z to Q. The set of all rational numbers with denominator 1 is canonically isomorphic to Z and is a subring; the set of these elements that are moreover positive is canonically isomorphic to N and is a sub-semiring. Define a/b ≤ c/d by ad ≤ bc. This makes Q a real field. It is

Archimedean (if x = a/b and n = |a| + 1, then x < n and x ∈ N). For any number field R, there is a morphism Q → R (it maps a/b to f (a)/f (b) where f : Z → R is the canonical morphism; note that f (b) is not zero).
Finally, rat is declared as a ring and a field for the ring and field tactics.

Consider now real numbers. The standard library defines them via a sequence of axioms. It is assumed that there is a set R, constants 0, 1, +, -, * , < and u such that:

• 11 Rmult_lt_compat_l: ∀x, y, z, 0 < z and x < y implies z * x < z * y. archimed: ∀x, u(x) -1 ≤ x < u(x). completeness: Every non empty bounded subset of R has a least upper bound.

Notes. That the ordering of R is total is expressed as: it is decidable that one of x < y, x = y or y > x holds; these conditions are mutually exclusive by antisymmetry. One can define by induction the canonical injection INR:N → R, thus the canonical injection IZR:Z → R. In the axiom archimed, the quantity u(x) is in Z, coerced to R (the axiom has u(x) -x ≤ 1 instead of u(x) -1 ≤ x). This can be seen equivalent to the ssreflect definition: there is a natural number v(x) such that |x| < v(x). If n is the least natural satisfying this property, then n -1 ≤ |x| < n; this covers the case of positive numbers; defining u(x) for negative numbers is easy.

The last axiom says the following. Let E be a real predicate (an object of type R → Prop). An upper bound m is such that E(x) implies x ≤ m, and E is bounded if such an m exists. A least upper bound is an upper bound m such that for every upper bound b, we have m ≤ b (it is sometimes better to say: for every b such that b < m, there exists x ∈ E such that b < x).

One deduces: every Cauchy sequence has a limit. In fact, if (x n ) n∈N is Cauchy, it is bounded, so that one may consider v n = sup n<k x k . This sequence is decreasing, and has a lower bound, thus converges to v (in fact to inf v n ). Clearly v is the limit of (x n ) n . On the other hand, every real number x is the limit of a sequence of rational numbers: let

x n = u(2 n x)/2 n , by archimed we have x n -1/2 n ≤ x ≤ u n , hence |x -u n | ≤ 1/2 n .
The standard library provides many results about real numbers. For instance, the cosine function is continuous and has a sign change between 7/8 and 7/4. By the intermediate value theorem, there is a zero there; call it π/2. We have then the celebrated Machin Formula π/4 = 4 arctan(1/5) -arctan(1/239). The ssreflect library, on the other hand, does not provide real numbers, but the MathComp library7 provides in cauchyreals.v a definition of real numbers as Cauchy sequences over some real field F . A real number x is a map N → F satisfying the following property:

Lemma crealP (x : creal) : {asympt e : i j / '|x i -x j| < e}.

This has to be understood as: there is a function m : F → N such that, if > 0, for every i and j such that m( ) ≤ i and m( ) ≤ j, it holds that |x(i) -x(j)| ≤ . Two real numbers x and y are called unequal if for some > 0, we have 3 ≤ |x(m x ( )) -y(m y ( ))|. This means: there is > 0, such that, if i is big enough then ≤ |x(i) -y(i)|. If moreover x(m x ( )) + 3 ≤ y(m y ( )), one writes x < y. This says that if i is big enough then x(i) + ≤ y(i). If x and y are not unequal, then one • José Grimm writes x == y; this is an equivalence relation (but not boolean); if y < x is false, one writes x ≤ y (again this is not a boolean relation); it is a preorder, compatible with x == y. One has for instance:

Lemma eq_crealP (x y : creal) : {asympt e : i / '|x i -y i| < e} -> (x == y)%CR. Lemma asympt_le (x y : creal) (le_xy : (x <= y)%CR) : {asympt e : i / x i < y i + e}.

The sum and product of two real numbers x and y are the sequences i → x(i) + y(i) and i → x(i) * y(i) (as every Cauchy sequence is bounded, the product of two real numbers is real). The operations (addition, multiplication, etc, including evaluation of polynomials with coefficients in F at a real number) are compatible with the equality.

This is a partial implementation of real numbers (for instance, associativity of addition is not shown), and could be completed; it it is however sufficient to implement the set of real algebraic numbers, as described in [START_REF] Cohen | Construction of real algebraic numbers in Coq[END_REF].

The axioms of Gaia

Our work relies on an axiomatization of the theory of Zermelo-Fraenkel as described in [START_REF] Grimm | Implementation of Bourbaki's Elements of Mathematics in Coq, part one theory of sets[END_REF]; the axioms are the following:

Parameter Ro : forall x : Set, x -> Set. Axiom R_inj : forall x : Set, injective (@Ro x). Axiom extensionality : antisymmetric_r sub. Parameter IM : forall (x : Set) (f : x -> Set), Set. Axiom IM_P : forall x f y, inc y (IM f) <-> exists a : x, f a = y. Axiom p_or_not_p: forall P:Prop, P \/ ~P. Parameter chooseT : forall t : Type, (t -> Prop) -> inhabited t -> t. Axiom chooseT_pr: forall (t : Type) (p : t -> Prop) (q : inhabited t), (exists x, p x) -> p (chooseT p q).

We first assume that there is some function Ro, such that, if x is a set, and a is of type x, then 'Ro x a' is a set; for any x, the function is injective; note that x is an implicit argument of Ro, since it is the type of a. The relation "there is some a such that 'Ro x a = t' " is denoted by 'inc t x' and interpreted as t ∈ x. The relation "for all t, t ∈ x implies t ∈ y" is denoted 'sub x y' and interpreted as x ⊂ y. Our second axiom (Axiom of Extent) says: if x ⊂ y and y ⊂ x then x = y. We shall assume that, whenever x is a set, f a function on x (an object of type x → Set), there is some set I, such that y ∈ I if and only if there is some a of type x such that f (a) = y. This implies the Axiom of Replacement: if f maps sets to sets and if X is a set, there is a set Y , denoted {f (x), x ∈ X} such that y ∈ Y if and only if there is x ∈ X such that y = f (x). It also implies a weaker form: if X is a set, P a predicate, there exists a set Y , denoted {x ∈ X, P (x)} or 'Zo X P', such that x ∈ Y if and only if x ∈ X and P (x) holds. If a, b, X are sets, we also deduce the existence of: the doubleton {a, b} such that x ∈ {a, b} if and only if x = a or x = b, the union X such that x ∈ X if and only if there is y such that x ∈ y • 13 and y ∈ X, and the power set P(X), such that x ∈ P(X) if and only if x ⊂ X. These sets are unique by the Axiom of Extent. In summary, our theory satisfies the axioms of Zermelo-Fraenkel.

Generally, in a theory of sets, one considers a collection of objects, called sets, such that an object is a set if and and only if it can be constructed via one of the five constructions given above. Since the empty collection satisfies the property, one assumes that there is at least one set, hence the empty set. Since V ω (the collection of hereditarily finite sets) satisfies this property, one moreover assumes that there is at least one infinite set. Sometimes the Axiom of Foundation is assumed (but usual mathematics does not depend on it) or its converse (this requires a modification of the Axiom of Extent). Our approach is different: we assume that every Coq object of type Set is a set, and postulate the existence of some function Ro.

The Axiom of Infinity says: there is an infinite set. This can be interpreted as: there is a set X, and a function f : X → X which is injective and not surjective. For instance, nat is infinite: if N (n) is '@Ro nat n', then for any n of type nat, we have

N (n) ∈ nat; if g(n)
is the pair (N (n), N (n + 1)), then 'IM g' is the graph a function that maps N (n) to N (n + 1); it is injective but not surjective8 . Traditionally, the Axiom of Infinity says that there is a set X satisfying I(X): "∅ ∈ X and ∀x, x ∈ X ⇒ x + ∈ X" where x + is x ∪ {x} (One can show that the least subset Z of X that satisfies I is the set of all finite ordinals; the subset Y of X formed all ordinals of X is infinite as x → x + becomes injective). For instance, if f : nat → Set is defined by induction via f (0) = ∅ and f (n + 1) = f (n) + , then IMf satisfies I. One can define a set with an arbitrary cardinality n, for instance Empty_set is empty and bool has two elements. The current version of Gaia differs slightly from the description of [START_REF] Grimm | Implementation of Bourbaki's Elements of Mathematics in Coq, part one theory of sets[END_REF]: for instance emptyset is now a CoInductive variant of Empty_set, and the definition of the set with two elements (a copy of bool) has been removed. In fact, {x, y} is now defined by 'IM (fun z => if z then x else y)' (note that z has type bool). Write 0 instead of ∅, 1 instead of {0, 0} and 2 instead of {0, 1}. Then 2 is a set with exactly two elements, and is called "the canonical doubleton" (the Gaia names of these sets are C0, C1, C2).

We shall assume the Axiom of Choice in the form: whenever t is a type, q a proof that it is inhabited, and p a proposition over t, then there exists a set C such that, if p holds for some value, it holds for C. We shall almost exclusively consider the case where the type t is Set, inhabited by ∅. In this case, the axiom of choice says that there is a set τ x (P ), such that (∃x)P implies P (τ x (P )). In fact, Bourbaki uses P (τ x (P )) as the definition of (∃x)P . Here τ x (P ) is some expression formed of P by binding the free variable x (thus is independent9 of x) and P (τ x (P )) denotes the expression obtained from P by replacing every occurrence of x by τ x (P ); it is thus independent of x. The quantity τ x (p(x)) is denoted in Gaia by 'choose p', and

• José Grimm
the axiom of choice is: 'ex p → p(choose p)'. In the case where there is a unique element in some set E satisfying some property p(x), this element is {x ∈ E, p(x)}, denoted 'select p E', and the axiom of choice is not needed. Let E be a set, P be 'x ∈ E', so that (∃x)P is equivalent to E = ∅; in this case, we denote by 'rep E' (in short r(E)) the quantity τ x (P ). We have then: ∀E, E = ∅ ⇒ r(E) ∈ E. One easily deduces Zermelo's theorem: every set can be well-ordered (see [START_REF] Grimm | Implementation of Bourbaki's Elements of Mathematics in Coq, part one theory of sets[END_REF]).

Bourbaki manipulates only two kinds of objects: terms and relations, this corresponds in Coq to Set and Prop, and he allows quantification only over terms (i.e., sets). There is no equivalent of 'fun x => x <> emptyset' or nonempty of type Set → Prop. However "x = ∅" is a relation with a free variable; let's call it P . Similarly x ∪ y is a term with two free variables; let's call it Q. One may replace x in P by Q, and then y by ∅. The result is denoted (∅|y)(Q|x)P ; if the order of substitutions is exchanged one gets ((∅|y)Q|x)P ; this is traditionally denoted P (Q(∅)), but this is ambiguous. For this reason, Bourbaki introduces the notation T x (instead of a double bar, there is a specific symbol, not used by anyone else): "if A is an assembly and we are interested particularly in a letter x, or two distinct letters x and y (which may or may not appear in A), we shall often write A x or A x, y . In this case we write A B instead of (B|x)A. We denote by A B, C the assembly obtained by simultaneously replacing x by B and y by C whenever they occur in A (note that x and y may occur in B and in C)." So, P Q x, ∅ means ((∅|y)Q|x)P . Note that, if x appears in A, and B is a relation, then one of A x and A B is ill-typed; for this reason Bourbaki uses A B only when B is a term. The Axiom of Excluded Middle says that a relation R is either true or false. One has to be careful when the relation depends on a parameter: in fact Bourbaki notes: "Let R be a relation; it is the same whether we state the theorem R or the theorem (∀x)R, or the metamathematical rule: if T is any term then (T |x)R is a theorem." If P is the relation introduced above, then, obviously, (∀x)P and (∀x)¬P are false, so neither P nor ¬P are theorems.

Equality is defined by Bourbaki via two axiom schemes. Scheme S6 says that if U and V are terms and R x is a relation, then (U = V ) ⇒ (R U ⇔ R V ) is an axiom; scheme S7 says that if P and Q are relations, then ((∀x)(P ⇔ Q)) ⇒ (τ x (P ) = τ x (Q)) is an axiom. Quoting Bourbaki, "Intuitively, the scheme S6 means that if two objects are equal, they have the same properties. Scheme S7 is more remote from everyday intuition". One consequence of S7 is reflexivity of equality, one deduces symmetry and transitivity. Another consequence is Criterion C44: (T = U ) ⇒ (V T = V U ), whenever T , U and V are terms. Proof. Assume T = U ; by symmetry we have

U = T . Substitute this relation in V x = V U ; we get V U = V U ⇔ V T = V U .
The conclusion follows by reflexivity. This is exactly how rewrite works in Coq, while scheme S6 is eq_ind. For this reason we shall use Coq's equality in whatever follows. What about S7? Let P and Q be equivalent propositions. Assume that we know that there is a set E, such that P (x) implies x ∈ E, or such that ∃x ∈ E, P (x). Then τ x (P ) can be replaced by r({x ∈ E, P }). By the axiom of extent, {x ∈ E, P } = {x ∈ E, Q} and S7 holds (this argument explains why S7 is part of the definition of choiceType in ssreflect). On the other hand, consider Card(X) = τ Z (Eq(X, Z)) introduced in section 1.3.1. Let X be a set equipotent to X, so that Eq(X, Z) ⇔ Eq(X , Z). Scheme S7 says

• 15 Card(X) = Card(X ), but since there is no set containing all cardinals, this relation is unprovable in Gaia. Similarly, one cannot prove that two order isomorphic sets have the same order type. The first problem is solved by using a different definition of the cardinal of a set (see below); the second one by introducing an axiom (see section 4.1).

Order relations and ordered sets

A pair (x, y) is a set z from which x and y can be recovered (via x = pr 1 z and y = pr 2 z). It is defined by an Axiom in Bourbaki [START_REF] Bourbaki | Elements of Mathematics, Theory of Sets[END_REF], and as {{x}, {x, y}} in the 1970 French Edition [START_REF] Bourbaki | Éléments de mathématiques, Théorie des ensembles[END_REF]. In Gaia, the constuctor is named J and the two projectors are P and Q.

A graph G is a set such that every element z of G is a pair, say (x, y); the set of all those x, namely pr 1 G , is called the domain of the graph, and the set of all y, namely pr 2 G , is called the range. A graph is functional if for any x in the domain, there is a unique y, such that (x, y) ∈ G; this quantity is called the value of G at x, and denoted G(x) or G x or 'Vg G x'. The quantity 'Lg E f' denotes the functional graph with domain E that maps x to f (x). A sequence is a functional graph whose domain is N. It is generally denoted by (x n ) n , sometimes by n → x n . A finite sequence is a functional graph whose domain is a finite subinterval of N; it may be denoted by (x n ) n<k if the domain is the set of integers < k. A correspondence Γ = (S, T, G) is a triple such that G is a graph whose domain is a subset of S (the source) and whose range is a subset of T (the target). A function is a correspondence such that its graph G is functional and its source is the domain of G. The value of Γ at x, denoted Γ(x) or 'Vf Γ x', is G(x). Functions can be injective, surjective, bijective. If f : E → F is a bijection, then E and F are said to be equipotent; this is an equivalence relation, since compositions of bijections are bijections, and bijections have an inverse for composition. The notations 'f \cf g' and 'f \co g' stand for the composition of two functional graphs or functions. The quantity 'Lf f E F' denotes the function with source E, target F that maps x to f (x) (it makes sense if f (x) ∈ F whenever x ∈ E). The notation f X denotes the set {f (x), x ∈ X} (that exists by the Axiom of Replacement), when f is a functional term; it is extended to functional graphs, correspondences, and functions.

An order is a graph G such that the relation (x, y) ∈ G, written x ≤ y, is an order relation (reflexive, antisymmetric, and transitive); here reflexive means that x ≤ y implies x ≤ x and y ≤ y; this can also be restated as: if E is the substrate of G (the union of the domain and range of G), then x ∈ E implies x ≤ x. One says: G is an order on E instead of the longer: G is an order with substrate E. Finally, for Bourbaki, an ordering is a correspondence Γ = (E, E, G), such that G is an order on E (by abuse of language, G itself is called an ordering). The relation x ≤ y is equivalent to y ∈ Γ x (an abuse of notations for y ∈ Γ {x} ). One says that E is ordered by Γ (or equivalently, by the relation x ≤ y). An ordered set E is an abuse of language: it consists of writing E instead of G or Γ. For instance, Bourbaki says: "whenever N is considered as an ordered set, it is always the ordering (called the usual ordering) defined in §3, no. 2, that is under consideration, unless the contrary is expressly stated".

• José Grimm

In Coq, we do not have the right to use Γ, G, ≤ and E as synonyms. The first simplification consists in ignoring Γ: for us an order is a graph G, it is an order on pr 1 G . If ≤ is a relation then {(x, y) ∈ E × E, x ≤ y}, often denoted E ≤ , is an order on E in some cases. The relation (x, y) ∈ E ≤ may be denoted by x ≤ E y; it is equivalent to "x ∈ E and y ∈ E and x ≤ y". For instance, the relation defined by Bourbaki in §3, no. 2, (which is an order relation, but not an order, since it has no graph), denoted below by ≤ c , defines an order on N, denoted Nat_order, associated to the relation x ≤ N y, which is equivalent to "x ∈ N and y ∈ N and x ≤ c y". If G is an order on F , E ⊂ F , and x ≤ y is "(x, y) ∈ G", then E ≤ is always on order on E, called the order induced by G on E. For instance, in section 4.1, we shall meet BQ_ordering, the usual order on Q, and BQps_ordering, the order induced on Q * + . We shall also meet BQ_int01_ordering, the order induced on the interval ]0, 1[; the associated relation x ≤ I y is equivalent to 0 < q x ≤ q y < q 1.

Cardinal and ordinal numbers

One can define a function by transfinite induction. Let E be a well-ordered set, and T a procedure that constructs a set given another set (technically a λ-term of type Set → Set). For any function f defined on E, let f (x) be the restriction of f to ]←, x[ (this is the set of elements y of E such that y < x10 ). There is a unique surjective function f defined on E such that f (x) = T (f (x) ). This is Criterion C60 of Bourbaki and transfinite_defined in Gaia (see an example on page 37).

The quantity T (g) mentioned above has to be defined whatever g, but the only values that matter are when g is a function whose source is a subset of E. In some cases, there is a set X such that T (g) belongs to X; in this case, the target of f is a subset of X, and it suffices that T be defined on X P(E) . In the general case, some axiom is required for the existence of f (in our case, the axiom of choice). Example: if T (g) is the target of g, the target of the function f so defined is called the ordinal of the well-ordered set E, and denoted ord(E). It happens that no set contains all ordinals. Note that two order isomorphic sets have the same ordinal.

We say that a set x is an ordinal if every transitive subset of x is x or a member of x (y is transitive if a ∈ b, b ∈ y implies a ∈ y). The relation "x and y are ordinals such that x ⊂ y" (denoted x ≤ o y or x ≤ y in what follows) is a wellorder relation on the collection of ordinals. The intersection of a non-empty set of ordinals is an ordinal (this is the least element of the set); the union is also an ordinal (the supremum of the set); the collection of all ordinals has, however, no upper bound. For every ordinal x, the quantity x ∪ {x} (denoted x + as previously) is the successor of x (the least ordinal y such that x < y). Every element of an ordinal is an ordinal, and the relation "a ∈ x, b ∈ x, a ⊂ b" between a and b makes x a well-ordered set, that will be denoted by o(x). For every well-ordered set E, ord(E) is an ordinal, and o(ord(E)) is order isomorphic to E; conversely, if x is an ordinal, then ord(o(x)) = x. (The definition of "ordinal" used here comes from an

• 17
Exercice of Bourbaki, it is equivalent to the definition of von Neumann; for details of implementation, see [START_REF] Grimm | Implementation of Bourbaki's Elements of Mathematics in Coq: Part Two; Ordered Sets, Cardinals, Integers[END_REF]).

Every set x is the substrate of a well-order E, so that there exists an ordinal o(E) equipotent to x; the least such ordinal is called the cardinal of x and denoted by card(x). A cardinal is an ordinal x of the form card(y), i.e., it is such that every ordinal z equipotent to x satisfies x ⊂ z.

Definition cardinal x := (least_ordinal (equipotent x) (ordinal (worder_of x))). Definition cardinalp x:= ordinalp x /\ (forall z, ordinalp z -> x \Eq z -> sub x z).

By definition, card(X) is equipotent to X, and if X and Y are equipotent, they have the same cardinal. This means that our notion of cardinal behaves the same as that of Bourbaki. The cardinal of ∅ is ∅, denoted 0, the cardinal of any singleton is {0}, denoted 1. The sum and product of a family of cardinals is defined as the cardinal of the disjoint union or cartesian product, and x y is the cardinal of the set of functional graphs y → x (this is also the cardinal of the set of functions y → x).

The relation "x and y are cardinals such that x ⊂ y" (denoted x ≤ c y or x ≤ y) is the same as "x and y are cardinals such that x ≤ o y", thus is a well-order relation on the collection of cardinals, and every nonempty set of cardinals has a least element and a least upper bound. If E is a set, F is a subset of E, and f an injection E → F , then E is equipotent to F . (Let D be the smallest set invariant by f that contains E -F . The bijection is the function that is f on D, the identity elsewhere). One deduces the Cantor-Bernstein Theorem: if there is an injection E → F and an injection F → E, then there is a bijection E → F . Moreover, card(X) ≤ card(Y ) if and only if there is an injection X → Y . This means that ≤ c coincides with the Bourbaki definition.

We say that an ordinal x is finite if it is not equipotent to x + ; we say that a set is finite if its cardinal is a finite ordinal. Note that zero (the empty set) is finite, and x is finite if and only if its successor is finite. If x is finite and y ≤ x, then y is finite. The Cantor-Bernstein theorem says that if x is a finite ordinal, its successor is a cardinal (so that x itself is a cardinal). So, a cardinal is finite if and only if x = x + 1. This is the Bourbaki definition of an integer. As mentioned above, nat is an infinite set, so that there exists at least one infinite ordinal, thus a least infinite ordinal ω.

Definition infinite_o u := u \Eq (osucc u). Definition omega0 := least_ordinal infinite_o (cardinal nat).

It is immediate that x < o ω if and only if x is a finite ordinal. Thus ω is the set of all finite ordinals. Since a finite ordinal is a cardinal, ω is also the set of all finite cardinals. It contains zero and is stable by successor; note that every ordinal, that contains zero and is stable by successor, must be infinite, thus is a superset of ω.

• José Grimm

THE SET OF NATURAL NUMBERS N

In what follows, we rename ω as N, and say that an element of N is a natural number. Remember that cardinal comparison coincides with ordinal comparison on N, so that x ≤ N y (see above) makes N a well-ordered set. The quantity card(x + ), denoted 'csucc x', is the successor of x for this ordering; in fact it is the ordinal successor of x when x ∈ N, it is x + 1 whenever x is a cardinal, thus is x when x is an infinite cardinal.

Definition Nat := omega0. Definition natp x := inc x Nat.

Since N is an ordinal, for every non-empty subset X of N, the quantity X is the least element of X. Since ω is the least ordinal that is neither zero nor a successor (i.e., is a limit ordinal), it follows that a natural number is zero or a successor (in this case, it is the successor of its predecessor, x -1) Assume that P is a property, satisfied by at least one integer; if the least integer satisfying P is not zero, it is the successor of some x such that P fails for x, and holds for x + 1.

Lemma sub_natI_prop X (x := intersection X): sub X Nat -> [/\ natp x, forall t, t <c x -> ~(inc t X) & nonempty X -> inc x X]. Lemma wleast_int_prop (prop:property): (exists2 x, natp x & prop x) -> prop \0c \/ (exists x, [/\ natp x, prop (csucc x) & ~prop x]).
Let's state some notation conventions: we cannot use the same notation to denote the zero, addition, comparison of N, Z, etc, since these objects have the same type, so we add a suffix: s for set operations, o for ordinal, c for cardinal, z, q, r, for Z, Q and R. Thus, in the first lemma above, 't <c x' is cardinal comparison, in the second lemma \0c is the cardinal zero (i.e., the empty set). The quantities \2o and \2c denote 2 as an ordinal or a cardinal (these two quantities are equal to the canonical doubleton C2). The ordinal successor of x, 'osucc x' is x ∪ {x}, thus 'x +s1 x'. The quantity 'Nat -s1 \0c', denoted N * , is the set of all non-zero integers. Note that 'x %/c y' and 'x %%z y' are the quotient and remainder in the Euclidean division of x by y (on N and Z respectively), while 'x /q y' is the quotient on Q. Having notations that start with a minus sign or a slash is not really a good idea, as 'rewrite -cprodA /ratp' has to be replaced by 'rewrite -cprodA / ratp'.

Other naming conventions: we use the capital letters A, B, C, etc, in theorem names, similarly to ssreflect (A: associative, C: commutative, D: addition, B: subtraction, I: intersection, U: union, X: cartesian product, P: powerset). Lemmas of the form: P ⇔ Q finish with a P, and B may stand for Bourbaki.

Induction properties

The most important difference between Bourbaki and Gaia concerns the principle of induction. Since Bourbaki uses first order logic, he cannot write: ∀R, H ⇒ C. So he says: in any theory (in which "integer" makes sense), for any formula R, if we

• 19 have a proof of H, then we can prove C. Since R may depend on some parameters, he adds some clues such as n is not a constant of the theory or u is a letter, or sometimes omits them.

C61. Let R n be a relation in a theory T (where n is not a constant of T ). Suppose that the relation R 0 and (∀n)((n is an integer and R n ) =⇒ R n + 1 ) is a theorem in T . Under these conditions the relation

(∀n)((n is an integer ) =⇒ R n ) is a theorem in T .
The proof is by contradiction: if the conclusion were false, there would exist an integer not satisfying R, thus a least such one, either zero or a successor, both alternatives being absurd. We show here the Coq statement and its proof: C62. Let u be a letter and let T u be a term. Then there exists a set U and a mapping f of N onto U such that for each integer n we have f (n) = T f (n) , where f (n) This criterion is the specialization to N of criterion C60 (introduced in section 1.7). It uses the interval I n = [0, n[, while C60 considers ]←, n[. These sets are equal (because 0 is the least element of N) to the set of all x such that x < N n. With the Gaia definition of integers, this is the set of all x such that x < o n, hence n. Whenever possible, we use n instead of I n in the code.

An example of a function f such that f (n) depends on all values f (i) for i < n is EPfun_aux page 37. A more complicated example is the following. Let E be a set, and define a formula over E to be either a = b, a ∈ b (where a and b are in E) or ¬F , F ∨ F , ∀x, F (where F and F are formulas, x ∈ E). This can be trivially defined in Coq via Inductive, and defining the set of free variables (not shadowed by a ∀) is trivial as well. In Bourbaki, one can define by induction a set X n such that a formula of X n+1 is either a formula of X n or satisfies the previous property (with F , F in X n ), then consider the union of these X n . Each formula has a depth (the least n such that the formula is in X n ), and one can show properties by induction on the depth. Defining a function (for instance the set of free variables) is more complicated (one defines by induction a function f n whose source is X n , then takes the common extension in order to get a function on the union).

• José Grimm

Note: Bourbaki makes a difference between a "function" (possibly defined on N) and a "mapping of N into U " (in French: "fonction" and "application de N dans U "); if "into" is replaced by "onto" (in French "dans" by "sur"), then the function is assumed surjective. The criterion could be simplified if the word "mapping" were replaced by "function", in the form: there exists a unique surjective function defined on N such that f (n) = T f (n) . This formulation avoids the need to give a name to the target of f and claim its existence and uniqueness (idem for C63, where a different name has been used).

C63. Let S v and a be two terms. Then there exists a set V and a mapping f of N onto V such that f (0) = a and f (n) = S f (n -1) for each integer ≥ 1. Moreover, the set V and the mapping f are uniquely determined by these conditions.

Usually, the second condition is written f (n + 1) = S f (n) for all n, and the existence part is what really matters. So we prove:

Lemma induction_defined_pr s a (f := induction_defined s a): [/\ source f = Nat, surjection f, Vf f \0c = a & forall n, natp n -> Vf f (csucc n) = s (Vf f n)].
One can also impose: f (0) = a and f (n+1) = s(n, f (n)). The Bourbaki approach (using only induction_defined) is very complicated, but the result follows directly from C60. In the lemmas that follow, we consider a lambda term rather that an mapping.

Lemma induction_term0 s a: induction_term s a \0c = a. Lemma induction_terms s a n: natp n -> induction_term s a (csucc n) = s n (induction_term s a n).

Arithmetic properties

Consider a family of sets X, i.e., a functional graph; it is characterized by its domain I and its evaluation map i → X i . Note that every set X can be considered as a family by taking as domain the set of all i such that for at least one j we have (i, j) ∈ X and as evaluation X i some j satisfying this condition (an example is csum_Cn below). The disjoint union S of the family is the set of all (x, i), where i ∈ I and x ∈ X i . The cardinal of S are called the cardinal sum of the family and denoted 'csum X'; there is a variant csumb that takes two arguments: the domain and the evaluation function; what is traditionally written i∈I X i corresponds to 'csumb I (fun i => Vg X i)' or 'csumb I (Vg X)'.

The quantity i∈I X i remains unchanged if each X i is replaced by an equipotent set (for instance its cardinal). Commutativity of addition means that if f is any bijection J → I, then i∈I a i = j∈J a f (j) . Associativity of addition means: if (I k ) k∈K is a functional graph formed of mutually disjoint sets whose union is I and if s k = i∈I k a i , then i∈I a i = k∈K s k . It is important (for the ease of proofs) to notice that we do not require a be a functional graph, nor a i to be a cardinal.

Theorem csum_An f g: partition_w_fam g (domain f) -> • 21 csum f = csumb (domain g) (fun l => csumb (Vg g l) (Vg f)). Theorem csum_Cn X f: target f = domain X -> bijection f -> csum X = csum (X \cf (graph f)).
Given two sets a, b, one can consider the family indexed by a set of two elements; the sum of this family is denoted a + b. Associativity and commutativity take a more familiar form: The cartesian product i∈I X i is the set of all functional graphs f defined on I such that f (i) ∈ X i whenever i ∈ I. Its cardinal is called the cardinal product of the family and is denoted here cprod or cprodb; in order to avoid ambiguities (for instance in equation (1), the product in the definition of I is the cartesian product, the two other products are cardinal products), Bourbaki uses a big P in Chapter 3, section 3, the usual notation later on. As in the case of a sum, the cardinal product remains unchanged if a factor X i is replaced by an equipotent set, the factor need not be a cardinal. The product is associative, commutative; distributivity over sums is expressed as follows: let ((a j,i ) i∈Jj ) j∈L be a double family, then

j∈L i∈Jj a j,i = f ∈I j∈L a j,f (j)
where I = j∈L J j .

(

As in the case of a sum, formulas are simpler when the family is reduced to two elements: We define a b as the cardinal of the set of functional graphs (or functions) b → a. This is equal to the product of a family (indexed by b) of cardinals all equal to a, in the same manner as a • b is the sum of this family (moreover b is the sum of the family of cardinals all equal to one). A product is zero if and only if one factor is zero11 . Lemma csum0r a: cardinalp a -> a +c \0c = a. Lemma cprod1r a: cardinalp a -> a *c \1c = a. Lemma cprod2_nz a b: a <> \0c -> b <> \0c -> a *c b <> \0c. Lemma cprod0r a: a *c \0c = \0c. Lemma cpow1x a: \1c ^c a = \1c.

Theorem

• José Grimm

The operations defined above are compatible with comparison. First note that if f : A → B is injective, then card(A) ≤ card(B) (if card(B) ≤ card(A), we have an injection B → A, and by the Cantor-Bernstein theorem A and B are equipotent). In particular, if A is a subset of B, we have card(A) ≤ card(B). To proceed further, we define a -b to be the cardinal of the complement c of b in a. If b ≤ a (so that a and b are cardinals, b ⊂ a), then {b, c} forms a partition of a; so that a = b + (a -b). It follows that b ≤ a if and only if there is c such that a = b + c. Let's note that card(P(X)) = 2 X (for each A ⊂ X, we consider the characteristic function φ A whose value is one in A and zero on the complement). There is no surjection f : X → P(X) (consider y such that f (y) is the set of all z such that f (z) ∈ z). One deduces a < 2 a , so that there is no set containing all cardinals.

Theorem card_setP X: cardinal (powerset X) = \2c ^c X. Theorem cantor a: cardinalp a -> a <c (\2c ^c a). Lemma cantor_bis: ~(exists a, forall x, cardinalp x -> inc x a).

Let's consider now the set N of finite cardinals. Since x + 1 is the cardinal of x + , it follows that a cardinal x is finite if and only if x = x + 1. In this case x + 1 = x + . The relations a + (b + 1) = (a + b) + 1, a • (b + 1) = a • b + a and a b+1 = a b • a show, by induction on b, that N is stable by addition, multiplication and exponentiation. Since a -b ≤ a, it follows that a -b is an integer whenever a is an integer. One can define (by induction on nat) a mapping nat → N; it is injective (by induction on nat) and surjective (by induction on N). Obviously, this function is compatible with the operations and ordering. As a consequence, every property valid on nat, and proved in the standard library of Coq, has a analogue on N with a trivial proof. For instance, if a, b, c are integers, a < b implies a + c < b + c. Our proof is the following: since a < b there is a non-zero integer d such that b = a + d and d has the form e + 1; now a + c < (a + c) + 1 ≤ ((a + c) + 1) + e = b + c. This property holds even when a and b are infinite (as x + c = x whenever x is infinite and c finite), but fails if c is infinite and big enough (if c is infinite and c ≥ max(a, b), then a

+ c = b + c = c).
If A and B are two finite sets with the same cardinal, then a function f : A → B is bijective if and only if it is injective (or surjective). The principle of induction on N can be extended as follows: let P be a property, true for the empty set, such that P (A) implies P (A ∪ {a}). Then P holds for every finite set. Assume that P (∅) is replaced by: P holds for every singleton; then P holds for every non-empty finite set. Example: let A be a totally ordered set; then every non-empty finite subset of A has a least and a greatest element. As a consequence, if A is finite, it is well-ordered.

• 23

Expansion to base b

If a and b are integers, b non-zero, there exists p such that a < bp. The least such integer is non-zero, thus of the form q + 1. Moreover, there exists r such that a = bq + r, 0 ≤ r < b. The two quantities q and r, uniquely defined by this pair of relations, are called the quotient and remainder in the Euclidean division of a by b.

Let's notice that a finite sum (or product) of integers is an integer (proof by induction on the domain). In particular, if f (k) is an integer for k < n, then k<n f (k) and k<n f (k) are integers. If S n is the sum then S n+1 = S n + f (n); one could prove by induction on n via this formula that S n is an integer. One also has S n+1 = f (0) + i<n f (i + 1). Consider for example

E nb (a) = i<n a i b i where (a i ) i<n is a sequence of integers and b ≥ 2 [If b = 0, the sum is a 0 for n > 0, if b = 1, the sum is a i , we shall omit the index b in what follows].
We have

E n+1 (a) = E n (a) + a n b n = a 0 + bE n (a ) ( 2
)
where a is the sequence i → a i+1 . In what follows, we shall assume implicitly a i < b for each i. It is easy to deduce from these considerations that, for every integer A, if A < b n , there is a unique sequence (a i ) i<n such that A = E n (a); it is called the expansion to base b with n digits. If n < m and A has two expansions with n and m digits, then a i = 0 for n ≤ i for the second expansion; thus, there is a unique expansion (called normal) with n = 0 or a n-1 = 0. Let C be another number and c its expansion with m digits. We have now the following criterion for A < C: Either there is k such that n ≤ k < m and c k is non-zero, or there are two indices k, p such k < p ≤ min(n, m) and a k < c k , a i = c i for k < i < p; moreover a i and c i are zero for i ≥ p. In particular, if the expansions are normal, then n < m implies A < C.

Note: assume n = m; the criterion simplifies to: there is an index k, such k < n, a k < c k , a i = c i for k < i < n. Bourbaki states this in Proposition 8 of §5.7 as: "let E k be the lexicographic product of the family (J h ) 0≤h≤k-1 of intervals all identical with [0, b -1], then f k is an isomorphism of the ordered set E k onto the interval [0, b k -1]." Here, all intervals (including [0, h -1]) are ordered by ≤; since the leading digits have to be compared first, this leading digit corresponds to h = 0; for this reason Bourbaki uses

f k (r) = k-1 h=0 r h b k-h-1 .
The condition for the expansion to be normal simplifies to r 0 = 0. [Note that k has to be non-zero, so that zero is the only integer that has no expansion in the Bourbaki sense; our approach is a bit simpler and has no exception.] [Note also: in order to prove that N and N × N are equipotent, Bourbaki uses the fact that every integer can uniquely be written as an infinite sum h a h b h , where a h = 0 for h ≥ k.] Let C(A) be the sum i<n a i where A = E n (a). Assume that A is not a digit (so that A > b and there is i such that 0 < i < n and a i = 0). One gets C(A) < A. Let C k (A) be the k-th iteration of C. This sequence is eventually constant, let's denote the limit value by C (A). A special case is expansion to base two. Here a i < b says a i = 0 or a i = 1. The number of digits in a normal expansion of n is called the base two logarithm of n. If n is non-zero, this is a non-zero integer such that 2 ln(n)-1 ≤ n < 2 ln(n) . Moreover a ln(n)-1 = 1. We define the base-two reverse r(n) of n to be E l (a ), where the sequence a is the base two expansion of n, l its length, and a i = a l-1-i . The relation a l-1 = 1 says a 0 = 1, so that r(n) is odd (unless n = 0). We have r(r(n)) = n when n is odd. This can be restated as: r(r(r(n))) = r(n), whatever n. natp n -> r (r (r n)) = r n.

Combinatorial Analysis

A key relation is (shepherd's principle in France): if f : E → F is any mapping such that the inverse image of any singleton has the same cardinal c, then the cardinal of E is c times the cardinal of F . [Note: For some reason, Bourbaki assumes f surjective; if x is in F but not in the image, the cardinal of the inverse image of {x} is zero, thus c = 0, thus no element is in the image, thus E is empty and the result is still true].

Theory of Sets / From natural numbers to real numbers • 25 A first consequence is: the number A nm of injections of a set with m elements into a set of n elements satisfies A n,m+1 = A n,m • (n -m) thus A nm = n!/(n -m)!, where n! is i<n (i + 1). Taking n = m says that n! is the number of permutations of a set with n elements. [Proof: if E has m + 1 elements, a is one of those, E = E -{a}, a function f : E → F is characterized by its value at a, and the restriction f to E . In order for the function f to be injective, we need f to be injective and the value f (a) not in the range of the restriction. The set in which f (a) can be chosen depends on f , but not its cardinal, which is n -m].

Let (p i ) i<h be a finite sequence of integers, n = p i , E a set with n elements; the number of ways to write E as the union of disjoint sets E i with cardinal p i is n!/( i<h p i !). Proof. Let I = [0, n[, and consider a partition I k of I formed of sets with p i elements (I k contains the p k smallest elements not in I j for j < k). Let f : I → E be a bijection, g a permutation of I, E k the image by f • g of I k , G(g) the sequence of these E k . The family G(g) is a solution, every solution has this form; the relation G(g) = G(g ) is equivalent to say that g -1 • g , restricted to each I k , is a permutation (size of the proof: 450 lines of script). Using the same techniques, one deduces the following (250 lines of script). Application: the number of subsets with p elements in a set with n elements is n!/(p!(n -p)!) = n p . One deduces that, if p ≤ n, then p!(n -p)! divides n!, and the quotient could be used to define the binomial coefficient. We give here an inductive definition and a proof of correctness, as an example of how to proceed when the induction principle (induction_defined or induction_term) cannot Our library contains many other formulas, using similar or different proof techniques. For instance (3) holds in any ring (the only condition being that a i a j = a j a i ) and can be shown by induction 12 . The number of strictly increasing functions E → F (where both sets are finite and totally ordered, of cardinal n and m) is m n (the function is uniquely determined by its image, a subset of n elements of F ). One deduces the number of increasing functions: we may reduce the case to E = I n and F = I m (the ordered set of integers < n or < m); if g(i) = f (i) + i, then f is increasing if and only if g is strictly increasing, and the range of g is I n+m-1 . Let h(i) = f (i + 1) -f (i); then f (i) is the sum of the h(j). So counting the number of (strictly) increasing functions is the same as counting the number of functions h such that h i = m (or h i ≤ m). This is the number of monomials with n variables of total degree m or ≤ m; these two numbers are related and can be computed by induction on n.

p1+p2+•••+p k =n n! p 1 ! • • • p k ! a p1 1 ...a p k k = (a 1 + a 2 + • • • + a k ) n . ( 3
Many of the formulas can be expressed and proved using the structure of finite sets provided by the ssreflect library (thus do not require any axiom). For instance the file binomial.v provides three lemmas that give the number of injections, the number of increasing functions (in fact, sorted lists) and the number of functions such that h i ≤ m. One of our objectives is to solve in Coq all exercices of Bourbaki, and if possible, directly in ssreflect. This is sometimes a challenge: for instance, let S n,p be the number of surjections I n → I p . There is an explicit formula, but it requires negative numbers. On the other hand, there is an implicit formula relating S n,i , the binomial • 27 coefficients and the number of functions I n → I p (every function is a surjection on its image). There is also a simple recurrence relation, S n,p = p(S n-1,p + S n-1,p-1 ) (proved in Gaia), and if P n,p is the number of partitions of I n into p parts, then S n,p = p!P n,p . The quantity P is known as Stirling numbers of the second kind; we have defined it in ssreflect, and shown that it is the number of partitions, but we have not yet managed to compute the number of surjections (work in progress).

THE SET OF RATIONAL INTEGERS Z

We define Z as the disjoint union of N * and N. An element of this union is a pair (a, b) where either b = C0 and a ∈ N * , or b = C1 and a ∈ N. We denote by φ + (a) the pair (a, C1), and by φ -(a) the pair (a, C0) when a = 0, extended by φ -(0) = φ + (0). The image of φ + will be denoted by Z + , the image of φ -will be denoted by Z -(these two sets contain zero). Removing zero yields Z * + and Z * -.

Definition Nats:= Nat -s1 \0c. Definition BZ := canonical_du2 Nats Nat. Definition BZ_of_nat x := J x C1. Definition BZm_of_nat x := Yo (x = \0c) \0z (J x C0). Notation BZ_val := P (only parsing). Notation BZ_sg := Q (only parsing). Definition intp x := inc x BZ.

We show here simple functions: absolute value, sign and opposite. Note that if x is the pair (a, b), then the absolute value is a (considered in Z) and the sign is b (converted into +1 or -1; except that the sign of zero is zero). Consider the following three functions, with range N 2 , Z and N 2 respectively:

f : x ∈ Z → (0, |x|) if x ∈ Z + (|x|, 0) otherwise, g : (x, y) ∈ N 2 → φ + (y -x) if x ≤ y φ -(x -y) otherwise, h : ((x, y), (x , y )) ∈ N 2 × N 2 → (x + x , y + y ).
Note that g is surjective as g(f (x)) = x, but not injective; however g(x, y) = g(x , y ) is equivalent to x + y = x + y. The operation x + z y = g(h(f (x), f (y))) is clearly associative, and makes Z the group of differences of N.

Definition Bzsum x y := let f := fun x => Yo (inc x BZp) (J \0c (BZ_val x)) (J (BZ_val x) \0c) in let g := fun x => Yo ((P x) <=c (Q x))

• 29

(order_isomorphism f BZ_ordering BZ_ordering) <-> (exists2 u, intp u & f = Lf (fun z => z +z u) BZ BZ).
We show here that every non-empty, totally ordered, complete and connected set is order isomorphic to Z. Let's say that x and y are consecutive when x < y, and there is no z such that x < z < y. In this case, we say that y is a successor of x and that x is a predecessor of y. We say that the set is complete when each x has a successor and a predecessor. In a totally ordered set, these quantities are unique. We say that a set is connected when no trivial subset is stable by neighborhood (successor and predecessor).

Primo, it is obvious that z + 1 and z -1 are the successor and predecessor of z in Z. Secondo, if P is a property, a ∈ Z, in order for P to hold on Z, it suffices that P (a) holds, that P (x) implies P (x + 1) for x ≥ a, and that P (x) implies P (x -1) for x ≤ a [Note: this is a generalization of the induction principle of ssreflect, which holds when a = 0]. Thus, every subset of Z stable by neighborhood that contains a contains all elements, and Z is connected. Tertio, if E is an ordered set, if f : Z → E is a mapping such that f (z) < f (z + 1), then f is strictly increasing. Assume that E is totally ordered and complete, and a ∈ E. Define, by induction on N, two sequences x and y, such that x 0 = y 0 = a, x n+1 is the successor of x n and y n+1 is the predecessor of y n . We may consider this as a function f : Z → E, that satisfies: for every z, f (z) and f (z + 1) are consecutive. Thus, f is an order isomorphism on its image, which is clearly stable by neighborhood. So, if E is connected, f is surjective.

• José Grimm

The Stern Brocot sequence

We know that Q is countable, but is there an explicit bijection N → Q? A positive answer was given by Moritz Stern in 1858 [START_REF] Stern | Ueber eine zahlentheorische Funktion[END_REF] and independently by Achille Brocot in 1861. If s n denotes the sequence (listed under number A002487 in the On-line Encyclopedia of Integer Sequences) formed of all numbers that appear in the basic Stern diatomic sequence (see [START_REF] Grimm | Fibonacci numbers and the Stern-Brocot tree in Coq[END_REF] for details), then the following conditions hold: s k and s k+1 are coprime, and every rational number is uniquely a quotient s k /s k+1 . The Stern-Brocot tree is a tree representation of the sequence, it also provides an algorithm for the inverse function Q → N; it can be used for an implementation of Q in Coq, see [START_REF] Niqui | Exact arithmetic on the Stern-Brocot tree[END_REF][START_REF] Niqui | Qarith: Coq formalisation of lazy rational arithmetic[END_REF].

The sequence was rediscovered in 1976 by Dijkstra, under the name "fusc" [START_REF] Edsger | An exercise for Dr[END_REF][START_REF] Edsger | More about the function "fusc[END_REF], with the following definition:

s 1 = 1, s 2n = s n , s 2n+1 = s n + s n+1 .
(4)

In the first paper Dijkstra writes: if f 1 = fusc(n 1 ) and f 2 = fusc(n 2 ), "if there exists an N such that n 1 + n 2 = 2 N , then f 1 and f 2 are relatively prime" and "if f 1 and f 2 are relatively prime, then there exists an n 1 , an n 2 , and an N such that n 1 + n 2 = 2 N . In the above recursive definition, this is no longer obvious, at least not to me; hence its name."

There is an implementation in pure ssreflect of the definitions and theorems given in this section, see [START_REF] Grimm | Fibonacci numbers and the Stern-Brocot tree in Coq[END_REF]; we show the definition and the two claims of Dijkstra. The second paper of Dijkstra starts with two properties.

s(n) = s(i(n)), s(n) = s(r(n)).

(5)

Here r(n) is the base two reverse of n and i(n) the number obtained by inverting in the binary representation of n all inner digits (inner digits are those that follow the initial 1 and are before the last 1; if n is a power of two there is no inner digit and i(n) = n). For instance 19 = 10011 2 , r(19) = 11001 2 = 25 and i(19) = 11101 2 = 29. If n is odd then i(r(n)) = r(i(n)). Moreover, unless n is a power of two, then n + i(n) = 3p where p is the greatest power of two such that p ≤ n (example: 19 + i(19) = 3 • 2 4 ). From r(2k + 1) = 2 log 2 (k) + r(k), it follows the magic formula r(n -1) + i(r(n)) = 2 log 2 n (n > 1, n odd). (6)

• 49

CONCLUSION Notes on the Implementation

The work presented here corresponds to 8 files (sset7, sset8, sset9, sset10, ssetz, ssetq1, ssetq2, ssetr), 360 definitions, 71 notations, 2700 lemmas and 34,000 lines of code (16,000 lines for N and 18,000 for the other data structures). It implements the basic properties of N, Z and Q, presents the arithmetic properties of R and some of its analytic properties, with a focus on the properties of order. It represents 20% of the Gaia library. The code is available on the Web, under http://wwwsop.inria.fr/marelle/gaia.

In [START_REF] Grimm | Implementation of Bourbaki's Elements of Mathematics in Coq, part one theory of sets[END_REF] we wrote "Coq was much slower on Q than on Z"; in particular the two tactics 'auto with fprops' and 'autorewrite with aw' were sometimes very slow. The first remedy was to use a second data base and add tactics 'auto with qprops' and 'autorewrite with qw'. We then removed the most costly calls to these tactics, and in the current version, we removed the second database, and the implementation of Z, Q and R adds no hint to the first database. This is inspired from the ssreflect library, which very rarely uses auto.

We also noticed a slowdown when replacing one definition of addition on Z by a variant; the exact reason is unclear: is it due to a limited number of lemmas that became much slower, or a great number of lemmas that became just a bit slower? For instance, in the proof of (a + b) 2 = 4ab + (a -b) 2 on Q, which is rather straightforward, replacing trivial by reflexivity reduces compilation time from 2.5 seconds to 0.5 second. On the other hand, a previous version of Gaia used the 'Module Type' trick of ssreflect in order to make the cardinal function completely opaque. This is no more needed.

Comparison with the Coq library

As shown in the text, defining a function f : nat → N, and showing that it is bijective is quite easy; this obviously preserves the structures (addition, multiplication, comparison). Using the axiom of choice (for the non-empty type nat), one can introduce the inverse of this function (but we never needed it in our development). Similarly, we have defined a bijection g : int → Z, and proved that it respects the structures; in particular, it respects divisibility and gcd, so that defining h : rat → Q should be straightforward as well (work in progress).

The case of real numbers is more challenging: if x : R is a real number (according to the standard library of Coq), it is the limit of a sequence of rational numbers x i . One can cast this into a Cauchy sequence in Q, and take its limit x ∈ R; one has to show that this number is independent of the chosen sequence. Conversely, given x ∈ R, associated to a Dedekind cut (A, B), it should be possible to consider A as a "bounded subset" of R and use the completeness axiom to get a real x. One has to prove that this is the inverse function of the preceding one, and that it respects the operations. [This is a possible extension of our library].

All the code described in section 4.2 has been implemented both in Gaia and directly in ssreflect, using the int and rat type, see [START_REF] Grimm | Fibonacci numbers and the Stern-Brocot tree in Coq[END_REF]. Some comments:

• 51 although Kuratowski introduced its definition in 1921]. Bourbaki introduces his Axiom of Infinity (hence the set of natural integers) in section 6, page 183, while "integer" is defined on page 166 and the principle of induction (criterion C61) on page 168. As the Axiom of Infinity is implicit in Gaia, we introduced N much earlier. There is no other fundamental difference between the Bourbaki integers and those of Gaia.

Implementing Z as explained by Bourbaki is more challenging. It imposes to define the notion of: monoid, group, homomorphism, group of differences, etc (20 pages of the Book of Algebra). This is technically possible, and corresponds to a part of the ssralg.v file of ssreflect. To go further (establish some properties of Z and define Q), one can either implement the whole Chapter 1 of the Book of Algebra (120 pages) or select some specific topics. In any case, it requires to implement the equivalent of ssralg.v, including canonical structures, bigop.v, etc. Now, some properties of Q (for instance that it is an ordered field) is defined in Chapter 6 (still more things to implement, for instance, the equivalent of ssrnum.v). The fact that every rational number can unique be written as a/b where a and b are coprime is explained in another Chapter. Implementing the whole Book of Algebra (or just the part needed for Q) using an untyped theory like Bourbaki makes little sense, as it can never be as simple or efficient as the ssreflect library.

The case of real numbers is a bit different. Bourbaki introduces R as a topological field (obtained by completion of Q) and studies it in the Book of Topology as a topological object; many other properties are found in the Book "Functions of a Real Variable". There is so much material in these books that implementing them would take forever; it is much wiser to start with a simple definition (for instance, that of the standard library of Coq), and extend it, little by little, with independent modules.

  Inductive nat : Set := O : nat | S : nat -> nat.

  Inductive le (n:nat) : nat -> Prop := • 7 | le_n : n <= n | le_S : forall m:nat, n <= m -> n <= S m end where "n <= m" := (le n m) : nat_scope. Fixpoint max n m : nat := match n, m with | O, _ => m | S n', O => n | S n', S m' => S (max n' m') end.

  Lemma muln_eq1 m n : (m * n == 1) = (m == 1) && (n == 1). Definition leq m n := m -n == 0. Definition maxn m n := if m < n then n else m.

  Inductive positive : Set := | xI : positive -> positive | xO : positive -> positive | xH : positive. Inductive N : Set := | N0 : N | Npos : positive -> N. Inductive Z : Set := | Z0 : Z | Zpos : positive -> Z | Zneg : positive -> Z. Definition opp x := match x with | 0 => 0| pos x => neg x | neg x => pos x end.

  CoInductive int : Set := Posz : nat -> int | Negz : nat -> int. Definition oppz m := nosimpl match m with | Posz n => if n is (n'.+1)%N then Negz n' else Posz 0 | Negz n => Posz (n.+1)%N end.

  Instance Qplus_comp : Proper (Qeq==>Qeq==>Qeq) Qplus. Instance Qle_comp : Proper (Qeq==>Qeq==>iff) Qle. Theorem Qplus_assoc : forall x y z, x+(y+z)==(x+y)+z.

  Theorem R_complete :forall Un:nat -> R, Cauchy_crit Un -> { l:R | Un_cv Un l } . Lemma Machin_4_5_239 : PI/4 = 4 * atan (/5) -atan(/239).

  Lemma Nat_induction (r:property):(r \0c) -> (forall n, natp n -> r n -> r (csucc n)) -> (forall n, natp n -> r n). Proof. move=> r0 ri n nN. case: (p_or_not_p (r n)) => // nrn. have pa: (exists2 x, natp x & ~r x) by exists n. case:(wleast_int_prop pa) => // [] [x [xN nsr /excluded_middle rx]]. by case: nsr; apply: ri. Qed.

  denotes the mapping of [0, n[ onto f ([0, n[) which agrees with f on [0, n[. Moreover the set U and the mapping f are uniquely determined by this condition.

  Lemma csumC a b: a +c b = b +c a. Lemma csumA a b c: a +c (b +c c) = (a +c b) +c c.

  cprodDn f: cprodb (domain f) (fun l => csum (Vg f l)) = csumb (productf (domain f) (fun l => (domain (Vg f l)))) (fun g => (cprodb (domain f) (fun l => Vg (Vg f l) (Vg g l)))). Lemma cprodDr a b c: (b +c c) *c a = (b *c a) +c (c *c a). Lemma cprodC a b: a *c b = b *c a. Lemma csumA a b c: a +c (b +c c) = (a +c b) +c c.

Fixpoint

  nat_to_B (n:nat) := if n is m.+1 then csucc (nat_to_B m) else \0c. Lemma nat_to_B_injective: injective nat_to_B. Lemma nat_to_B_surjective x: natp x -> exists n, x = nat_to_B n.

  We deduce: a n and E n (a) are the quotient and remainder in the division of E n+1 (a) by b n ; E n (a ) and a 0 are the quotient and remainder of the division of E n+1 (a) by b.

  Lemma expansion_prop15 f g b n:• José Grimm expansion f b n -> expansion g b n -> ( (expansion_value f b) <c (expansion_value g b) <-> exists k, [/\ k <c n, (Vg f k) <c (Vg g k) & (forall i, k <c i -> i <c n -> Vg f i = Vg g i)]).

  The two quantities A and C(A) are equal modulo b -1 (since b n is one modulo b -1). Thus A and C (A) are the same modulo b -1. One can be more precise: either A = 0 case where C (A) = A, or A = 0, case where C (A) is between 1 and b -1; if y is the remainder in the division of A by b -1, then either y = 0 (division is exact) and C (A) = b -1, or C (A) = y. We show here what happens when b = 10. Lemma divisibiliy_by_nine f k: expansion_ten f k -> let g:= (Lg (domain f) (fun i=> (Vg f i) *c (\10c ^c i))) in eqmod \9c (csum g) (csum f). Lemma eqmod_contraction_rep9 a (x := contraction_rep \10c a) (y := a %%c \9c) : natp a -> [/\ eqmod \9c a x, (a = \0c -> x = \0c) & (a <> \0c -> (y = \0c -> x = \9c) /\ (y <> \0c -> x = y))].

  Definition base_two_reverse n := let F := the_expansion \2c n in let p := cardinal (domain F) in expansion_value (Lg p (fun z => (Vg F (p -c (csucc z))))) \2c. Lemma base2r_oddK_bis n (r := base_two_reverse) :

  Definition partition_with_pi_elements p E f := [/\ domain f = domain p, (forall i, inc i (domain p) -> cardinal (Vg f i) = Vg p i) & partition_w_fam f E]. Definition partitions_pi p E := Zo (gfunctions (domain p) (powerset E)) (partition_with_pi_elements p E). Theorem number_of_partitions_bis p E: finite_int_fam p -> csum p = cardinal E -> cardinal (partitions_pi p E) = (factorial (cardinal E)) %/c (cprodb (domain p) (fun z => factorial (Vg p z))).

)

  Lemma sum_of_gen_binom0 E n a: natp n -> cardinal E = n -> finite_int_fam a -> (csum a) ^c n = csumb (graphs_sum_eq (domain a) n) (fun p => (cardinal (partitions_pi p E)) *c (cprodb (domain a) (fun i=> ((Vg a i) ^c (Vg p i))))).

•

  José Grimm be used directly. So, we define a functional graph f n with domain N such that f n+1 (m) = f n (m) + f n (m -1), and apply it to m. The anonymous function has an unused parameter (the value of n), the second parameter being f n . The expression 'variant a b c d', short for 'Yo (d = a) b c', means: if d = a then b else c, it is used to say that f 0 (0) = 1 and f n+1 (0) = 0. Definition binom n m := Vg (induction_term (fun _ T: Set => Lg Nat (fun z => variant \0c \1c (Vg T z +c Vg T (cpred z)) z)) (Lg Nat (variant \0c \1c \0c)) n) m. Lemma binom_alt_pr n m: natp n -> natp m -> (binom n m) *c (factorial m) *c (factorial (n -c m)) = Yo (m <=c n) (factorial n) \0c.

  Lemma card_inj_ffuns D T : #|[set f : {ffun D -> T} | injectiveb f]| = #|T| ^_ #|D|. Lemma card_sorted_tuples m n : #|[set t : m.-tuple 'I_n.+1 | sorted leq (map val t)]| = 'C(m + n, m). Lemma card_partial_ord_partitions m n : #|[set t : m.-tuple 'I_n.+1 | \sum_(i <-t) i <= n]| = 'C(m + n, m).

Definition

  BZabs x := BZ_of_nat (BZ_val x). Definition BZsign x:= Yo (BZ_val x = \0c) \0z (Yo (BZ_sg x = C1) \1z \1mz). Definition BZopp x:= Yo (BZ_sg x = C0) (BZ_of_nat (BZ_val x)) (BZm_of_nat (BZ_val x)).

  Definition fusc n := let fix loop n k := if k is k'.+1 then if n<=1 then n else if (odd n) then (loop n./2 k') + loop (uphalf n) k' else loop n./2 k' else 0 in loop n n. Lemma fusc_fusc3 n m p: n + m = 2^p -> coprime (fusc n) (fusc m). Lemma fusc_fusc2 a b: coprime a b -> exists n m p, [/\ n + m = 2^p, a = fusc n & b = fusc m].

In short, MathComp; for details, see the web site http://math-comp.github.io/math-comp/ Journal of Formal Reasoning Vol. ?, No. ?, Month Year, Pages 1-52.

by the Burali-Forti paradox, there is no type for all the ordinals

For instance

4/6 and 6/9 are equivalent for the equivalence that makes Q a quotient; in lowest terms they become equal to 2/3; in a theory of sets, the classes are equal and can be identified with their canonical representative 2/3 Journal of Formal Reasoning Vol. ?, No. ?, Month Year.

Journal of Formal Reasoning Vol. ?, No. ?, Month Year.

This is a commutative group, hence canonically isomorphic to a Z-module Journal of Formal Reasoning Vol. ?, No. ?, Month Year.

Technically, MathComp is the name of the library, ssreflect the tactic language and Small Scale Reflection the principle behind the language and the library Journal of Formal Reasoning Vol. ?, No. ?, Month Year.

In the mathcomp/real_closed directory on GitHub, accessible via the MathComp web page Journal of Formal Reasoning Vol. ?, No. ?, Month Year.

For the formal definition of function and graph, see below; given a functional graph G and a superset X of its range, there is a unique function f with graph G and target X; in the example X is chosen as the domain of G, so that f has the same source and target; one can choose X as the range so that f becomes surjective.

Bourbaki considers the notion of "assembly" which is a character string with links. Binding a variable consists in replacing it by a specific symbol and adding a link. There is no x in τx(P ). This avoids the need for α-conversion, but an assembly cannot be represented in a computer.Journal of Formal Reasoning Vol. ?, No. ?, Month Year.

It is traditionally denoted ]-∞, x[; if E has a least element e, then ]←, x[ = [e, x[; similarly [x, →[ corresponds to [x, +∞[ Journal of Formal Reasoning Vol. ?, No. ?, Month Year.

The expressions a + 0 and a * 1, defined whatever a are requal to card(a), hence to a when a is a cardinal Journal of Formal Reasoning Vol. ?, No. ?, Month Year.

ACKNOWLEDGMENT

We wish to thank the anonymous referee for his valuable suggestions.

• José Grimm (BZ_of_nat((Q x) -c (P x))) (BZm_of_nat ((P x) -c (Q x))) in let h := fun x y => J ( (P x) +c (P y)) ( (Q x) +c (Q y)) in g (h (f x) (f y)).

Let x and y be two numbers, with absolute value a and b; then x + y is g(z), where z is one of (0, a + b), (a, b), (b, a) or (a + b, 0), depending on the signs of the numbers. In the first and last cases, the sum is φ + (a + b) and φ -(a + b). This leads to the following equivalent (longer, but more natural) definition: Addition on Z is compatible with addition on N and makes it a commutative group; the successor and predecessor functions (that map z to z + 1 or z -1) are compatible with those of N.

Lemma BZsum_cN x y: natp x -> natp y -> BZ_of_nat x +z BZ_of_nat y = BZ_of_nat (x +c y). Lemma BZsucc_N x: natp x -> BZsucc (BZ_of_nat x) = BZ_of_nat (csucc x). Lemma BZprec_N x: inc x Nats -> BZpred (BZ_of_nat x) = BZ_of_nat (cpred x).

Consider the ordinal sum (see section 4.1 for the definition) of the opposite of the order of N * and the natural order of N. This is a total order on Z, as each component is totally ordered. The order is compatible with addition (so that Z is an ordered group). Note that φ + is strictly increasing and z → -z is strictly decreasing (it is an order isomorphism of Z onto the opposite order of Z). Since N is well-ordered, there is a unique order isomorphism N → N; here we have: for any x ∈ Z, there is a unique order isomorphism f : Z → Z such that f (0) = x; it is defined by f (z) = z + x; and all order isomorphisms are of this form. Definition consecutive r x y := glt r x y /\ forall z, inc z (substrate r) -> ~(glt r x z /\ glt r z y). Definition or_succ r x := select (fun z => consecutive r x z) (substrate r). Definition or_pred r x := select (fun z => consecutive r z x) (substrate r). Definition or_complete r := forall x, inc x (substrate r) -> (exists y, consecutive r x y) /\ (exists y, consecutive r y x). Definition or_stable r E:= forall x, inc x E -> inc (or_succ r x) E /\ inc (or_pred r x) E. Definition or_connected r:= forall E, sub E (substrate r) -> or_stable r E -> E = emptyset \/ E = substrate r. Definition or_likeZ r := [/\ total_order r, or_complete r & or_connected r].

Lemma BZ_order_props: or_likeZ BZ_ordering. Lemma BZ_order_props_bis r: nonempty (substrate r) -> or_likeZ r -> r \Is BZ_ordering.

Defining multiplication, and proving the usual properties is easy. Note that the only invertible elements are 1 and -1.

Definition BZprod x y := let aux := BZ_of_nat ((BZ_val x) *c (BZ_val y)) in (Yo (BZ_sg x = BZ_sg y) aux (BZopp aux)). Lemma BZprod_1_inversion_l x y : intp x -> intp y -> x *z y = \1z -> (x = y /\ (x = \1z \/ x = \1mz)).

• José Grimm

If a and b are in Z, b = 0, there is a unique solution in Z of a = bq +r, 0 ≤ r < |b|. We give here the definition and characteristic property. ]. Lemma BZdvd_unique1 a b q r: intp a -> intp b -> intp q -> intp r -> b <> \0z -> BZdivision_prop a b q r -> (q = a %/z b /\ r = a %%z b).

Denote by I(a, b) the set of all elements of the form au + bv, where u and v are in Z. This is an ideal: it is stable by addition, and by multiplication by an element of Z. In particular, if x ∈ I, then -x ∈ I. As a consequence, if I contains a non-zero element, it contains a strictly positive element. The set of strictly positive elements of I can be considered as a subset of N, thus has a least element, say c. Let's say that a divides b if for some q we have b = aq. This defines an order on Z * + , and makes it a distributive lattice each pair x, y has a supremum and an infimum (here gcd and lcm), and there are some distributivity properties, for instance gcd(a, lcm(b, c)) = lcm(gcd(a, b), gcd(a, c)). (Exercice 1.16 of Bourbaki [START_REF] Bourbaki | Elements of Mathematics, Theory of Sets[END_REF] lists other properties, in particular, the previous relation remains true if gcd and lcm are exchanged).

Definition BZdvdordering := graph_on BZdivides BZps.

Lemma BZdvd_lattice_aux x y: inc x BZps -> inc y BZps -> (least_upper_bound BZdvdordering (doubleton x y) (BZlcm x y) /\ (greatest_lower_bound BZdvdordering (doubleton x y) (BZgcd x y))). Lemma BZdvd_latticeD: distributive_lattice1 BZdvdordering.

We give here an alternate characterization of the gcd as the greatest common divisor; this works when a and b are possibly negative (in a general ring, the gcd is defined modulo an invertible element). We say that a and b are coprime and write a ⊥ b if their gcd is one; this is obviously equivalent to: there exists u and v such that the Bezout relation au+bv = 1 holds. If g is the gcd of a and b, then a/g and b/g are coprime. We shall need the important property: if a and b are coprime, then gcd(a, bc) = gcd(a, c). The Bezout relation is not unique: for every q, u = u + qb, v = v -qa yields another solution. Assume a = 0, and take for q the quotient of v by a, it follows: there is a unique solution to au + bv = 1 with 0 ≤ v < |a|. Application: gcd(F n , F m ) = F gcd(n,m) , where F n is the n-th Fibonacci number. In particular, two consecutive Fibonacci numbers are coprime. We give here a formula for

We give here an isomorphism between Z and the data structure int of ssreflect; we show for instance that gcd and coprime are the same notions in both cases. The relation "x ∈ Q, y ∈ Q, N (x)D(y) ≤ D(x)N (y)", denoted by x ≤ q y, is a total order on Q. Defining addition, subtraction, multiplication and proving that Q is an ordered ring is easy. Define the inverse x -1 of a non-zero rational number x as the pair (D(x), N (x)) when N (x) > 0 and (-D(x), -N (x)) otherwise; then x -1 •x = 1. For completeness, we define the inverse of zero to be zero, so that (x -1 ) -1 = x in any case. Since x has the same sign as its inverse, it follows easily that Q is an ordered field.

Journal of Formal Reasoning Vol. ?, No. ?, Month Year.

Theory of Sets / From natural numbers to real numbers • 33 Definition BQinv x := Yo (inc (Qnum x) BZps) (J (Qden x) (Qnum x)) (Yo (Qnum x = \0z) \0q (J (BZopp (Qden x)) (BZopp (Qnum x)))). Lemma BQprod_inv1 x : ratp x -> x <> \0q -> (x *q (BQinv x)) = \1q. Lemma BQinv_K x: ratp x -> BQinv (BQinv x) = x. Lemma BQinv_sign x: ratp x -> BQsign (BQinv x) = BQsign x.

4.1 The order type of Q Let η be "the ordinal type of the aggregate R of all rational numbers which are greater than 0 and smaller than 1, in their natural order of precedence" as defined by Cantor in [Can97, first article, §9].

Cantor notices that one can well-order R, the set of all p/q, where p and q are coprime and 0 < p < q, by comparing first p + q, and then p/q. In particular, he deduces that R has cardinal ℵ 0 . On the other hand, for the natural ordering, R has no least element (consider x/2) and no greatest element (consider (x + 1)/2), and R is everywhere dense, in the sense that for every x ∈ R and y ∈ R, if x < y, there is z ∈ R such that x < z < y (consider (x + y)/2). Let's say that M is η-like if M is totally ordered, infinite countable, and satisfies these three conditions. Cantor proves, in §9, that an η-like set has the same order type as R.

We shall give the proof below, under the form "M and R are order isomorphic". Let's assume that there is a way to assign to each ordered set M some quantity M (the order type, or ordinal type for Cantor); the theorem takes then the form M = η, where η = R. According to Cantor, M is the "general concept which results from M if [...]. Thus M is itself an ordered aggregate [...]". The second sentence can be restated in modern words as: M is an ordered set, order isomorphic to M ; a trivial consequence of the condition of the first sentence is that two ordered sets that are order isomorphic have the same order type.

There is no obvious definition of M . In the case of a well-ordered set, one could use von Neumann ordinals. Bourbaki uses τ Y (X Is Y ), where "Is" means order isomorphic. In the four following lemmas, we shall admit the existence of an order type and its characteristic properties.

Parameter order_type_of: Set -> Set. Axiom order_type_exists: forall x, order x -> x \Is (order_type_of x). Axiom order_type_unique: forall x y, x \Is y -> (order_type_of x = order_type_of y).

Let E and F be two ordered sets, and G the ordinal sum (this means that G is the order on the disjoint union of E and F , where each element of E comes before each element of F ). Now, G depends only on E and F and is called the sum of the two order types. Similarly, one can define the product of two order types by considering the lexicographic product of F and E (this product is non-commutative). An easy consequence of Cantor's theorem is then: η + η = η, η • η = η; there are other formulas, for instance η + 1 + η = η and: the opposite of η is η.

• José Grimm

Lemma Cantor_eta_pr4: Cantor_eta +t Cantor_eta = Cantor_eta. Lemma Cantor_eta_pr5: Cantor_eta +t \1t +t Cantor_eta = Cantor_eta. Lemma Cantor_eta_pr6: Cantor_eta *t Cantor_eta = Cantor_eta. Lemma Cantor_eta_pr7: OT_opposite Cantor_eta = Cantor_eta.

It is easy to show that Q and Q * + are η-like, thus are order isomorphic to R. We give a direct proof here. Let f (z) = z/(1 + z). This function is defined when z = -1 and is strictly increasing (on either side of the cut). It is an isomorphism

Lemma BQ_iso1: order_isomorphism (Lf (fun z => z /q (\1q +q z)) BQps BQ_int01) BQps_ordering BQ_int01_ordering. Lemma BQ_iso2: order_isomorphism (Lf (fun z => Yo (z <q \0q) (\1q /q (\1q -q z)) (z +q \1q)) BQ BQps) BQ_ordering BQps_ordering.

The isomorphisms given above are not unique: in fact, the number of order isomorphisms Q → Q is the cardinal of R, thus 2 c , where c = ℵ 0 is the cardinal of N and also of Q. First note that an isomorphism is a function, and the number of functions is c c , this is 2 c since c is an infinite cardinal. Obviously, z → az + b is an order isomorphism when a > 0.

Let f be an element of 2 c ; it can be considered as a function N → {0, 1}, so that we can define, by induction,

Obviously f → g is injective, g is strictly increasing and unbounded. There is a function h, defined on Q + , such that, on each interval [n, n + 1], h has the form z → az + b, with h(n) = g(n) and h(n + 1) = g(n + 1). Since g is strictly increasing and unbounded, so is h. Extend h by h(z) = z for z < 0. Then h is an order isomorphism, and g → h is obviously injective.

so that Q * is order-isomorphic to the ordinal sum of two copies Q). As mentioned above, the number of order isomorphisms f :

If A and B are the sets of all f (x) such that x < 0 and x > 0 respectively, then A and B are disjoint, the union is Q, every element of A is less than every element of B. The pair (A, B) will be called an irrational cut in section 5.1. Consider the two sequences a i = f (-1/(i + 1)) and b i = f (1/(i + 1)), indexed by i ∈ N. They are Theory of Sets / From natural numbers to real numbers

• 35 called adjacent because the first sequence is strictly increasing, the second sequence is strictly decreasing, a i < b j , and the infimum of b i -a i is zero. Given adjacent sequences, we can define two disjoint sets, A, the set of all x such that x < a i for some i and B, the set of all x such that b i < x for some i. If B has an infimum q, then A is the set of numbers < q while B is the set of numbers > q; otherwise A ∪ B = Q and (A, B) is an irrational cut.

We show here that each pair of adjacent sequences (with an irrational cut) yields an order isomorphism f :

We shall prove later on that for every irrational cut (A, B), there is a pair of adjacent sequences (a, b) that defines the cut. Thus, there is an order isomorphism f :

As there is at least one irrational number, there is at least one order isomorphism f : Q * → Q. In the two lemmas that follow (that should be placed at the end of section 5.1.), r and r are the orders on Q and Q * .

Lemma BQ_order_isomorphisms_spec x: irrationalp x -> exists2 f, order_isomorphism f r' r & Vfs f BQps = x. Lemma BQ_order_isomorphisms_spec2: exists f, order_isomorphism f r' r.

Let's prove Cantor's theorem. We first assume that we has two η-like ordered sets, E and F ; as the sets are infinite countable, we consider two bijections f : N → E and g : N → F . These sets are totally ordered by r1 and r2, satisfying the conditions stated above (no least element, no greatest element, no empty interval). We pretend that there is an order isomorphism ψ :

At any stage, we choose the least integer compatible with the values chosen previously; thus h(0) = 0. Let's explain on an example how to compute h(3). Since E is totally ordered, the three elements f (0), f (1) and f (2) can be arranged in increasing order. This means that there is a permutation σ of I 3 such that i → f (σ(i)) is strictly increasing, and a necessary condition for h is that i → g(h(σ(i))) is also strictly increasing. Assume for instance σ(0) = 2, σ(1) = 0 and σ(2

; the position of y = g(h(3)) relative to y 0 , y 1 and y 2 is exactly k. Whatever k, there is always at least one y satisfying this condition, since there are elements a, b, c and d such that a < y 2 < b < y 0 < c < y 2 < d. We define h(3) to be the least integer g -1 (y) such that y satisfies this condition.

The first definition given here expresses that i → f (σ(i)) is strictly increasing; the last defines s = S k (σ) by

The first definition here, write it C(k, x), says that x is at position k (given an order r, a size n and a function h that plays the role of f • σ). We first specialize it to E, and say: if r is a total order, x not in the image of h, there is a unique k such that C(k, x) holds, it will be denoted k C (s, n). For completeness k C (s, 0) = 0.

We define by induction a sequence (s n ) n of permutations of I n , satisfying the conditions stated above, via s n+1 = S k (s n ), where k = k C (s n , n). Note that s 0 and s 1 are both defined to be the identity function on I 0 and I 1 respectively.

We assume here that we know the restriction h 1 of our function to

). Let K be the set of all j such that C(k, g(j)) holds. Since h is strictly increasing, with values in the η-like set F , and since g is surjective, this set is not empty, thus has a least element (which is the intersection). Note that, if h 1 is replaced by h 2 that takes the same value, we get the same result.

• 37 Definition EPpermi_fct h n k := intersection (Zo Nat (fun j => EPperm_compat0 r2 h n k (Vf g j))).

We denote by v(h 1 ) the quantity defined above. By transfinite induction, we define a function h, such that h(n) = v(h n ) where h n is the restriction of h to I n . Since n = 0 is special, we impose h(0) = 0. It is clear (but the proof is a bit long, 140 lines) that g • h • f -1 is an order isomorphism. We prove surjectivity of h by induction as follows. Assume that every integer < n is in the range of h, and let's show that n is in the range. The assumption is that, for some m, if K is the set of all h(i) for i < m, if i < n, then i ∈ K. If n ∈ K, there is nothing to do. Otherwise, we may consider the position q of g(n) compared to the g(j), j ∈ K. There is a least k 1 such that q is the position of f (k 1 ) compared to the g(j), j < m. This is expressed by the following definition: Definition EPperm_2pos m k1 q n (s := EPperm_rec m) (f1 := fun i => Vf f (Vf s i)) (h:= fun i => Vf g (Vf EPfun_aux (Vf s i))) (P1 := fun i => EPperm_compat0 r1 f1 m q (Vf f i)) := (P1 k1 /\ (forall i, natp i -> P1 i -> k1 <=c i)) /\ EPperm_compat0 r2 h m q (Vf g n).

We pretend h(k

the result is clear. Otherwise, we insert a new element in the sequence. The new q will be unchanged if q < k, incremented by one otherwise, but k 1 is left unchanged (the proof of this fact required 100 lines of script). We cannot always be in this situation, since m < k 1 (200 more lines of scripts are required). We finally have:

Definition EP_fun := g \co (EPfun_aux) \co (inverse_fun f). Lemma EP_fun_pr: order_isomorphism EP_fun r1 r2.

The main result is then the following (the proof script of this fact, including definitions) is a bit over 1000 lines.

• 39

The first equality of (5), together with n + i(n) = 3p, gives the palindrome condition: if a ≥ p, b ≥ p and a + b = 3p, then s(a) = s(b). A consequence is: for every k > 1 there is k such that s(k) = s(k + 1) and s(k + 1) = s(k ); moreover k + k is odd.

We pretend that, for every function s satisfying (5), the claims of the first paper of Dijkstra are equivalent to the Stern properties: whatever k, s(k) ⊥ s(k + 1); if a ⊥ b there is k such that a = s(k) and b = s(k + 1). The fusc function satisfies the Stern properties, but we doubt that Dijkstra used the reasoning explained here (he qualifies the second equality of (5) as "more surprising") and we have no idea how to prove directly the claims of the first paper. The Gaia definition is by transfinite induction: s(n) = V (s n ), where s n is the restriction of s to the set of integers < n, and V some function compatible with equation (4). Our function satisfies (4) because all arguments to s n in V are less than n (in the same manner, the loop above never terminates with the "else" part, if the argument in non-zero). Note that (4) has unique solution, and setting s 0 = 0 causes no harm.

Definition fusc := Vf (transfinite_defined Nat_order (fun u => (fusc_next u (source u)))).

Let x n = s n /s n+1 , this is the solution of:

The function n → x n is a bijection N → Q + . First note that, by induction, the two quantities s n and s n+1 are coprime. Let's show (by induction) that the function is injective. Assume x n = x m . Then n and m have the same parity (since x 2k < 1 and x 2k+1 ≥ 1). Assume for instance n = 2p and m = 2q. We have s p = q and s p + s p+1 = s q + s q+1 , thus s p+1 = s q+1 , and we conclude by induction; the other case is similar. Let's show (by induction on p + q) that x = p/q is of the form x k . If x ≥ 1, then (p -q)/q = x n for some n, so that x = x 2n+1 ; if 0 < x < 1, then (q -p)/p = x n for some n, so that x = x 2n ; the case x = 0 is trivial.

Definition fusc_quo n:= BQ_of_nat (fusc n) /q BQ_of_nat (fusc (csucc n)). Lemma fusc_quo_bijection: bijection_prop (Lf fusc_quo1 Nat BQp) Nat BQp.

There is a simple relation between x n and x n+1 .

Definition rat_iterator x := BQinv (\1q +q (BQdouble (BQ_of_Z(BQfloor x))) -q x). Lemma rat_fusc n: natp n -> rat_iterator (fusc_quo n) = fusc_quo (csucc n).

We may consider the sequence (s n ) n>0 as an infinite array, by considering A ij = s 2 i +j . Thus row i is formed of values with index beween 2 i and 2 i+1 . A priori, 2 i+1 is excluded, but recall that s n = 1 when n is a power of two. Each row is a palindrome. Each column is in arithmetic progression, the common difference being a Stern number. This is expressed as A i+1,j = A i,j + s j , or s 2p+j = s p+j + s j (whenever p is a power of two). Lemma fusc_col_progression i j: natp i -> natp j -> j <=c \2c ^c i -> fusc(\2c ^c (csucc i) +c j) = fusc(\2c ^c i +c j) +c fusc j.

A remarkable relation is that the maximum of each row is a Fibonacci number (that k ≤ 2 n implies s k ≤ F n+1 is rather obvious by induction on n: write s 2m+1 = s m + s m+1 and notice that one of m, m + 1 is even). On the other hand, since two consecutive Fibonacci numbers are coprime, there is m such that s m = F n • 41 and s m+1 = F n+1 , thus s 2m+1 = F n+2 ; that 2m + 1 is on row n is less obvious. It happens that the position of the first maximum of the row (there is a second maximum by symmetry) satisfies the relation c n+2 = c n+1 + 2c n . There is an explicit solution c n = (4.2 n -(-1) n )/3. We have shown above that every integer n has a unique expansion to base 2, i.e., can be written as n = i<k a i 2 i , with a i < 2, and a k-1 is non-zero. What happens if a i < 2 is replaced by a i ≤ 2? The relation a k-1 non-zero says n ≥ 2 k-1 , thus k < n. Thus the sequence (a i ) i<k belongs to some finite set X n , whose cardinal is s n+1 . We have shown the same property in pure ssreflect; the difficulty is the following: we can only compute the cardinal of a subset X n of a finite type T . We cannot say: X n is a subset of the set of functional graphs whose domain is a subset of N with values in I 3 (the Gaia definition), nor that X n is a subset of the set of sequences of length ≤ log 2 n with values in I 3 , because this finite set is not defined in ssreflect (although defining it should not be too complicated). For this reason, we replace the condition a k-1 non-zero by: the sequence has a fixed length. So, X n is a subset of the set of sequences of length k with values in I 3 . Now X n depends on k, say becomes X n,k but as explained above, if n has two representations of length k 1 and k 2 , then the digits, starting with max(k 1 , k 2 ), are zero (a non-zero digit is at position ≤ log 2 n). As a consequence, if k ≥ log 2 n, the cardinal of X n,k becomes independent of k. The pure ssreflect case is the following: Defining X n and its cardinal C(n) in Gaia is a bit easier. In both cases, we reason as follows. Consider a ∈ X n , and let b be the sequence with the first element removed. Then n = a 0 + 2m and b ∈ X m . If n is odd, then a 0 = 1; it follows that C(2m + 1) = C(m). On the other hand, if n is even, then a 0 can be 0 or 2, so n = 2m or n = 2m + 2, it follows C(2m + 2) = C(m + 1) + C(m) thus the result:

Lemma expe_fusc n: natp n -> Nbexp n = fusc (csucc n).

• José Grimm

We consider here three sums where the index ranges beween 2 n and 2 n+1 -1:

Let w i be the generic term of the sum. In the first case, w i is an integer and the sum is over the interval [2 n , 2 n+1 [ (below is a sum over 'Nintc n', this is the interval [0, n]). In the two other cases, w i is a rational number, and we compute i<p w p+i , where p = 2 n and p is defined by induction over p. There is no generic sum in Gaia, so the properties of used here are proved only for Q.

In the first case,

. The first sum is T n-1 , and the second sum is

In the second case, w i = 1/(s i s i+1 ). The sum of the i first terms is s i /s p+i provided i ≤ q, (where p = 2 n , q = p/2). Since q is a power of two, the partial sum up to q is s q /s 3q = 1/2. The palindrome condition says that the other part has the same sum, so that T n = 1. We finally assume w i = s i /s i+1 . As previously, we separate the cases, where i is even, and the case i is odd. Let a = s i , b = s i+1 . The first sum is a/(a + b), the second sum is (a + b)/b = q + a/b, and it can be evaluated by induction. We split the first sum in two parts i < q and q ≤ i, and use the palindrome condition for the second half; this has as effect to exchange a and b, so we get b/(a + b); adding these things together gives q/2. All in all, the result is (3p -1)/2 (unless n = 0, and p = 1, this is not an integer). Let's notice the following remarkable result. We consider the quantities i j where i + j = n. If we sum these quantities, we get the Fibonacci sequence (obvious by induction). If we reduce modulo 2, then sum, we get s n+1 . The trick is that b(2n, 2k+1) is even, so that b(2n, 2k), b(2n+1, 2k+1), b(2n, 2k+1) and b(2n+1, 2k) are b(n, k) modulo 2 (here b is the binomial coefficients, proofs are by induction).

• 43

THE SET OF REAL NUMBERS

Definition

A lattice is an ordered set such that each pair of elements has a least upper bound and a greatest lower bound. In a complete lattice, all subsets (even empty ones) have this property. In Exercise 1.15, Bourbaki asks to prove the existence of a "completion"; this is some subset X of P(X), which is a complete lattice for set inclusion, and there is a canonical injection X → X which is strictly increasing. If X is a totally ordered set, then an element of the completion is a set A such that t ∈ A and x ≤ t implies x ∈ A. The complement B satisfies: if t ∈ B and t ≤ x then x ∈ B. The pair (A, B) is called a Dedekind cut.

We shall consider here the ordered set Q, and the set of Dedekind cuts, represented by the B part. This is sometimes called the "extended real number line". It has a least element -∞ (when A is empty) and a greatest element +∞ (when B is empty). Excluding these two elements gives the real line. Let's denote by C x and C x the intervals ]x, →[ and [x, →[ (the set of all rational numbers that are respectively > x and ≥ x). The function C defines the injection Q → R. Note that if B has a least element y, it is of the form C y ; we shall identify this interval with C y . This means that we shall only consider cuts where B has no least element; if B has an infimum, it is of the form C x , and is called a rational cut; otherwise, its complement has no supremum and B is called an irrational cut. We define here the notion of adjacent sequences (a, b) (cf. section 4.1) and the associated cut (A, B). For instance, B is the set of all i such that b i < x for some i, so is the union of the intervals ]b i , →[. Some authors assume the sequences monotone instead of strictly monotone. There are two cases: if the sequence (b i ) i is not eventually constant, we can extract a strictly decreasing sequence that defines the same cut. On the other hand, if b i = b for large i, then B is the interval ]b, →[, the cut is rational, and we may replace the sequence by i → b + 1/(i + 1) which is a strictly decreasing sequence that gives the same cut.

Let (A, B) be the cut associated to the pair of sequences (a, b). If u and v are two rational numbers with u < v then either v is in B, or u is in A, or else, for all i we have v -u ≤ b i -a i . This last case contradicts the condition that the infimum of b i -a i is zero. So either A ∪ B is Q (and B is irrational) or it is Q minus a singleton x (and B = C x ). The converse holds: if x is a real number, there is a pair of adjacent sequences such that B = x; if x is rational,

) is a possibility, Q is the disjoint union of A, B and {x}; if x is irrational the axiom of choice is needed and Q is the disjoint union of A and B.

[Note: this requires approximatively 400 lines of script].

We show here: if √ 2 (denoted B) is the set of x such that 2 < x 2 , then √ 2 is irrational in the sense given above. Firstly x 2 = 2 has no solution since if x = a/b where a and b are coprime, we have x 2 = a 2 /b 2 where a 2 and b 2 are coprime. We get a 2 = 2 and b 2 = 1, absurd. Secondly, B has no infimum. Since (x -) 2 -2 ≥ x 2 -2 -2 x, whenever x > 0, it is possible to choose such that x -∈ B. If we choose by x 2 -2 -2 x = 0 we are led to: if f (x) = (x 2 + 2)/(2x), then x ∈ B implies f (x) ≤ x and f (x) ∈ B. Note that f (x) = x says x 2 = 2, which is impossible. Thirdly, the complement of B has no supremum; it suffices to show that the set A of all x > 0 such that x 2 < 2 has no supremum. Our proof is as follows. Take x = a/b in A and y = (a+1/4a)/b; we have x < y and (by) 2 ≤ a 2 +1; since a is an integer, a 2 < 2b 2 says a 2 + 1 ≤ 2b 2 , so that we get y 2 < 2.

. The functions f and g can be used to create a pair of adjacent sequences for √ 2. Since A is the set of all 2/x for x in B, A has a supremum if and only if

Definition BRsqrt2 := (Zo BQps (fun z => \2q <q z *q z)). Lemma sqrt2_irrational: irrationalp BRsqrt2.

• 45

Arithmetic properties

We define R as the set of all Dedekind cuts, and introduce the canonical inclusion Q → R and some constants, like zero, one, etc. The relation x ⊃ y makes it a totally ordered set; it is not a complete lattice, but every non-empty bounded set has a supremum or an infimum (intersection and union; note that the intersection could be of the form C x , case where C x has to be used instead). There is no greatest element; in fact, for each real number x, then is an integer n such that x ≤ n (take for n the successor of the integer part of any element of x). We say that a real number x is positive if it is a subset of Q + . This is the same as 0 ≤ x. Since x has no least element, this is also x ⊂ Q * + . Note that Q * + = 0. We shall often use the following property: for every real number x, every rational number > 0, there is Lemma rle0xP x: \0r <=r x <-> inc x BRp. Theorem BR_archimedean x: realp x -> exists2 n, natp n & x <r (BR_of_Q (BQ_of_nat n)). Lemma BR_sup_exists X: sub X BR -> nonempty X -> bounded_above BR_order X -> has_supremum BR_order X.

One can define addition, subtraction, multiplication, division, etc, and show the usual properties. The opposite of a real number x is the set of the opposites of the complement of x. If y is rational, and x = C y , this set is C -y , and C -y has to be used instead.

Definition BRopp x := Yo (rationalp x) (BR_of_Q (BQopp (BQ_of_R x))) (fun_image (BQ -s x) BQopp). Lemma BRopp_Q x: ratp x -> BRopp (BR_of_Q x) = BR_of_Q (BQopp x) Lemma BRopp_irrational x: irrationalp x -> BRopp x = (fun_image (BQ -s x) BQopp).

The sum x + y of two real numbers is the set of all a + b, where a ∈ x, b ∈ y. Similarly, x•y is the set of all a•b, where a ∈ x, b ∈ y, at least when a and b are > 0. The inverse is defined like the opposite (at least for positive arguments). Equipped with these operations, R is an ordered field. We show here some properties: if x > 0, then x < 1 is the same as 1 < x -1 , if x and y are non-zero, then 1/x -1/y = (y -x)/(x • y).

• José Grimm (BR_of_Q (BQinv (BQ_of_R x))) (Yo (inc x BRps) (aux x) (BRopp (aux (BRopp x)))).

Lemma BRinv_Q x: ratp x -> BRinv (BR_of_Q x) = BR_of_Q (BQinv x). Lemma BRinv_irrational x (aux:= fun z => BQps -s fun_image z BQinv): irrationalp x -> BRinv x = (Yo (inc x BRps) (aux x) (BRopp (aux (BRopp x)))). Lemma BQ_ltinv1 x: inc x BRps -> (x <r \1r <-> \1r <r BRinv x). Lemma BRinv_diff x y: realp x -> realp y ->x <> \0r -> y <> \0r -> (BRinv x -r BRinv y) = (y -r x) /r (x *r y).

Application: the square of √ 2 is 2. An element of the square of √ 2 is the product of two numbers u and v of √ 2; this product is obviously > 2; conversely, assume t > 2; write t = a/b, d = 2a + 1, let n be the integer such that n 2 ≤ abd 2 < (n + 1) 2 and c be n considered in Q. A little computation shows then u = c/(bd) and v = (ad)/c are in √ 2, and the product is t.

Lemma BRsqrt2_prop: inc BRsqrt2 BRps /\ BRsquare BRsqrt2 = \2r.

Cauchy sequences

We say that a sequence x (with values in R or Q) has a limit l if for every rational number > 0, there is an integer N such that if N ≤ n, then |x n -l| < . We say that the sequence is Cauchy, if for every every rational number > 0, there is an integer N such that if N ≤ n, and N ≤ m, then |x n -x m | < . If a limit exists it is unique and the sequence is Cauchy. An important property satisfied by R and not Q: every Cauchy sequence has a limit. Consider first a Cauchy sequence of rational numbers y. Let B be the set of all t ∈ Q such that, for some N , y n < t when n ≥ N . If B has a least element b, then b is the limit of the sequence y. Otherwise B is a real number (note that B is non-empty since the sequence y is bounded), and is the limit of y. Let x be a real Cauchy sequence. We can find (via the axiom of choice) a sequence of rational numbers y such that |x n -y n | < 1/(n + 1). This sequence is then Cauchy, and its limit is the limit of x. [The proof requires 400 lines of script].

• 47 Lemma BR_complete s: CauchyR s -> exists2 x, realp x & limitR s x.

Continuity

We say that f is continuous at x if the usual epsilon-delta condition is satisfied. This is a local condition. Addition, subtraction, multiplication, division are continuous (since the inverse of zero is zero, this function has a discontinuity there; so that division is continuous in its second argument only when it is non-zero). A non-trivial property is that the product of two continuous functions is continuous; in particular x → x 2 is continuous. Lemma continuous_comp f g x: continuous_at f x -> continuous_at g (f x) -> continuous_at (g \o f) x. Lemma continuous2_div x y: realp x -> realp y -> (continuous_at (BRdiv ^~y) x) /\ (y <> \0r -> continuous_at (BRdiv x) y). Lemma continuous_square: continuous BRsquare.

Let f be a continuous function on [x, y] (it is semi-continuous at x and y); if v is between f (x) and f (y), then there is z between x and y such that f (z) = v. Proof. We may assume f (x) ≤ f (y) and v = 0. Let E be the set of all t in the interval I = [x, y] such that f (t) ≥ 0. This is a non-empty bounded set thus has an infimum z in I. Assume f (z) > 0. This says z = x, so that there exists t (near z) such that x < t < z with f (t) > 0. This says t ∈ E, absurd. Assume f (z) < 0; this says z = y. There is > 0 such that z + < y and that f is negative on [z, z + ]. No element of this interval is in E, so that z + is a lower bound of E, contradicting the fact that z is the greatest lower bound. It follows f (z) = 0.

Application: each positive real number x has a square root. We have (-y) 2 = y 2 but the square root is unique in R + . By uniqueness, the square root of 2 is equal to the quantity √ 2 introduced above.

Lemma BRsqrt_exists x: inc x BRp -> exists2 y, inc y BRp & x = BRsquare y. Definition BRsqrt x := select (fun z => x = BRsquare z) BRp. Lemma sqrt2_prop : BRsqrt2 = BRsqrt \2r.

• José Grimm

Assume that f is a function such that a ≤ t implies a ≤ f (t) ≤ t. Fix x 0 ≥ a and define x n by x n+1 = f (x n ). Then the sequence (x n ) n∈N is decreasing hence has a limit x (namely inf i (x i )) such that a ≤ x. If f is continuous at x, then f (x) = x.

[Note: by assumption f (a) = a so that the limit could be a; if f (t) = 1/(1+(t-1)) 2 , the limit is b = 1 when b ≤ x 0 ≤ 2, and a = 0 otherwise.] Application. We define here a pair of adjacent sequences defining √ a. In fact we assume a real positive, so that the members of the sequence are real, but if a were rational, then the sequence would be rational as well. The first sequence corresponds to the Newton Scheme for solving x 2 = a. Let f (x) = (x 2 + a)/(2x). Let B be the set of all positive x such that x 2 ≥ a. We have

, where x 0 is big enough (say ≥ 1 + a) then x n converges to some x (the infimum of the range). If the limit is zero then a must be zero; otherwise f is continuous at x, so that f (x) = x and x 2 = a.

Let now g(t) = (f (t) + t)/2 and y n+1 = g(y n ), Let A be the set of all positive t such that a/9 ≤ t 2 ≤ a. We simplify our reasoning by assuming that a has a square root b, and define A as the set of all t such that b/3 ≤ t ≤ b. We have t -g(t) = (t -f (t))/2, so that g(t) ≤ t when t ∈ B, thus t ≤ g(t) when t ∈ A. We have g(t) -b = (t -b)(3t -b)/4t. This says that A is invariant by g. Thus if y 0 ∈ A, the sequence (y n ) n is increasing in A; its supremum y is a fixed point of g, thus of f , thus is b. [Size of the proof script: 280 lines.] • José Grimm -When dealing with a non-trivial recurrence relation of the form (4), the Gaia definition is trivial, and one has to prove a posteriori that it makes sense, on the other hand Coq requires a measure (an a priori proof of termination) or a bound on the number of operations, and a proof that the bound is big enough. -In Coq, we can use the list data structure, instead of a functional graph on I n ; for instance, the expansion to base b is a list a and a i b i is defined by the Horner Scheme; the second relation of (2), namely E n+1 (a) = a 0 + bE n (a ) becomes trivial, and the first is more complicated. Defining the base two reverse is easier: it suffices to revert the list.

-Assume that we want to count something, for instance, the number of integers < n such that the binary representation is formed of some digits 1, followed by some digits 0; the number of integers < n whose base ten expansion contains only even digits; the number of ways to express an integer as a sum of distinct Fibonacci numbers; the number of ways to write n in base two, using 0, 1 and 2 as digits; the number of surjective functions I n → I m . In each case, the objective is to compute c n = card(E n ) for some finite set E n . The ssreflect library provides a theory of finite sets, in which these cardinals can be computed. The difficulty is that the theory requires a finite type T such that E n ⊂ T . In the first two cases, one can take T = I n ; but this choice makes proofs by induction impossible; so one takes T = I m for some m ≥ n, this gives a cardinal c n,m , and an additional task: prove that is it independent of m. The other cases are similar, a bit more complicated. -Some exercises of section 5 of [START_REF] Bourbaki | Elements of Mathematics, Theory of Sets[END_REF] ask to prove some formulas on Z by using different ways to compute the cardinal of a same set; for instance k (-1) k n k = 0 says that there are as many subsets of I n with even and odd cardinal. Showing this in ssreflect should be easy (there are of course alternate proofs). In the current version of Gaia, we cannot even express the formula; so one of our priorities is to develop a generic sum on Z, in order to solve more such exercises.

Comparison with Bourbaki

A fondamental difference between Bourbaki and Coq is the type system: there are two types in Bourbaki: set and relation, and one can only quantify over sets, while Coq has an arbitrary number of types. This means that Criterion C61 and C62 are written in English and not in mathematical language of the form: ∀r, r(0) ∧ H(r) =⇒ C(r) (for some H and C). Note that r is a relation, and replacing the free variable n by 0 gives the relation r [START_REF]y + z) : ∀x, y, at least one of x < y, x = y or y > x holds[END_REF]. It is forbidden to replace n by a relation. In Gaia we make the distinction between Prop (relations without free variables) and Set→ Prop (relations with one free variable) and we allow Prop→ Prop (relations with one free variable that is a relation). We make a distinction between x = x (a relation with a free parameter) and ∀x, x = x (a theorem).

Our current implementation of cardinals uses von Neumann ordinals, rather than the Axiom of Choice. This allowed us to weaken our Axiom of Choice (Scheme S7 is not an axiom in Gaia; in other terms, ∀x, P ⇐⇒ Q does not imply τ x P = τ x Q).

[On occasions, Bourbaki is a bit conservative, for instance, the only English edition of the Theory of Sets, translated in 1968, uses an axiom for the ordered pair,