10.6092/issn.1972-5787/4771
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.
application/pdf
1972-5787
4771
2
en
José Grimm
Journal of Formalized Reasoning
real numbers
Implementation of Bourbaki's Elements of   Mathematics in Coq:  Part Two, From Natural Numbers to Real Numbers
Text.Serial.Journal
https://jfr.unibo.it/
9
Articles
2016-12-01
2015-03-06
2016-12-01
2017-09-04
1 -52
JFR
José Grimm
2016/12/01
10.6092/issn.1972-5787/4771
1
INRIA,  Marelle Team
1972-5787
2
real numbers
en
52
Moritz Stern. Ueber eine zahlentheorische Funktion. Journal für die reine und angewandte Mathematik, 55:193–220, 1858.
Implementation of Bourbaki's Elements of   Mathematics in Coq:  Part Two, From Natural Numbers to Real Numbers
https://jfr.unibo.it/article/download/4771/6203
9
Implementation of Bourbaki’s Elements of
Mathematics in Coq:
Part Two, From Natural Numbers to Real Numbers
JOSÉ GRIMM
Inria Sophia-Antipolis, Marelle Team
Email: Jose.Grimm@inria.fr


This paper describes a formalization of the rst book of the series Elements of Mathematics by
Nicolas Bourbaki, using the Coq proof assistant.            In a rst paper published in this journal, we
presented the axioms and basic constructions (corresponding to a part of the rst 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   (rst 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 Ssreect library, then present our implementation.




1.     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 math-
ematics. We have chosen the “Elements of Mathematics” of Bourbaki as our guide-
line, the Coq proof assistant as tool, and ssreflect as proof language. As ex-
plained in the first paper [Gri10], 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 [BLM14]; we shall consider here only the Coq system, that uses a higher-
order 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 library1
(see discussion in subsection 1.4). In Coq the set of natural integers comes for

1 In   short, MathComp; for details, see the web site http://math-comp.github.io/math-comp/


                                                Journal of Formalized Reasoning Vol. 9, No. 2, 2016, Pages 1–52.
2       ·    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 sub-
section 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.
                                 P Our ambition is more modest: provide a setting
in which formulas of the form 2n ≤i<2n+1 1/(si si+1 ) = 1 can be expressed and
proved correct [Here sn 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,
[Bou68]) with axioms designed by Carlos Simpson [Sim04a, Sim04b]; the imple-
mentation of Chapter 1 and 2 (“Description of formal mathematics”, and “Theory
of sets”) has been presented in [Gri10], 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 sec-
tions 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 Coq
libraries, and discuss further work on this subject.

1.2     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

2 bythe Burali-Forti paradox, there is no type for all the ordinals
3 Forinstance 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 Formalized Reasoning Vol. 9, No. 2, 2016.
                            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-structure, a morphism, and how can
these notions be implemented in computer.
   Bourbaki has a whole Chapter of Book I that deals with structures. Its def-
initions 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
[Sim04a, Sim04b] (who designed the axioms used in Gaia) explains a possible de-
sign for structures. For instance an ordered group is a record4 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 commuta-
tive group is given in the tutorial [GM10]; details about effective implementation
in ssreflect can be found in [GGMR09], for instance, it is explained how a com-
mutative 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 ex-
pressions 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 1Z .
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 1Q ). 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

4 The   trick is that the record has type Set and not Type



                                                 Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
4       ·     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 explicit structure, but we provides lemmas
of this form in each particular case).
                                          P
   The library provides a generic sum i∈I xi where the index belongs to a finite
set (a list, an interval In , 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 set, provided that all but a finite number of values are equal to
the unit.

1.3      Constructing the real numbers 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 opera-
tor; 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
(Ai )i∈I (i.e., the set of all (x, i), where i ∈ I and x ∈ Ai , or the set of all functional
graphs x with domain I such that     P xi ∈ AiQ   ) is called the cardinal sum or cardinal
product of the family, denoted i∈I Ai or i∈I Ai . Replacing Ai 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 AB (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
that x < x+ , and for no y do we have x < y < x+ . Obviously x + 1 ≤ x+ ≤ 2x . An
integer is a cardinal x such that x 6= x + 1. In this case, x + 1 is the successor of

5 In   ssreflect, this denotes an abelian group, which is canonically a module over Z.


Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
                         Theory of Sets / From natural numbers to real numbers            ·     5

x (the Generalized Continuum Hypothesis asserts that, if x is not an integer, then
x+ = 2x ).
  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 [Bou89a]
(Algebra, Chapter I, section 2, paragraph 5) as the group of differences6 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 (m1 , n1 ) and (m2 , n2 ) which is written m1 + n2 =
m2 + n1 ; 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.

   1.3.3 Rational numbers. In section 8, paragraph 11 of [Bou89a], Bourbaki no-
tices 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 6= 0 (and we may
even take b > 0). Q+ is used to denote the set of rational numbers of the form

6 Similarlyto Q and R below, Bourbaki introduces a general notion, here “group of differences”,
and in the particular case, finds a more practical definition: Z = N ∪ −N∗ .


                                              Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
6     ·      José Grimm

a/b with a ∈ N and b ∈ N∗ .” This set is stable by addition and multiplication; the
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 6∈ 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 x0 ≤ y 0 imply x + x0 ≤ y + y 0 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 [Bou89b]. The first claim is that there is a unique topology on Q, com-
patible with the additive structure such that a fundamental system of neighbor-
hoods 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) using the
same arguments shown in the previous paragraph.
  This is a short introduction to real numbers; a whole book is dedicated to the
study of functions of a real variable.

1.4   Real numbers in Coq

   We shall explain how integers, rational and real numbers are implemented, both
in the standard Coq library and in ssreflect7 . To begin with, the natural num-
bers are defined by

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

   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).
7 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 Formalized Reasoning Vol. 9, No. 2, 2016.
                       Theory of Sets / From natural numbers to real numbers           ·     7

Inductive le (n:nat) : nat    -> Prop :=
  | 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.

  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.

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.

   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 op-
erations (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
                                           Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
8     ·     José Grimm

A and B are two types, with a coercion f , two operations gA and gB with the same
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.

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.

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

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.

   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 do-
main, 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 xn 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 xn , where x is in the ring and n ∈ Z, such that x.2 = x + x and x2 = 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 6= 0,
then xn = 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.
Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
                       Theory of Sets / From natural numbers to real numbers          ·     9

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

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.

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.

  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 denom-
inator have different types, notations are sometimes a bit folkloric), in such a way
that x ∼ x̄, and x ∼ y implies x̄ = ȳ. Note that x = x̄ if and only if the numerator
and denominator of x are coprime; thus, if y is x̄, we have ȳ = 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 Xv and a proof Xp of Xv = Xv . The non-
trivial point with this definition is to prove that Xv ∼ Yv implies X = Y (that
Xv = Yv is obvious, so that Yp becomes a second proof of Xv = Xv , 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 Xv = x̄. Then x, y 7→ 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.

                                          Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
10      ·     José Grimm

Record rat : Set := Rat {
   valq : (int * int) ;
   _ : (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:

     Rplus_comm: ∀x, y, x + y = y + x.
     Rplus_assoc: ∀x, y, z, (x + y) + z = x + (y + z).
     Rplus_opp_r: ∀x, x + (−x) = 0.
     Rplus_0_l: ∀x, 0 + x = x.
     Rmult_comm: ∀x, y, x ∗ y = y ∗ x.
     Rmult_assoc: ∀x, y, z, (x ∗ y) ∗ z = x ∗ (y ∗ z).
     Rinv_l: ∀x, if x 6= 0 then (/x) ∗ x = 1.
     Rmult_1_l: ∀x, 1 ∗ x = x.
     R1_neq_R0: 1 6= 0.
     Rmult_plus_distr_l: ∀x, y, z, x ∗ (y + z) = x ∗ y + x ∗ z.
     total_order_T: ∀x, y, at least one of x < y, x = y or y > x holds.
     Rlt_asym: ∀x, y, at least of one x < y and y < x is false.
     Rlt_trans: ∀x, y, z, x < y and y < z implies x < y.
Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
                          Theory of Sets / From natural numbers to real numbers          ·     11

   Rplus_lt_compat_l: ∀x, y, z, x < y implies z + x < z + y.
   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 (xn )n∈N is Cauchy, it
is bounded, so that one may consider vn = supn<k xk . This sequence is decreasing,
and has a lower bound, thus converges to v (in fact to inf vn ). Clearly v is the limit of
(xn )n . On the other hand, every real number x is the limit of a sequence of rational
numbers: let xn = u(2n x)/2n , by archimed we have xn − 1/2n ≤ x ≤ un , hence
|x − un | ≤ 1/2n . 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).

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

  The ssreflect library, on the other hand, does not provide real numbers, but
the MathComp library8 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(mx ()) − y(my ())|. This means: there is  > 0, such that, if i is big enough then

8 In   the mathcomp/real_closed directory on GitHub, accessible via the MathComp web page

                                              Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
12     ·     José Grimm

 ≤ |x(i) − y(i)|. If moreover x(mx ()) + 3 ≤ y(my ()), 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
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 7→ x(i) + y(i)
and i 7→ 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 imple-
ment the set of real algebraic numbers, as described in [Coh12].

1.5   The axioms of Gaia

  Our work relies on an axiomatization of the theory of Zermelo-Fraenkel as de-
scribed in [Gri10]; 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
Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
                         Theory of Sets / From natural numbers to real numbers            ·     13

                  the doubleton {a, b}Ssuch that x ∈ {a, b} if and only if x = a or
the existence of: S
x = b, the union X such that x ∈ X if and only if there is y such that x ∈ y
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 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 surjective9 . 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 7→ 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.
  The doubleton {x, y} is defined by ‘IM (fun z => if z then x else y)’ (note that
z has type bool). Write 0 or ‘C0’ instead of ∅, 1 or ‘C1’ instead of {0, 0} and 2 or
‘C2’ instead of {0, 1}. Then 2 is a set with exactly two elements, and is called “the
canonical doubleton”. This differs from what is described in [Gri10]: we considered a
copy of bool, say D, with two constructors, say d1 and d2. This is a set with exactly
two elements ‘@Ro D d1’ and ‘@Ro D d2’, and was used as canonical doubleton (in
particular, in the definition of {x, y} instead of bool).
  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 independent10 of x) and p(τx (p)) denotes the relation

9 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.
10 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 Formalized Reasoning Vol. 9, No. 2, 2016.
14     ·     José Grimm

obtained from p by replacing every occurrence of x by τx (p); it is thus independent
of x. The quantity τx (p) is denoted in Gaia by ‘choose p’, and the axiom of choice
is: ‘ex p → p(choose p)’. In the case where thereSis 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 6= ∅; in this case, we denote by ‘rep E’ (in short r(E))
the quantity τx (p). We have then: ∀E, E 6= ∅ ⇒ r(E) ∈ E. One easily deduces
Zermelo’s theorem: every set can be well-ordered (see [Gri10]).
   Bourbaki manipulates only two kinds of objects: terms and relations, this corre-
sponds 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 6= ∅” 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 kxk (instead of
a double bar, there is a specific symbol, not used by anyone else): “if A is an as-
sembly 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 Akxk or Akx, yk. In
this case we write AkBk instead of (B|x)A. We denote by AkB, Ck 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 kQkx, ∅kk means ((∅|y)Q|x)P .
Note that, if x appears in A, and B is a relation, then one of Akxk and AkBk is
ill-typed; for this reason Bourbaki uses AkBk 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 Rkxk is a relation, then (U = V ) ⇒ (RkU k ⇔ RkV k) 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 kT k = V kU k), whenever T , U and V are terms. Proof. Assume
T = U ; by symmetry we have U = T . Substitute this relation in V kxk = V kU k; we
get V kU k = V kU k ⇔ V kT k = V kU k. 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).
Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
                      Theory of Sets / From natural numbers to real numbers          ·     15

On the other hand, consider Card(X) = τZ (Eq(X, Z)) introduced in section 1.3.1.
Let X 0 be a set equipotent to X, so that Eq(X, Z) ⇔ Eq(X 0 , Z). Scheme S7 says
Card(X) = Card(X 0 ), 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).

1.6   Order relations and ordered sets

  A pair (x, y) is a set z from which x and y can be recovered (via x = pr1 z and
y = pr2 z). It is defined by an Axiom in Bourbaki [Bou68], and as {{x}, {x, y}} in
the 1970 French Edition [Bou70]. In Gaia, the constructor 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 pr1 hGi, is called the domain of the graph, and the set of
all y, namely pr2 hGi, 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 Gx 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 (xn )n , sometimes by n 7→ xn .
A finite sequence is a functional graph whose domain is a finite subinterval of
N; it may be denoted by (xn )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 hXi 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 ∈ Γhxi (an abuse of notations for y ∈ Γh{x}i). 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

                                          Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
16     ·     José Grimm

usual ordering) defined in §3, no. 2, that is under consideration, unless the contrary
is expressly stated”.
   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
pr1 hGi. 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 an 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.

1.7   Cardinal and ordinal numbers

  Let E be a well-ordered set and T a functional term. 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 < x11 ). There is a unique surjective function f (called defined by transfinite
induction on E via T ) such that f (x) = T (f (x) ) whenever x ∈ E. This is Criterion
C60 of Bourbaki, the existence part is the following:

Definition transfinite_def r (p: fterm) f :=
  [/\ surjection f, source f = substrate r &
  forall x, inc x (substrate r) -> Vf f x = p (restriction_to_segment r x f)].
Lemma transfinite_defined_pr r p: worder r ->
  transfinite_def r p (transfinite_defined r p).

The proof (see for instance) [Gri10] uses 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 well-
order 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,

11 It is traditionally denoted ]−∞, x[; if E has a least element e, then ]←, x[ = [e, x[; similarly

[x, →[ corresponds to [x, +∞[

Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
                        Theory of Sets / From natural numbers to real numbers           ·     17

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
Exercice of Bourbaki, it is equivalent to the definition of von Neumann; for details
of implementation, see [Gri09]).
  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 xy 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 6= 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 ω.

                                             Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
18     ·     José Grimm

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

2.1   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
Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
                      Theory of Sets / From natural numbers to real numbers          ·     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 Rknk be a relation in a theory T (where n is not a constant of T ).
Suppose that the relation
            Rk0k and (∀n)((n is an integer and Rknk) =⇒ Rkn + 1k)
is a theorem in T . Under these conditions the relation
                         (∀n)((n is an integer ) =⇒ Rknk)
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:

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.

  C62. Let u be a letter and let T kuk 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 kf (n) k,
where f (n) 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.
  This criterion is the specialization to N of criterion C60 (introduced in section
1.7). It uses the interval In = [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 In 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 0 , ∀x, F (where F and F 0 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 Xn such that
a formula of Xn+1 is either a formula of Xn or satisfies the previous property (with
F , F 0 in Xn ), then consider the union of these Xn . Each formula has a depth (the
least n such that the formula is in Xn ), 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 fn whose source is Xn , then takes
the common extension in order to get a function on the union).
                                          Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
20     ·     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 kf (n) k. 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 Skvk 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) = Skf (n − 1)k 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) = Skf (n)k 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).

2.2   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 7→ Xi . 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 Xi 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 ∈ Xi . The cardinal of S are called the cardinal sum of the family and
denoted ‘csum X’; there is a variant csumb that takes two P arguments: the domain
and the evaluation function; what is traditionally written i∈I Xi corresponds to
‘csumb I (fun i => Vg X i)’ or ‘csumb I (Vg X)’.
                  P
   The quantity i∈I Xi remains unchanged if each Xi is replaced by an equipotent
set (for instance its cardinal).
                         P       Commutativity
                                   P             of addition means that if f is any
bijection J → I, then i∈I ai = j∈J af (j) . Associativity of addition means: if
(Ik )k∈KP is a functionalP        P of mutually disjoint sets whose union is I and
                         graph formed
if sk = i∈Ik ai , then i∈I ai = k∈K sk . It is important (for the ease of proofs)
to notice that we do not require a be a functional graph, nor ai to be a cardinal.

Theorem csum_An f g:
  partition_w_fam g (domain f) ->
Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
                         Theory of Sets / From natural numbers to real numbers             ·     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:

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.
                          Q
   The cartesian product i∈I Xi is the set of all functional graphs f defined on I
such that f (i) ∈ Xi 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),
                                        Q            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 Xi 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 ((aj,i )i∈Jj )j∈L be a double family, then
               Y X          X Y                                  Y
                       aj,i =             aj,f (j)     where I =       Jj .        (1)
               j∈L   i∈Jj          f ∈I   j∈L                              j∈L

As in the case of a sum, formulas are simpler when the family is reduced to two
elements:

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

   We define ab 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
zero12 .

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.

12 The expressions a + 0 and a ∗ 1, defined whatever a are equal to card(a), hence to a when a is

a cardinal
                                                Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
22     ·     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)) = 2X (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) 6∈ z). One deduces a < 2a , 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 6= x + 1. In this case x + 1 = x+ .
The relations a + (b + 1) = (a + b) + 1, a · (b + 1) = a · b + a and ab+1 = ab · 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.

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.

   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.



Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
                      Theory of Sets / From natural numbers to real numbers          ·     23

2.3   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
P          on theQdomain). In particular, if f (k) is an integer for k < n, then
  k<n f (k) and k<n f (k) are integers. If Sn is the sum then Sn+1 = Sn + f (n);
                   induction on n via this formula that Sn is an integer. One also
one could prove by P
has Sn+1 = f (0) + i<n f (i + 1). Consider for example
                                          X
                                Enb (a) =     ai bi
                                             i<n

where (ai )i<n is a sequence
                     P        of integers and b ≥ 2 [If b = 0, the sum is a0 for n > 0,
if b = 1, the sum is    ai , we shall omit the index b in what follows]. We have
                      En+1 (a) = En (a) + an bn = a0 + bEn (a0 )                          (2)
where a0 is the sequence i 7→ ai+1 . In what follows, we shall assume implicitly
ai < b for each i. We deduce: an and En (a) are the quotient and remainder in
the division of En+1 (a) by bn ; En (a0 ) and a0 are the quotient and remainder of the
division of En+1 (a) by b.
  It is easy to deduce from these considerations that, for every integer A, if A < bn ,
there is a unique sequence (ai )i<n such that A = En (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 ai = 0 for n ≤ i for the second expansion; thus, there is a unique expansion
(called normal) with n = 0 or an−1 6= 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 ck is non-zero, or there are two indices k, p
such k < p ≤ min(n, m) and ak < ck , ai = ci for k < i < p; moreover ai and ci
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,
ak < ck , ai = ci for k < i < n. Bourbaki states this in Proposition 8 of §5.7 as: “let
Ek be the lexicographic product of the family (Jh )0≤h≤k−1 of intervals all identical
with [0, b − 1], then fk is an isomorphism of the ordered set Ek onto the interval
[0, bk − 1].” Here, all intervals (including [0, h − 1]) are ordered by ≤; since the
leading digits have to be comparedP  first, this leading digit corresponds to h = 0; for
                                       k−1
this reason Bourbaki uses fk (r) = h=0 rh bk−h−1 . The condition for the expansion
to be normal simplifies to r0 6= 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 ah bh , where ah = 0 for h ≥ k.]
                     P

Lemma expansion_prop15 f g b n:

                                          Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
24      ·    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)]).
                         P
   Let C(A) be the sum i<n ai where A = En (a). Assume that A is not a digit
(so that A > b and there is i such that 0 < i < n and ai 6= 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 0 (A). The two quantities A and C(A) are equal modulo
b − 1 (since bn is one modulo b − 1). Thus A and C 0 (A) are the same modulo b − 1.
One can be more precise: either A = 0 case where C 0 (A) = A, or A 6= 0, case where
C 0 (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 0 (A) = b − 1, or C 0 (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))].

   A special case is expansion to base two. Here ai < b says ai = 0 or ai = 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 2ln(n)−1 ≤ n < 2ln(n) .
Moreover aln(n)−1 = 1. We define the base-two reverse r(n) of n to be El (a0 ),
where the sequence a is the base two expansion of n, l its length, and a0i = al−1−i .
The relation al−1 = 1 says a00 = 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.
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) :
  natp n -> r (r (r n)) = r n.

2.4    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].
Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
                       Theory of Sets / From natural numbers to real numbers           ·     25

   A first consequence is: the number Anm of injections of a set with m elements
into a set ofQn elements satisfies An,m+1 = An,m · (n − m) thus Anm = 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 0 = E − {a}, a function f : E → F is characterized by its value at a, and the
restriction f 0 to E 0 . In order for the function f to be injective, we need f 0 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 0 , but not its cardinal, which is n − m].
                                                        P
   Let (pi )i<h be a finite sequence of integers, n =      pi , E a set with n elements;
the number
      Q       of ways    to write E as the union of disjoint  sets Ei with cardinal pi is
n!/( i<h pi !). Proof. Let I = [0, n[, and consider a partition Ik of I formed of sets
with pi elements (Ik contains the pk smallest elements not in Ij for j < k). Let
f : I → E be a bijection, g a permutation of I, Ek the image by f ◦ g of Ik , G(g)
the sequence of these Ek . The family G(g) is a solution, every solution has this
form; the relation G(g) = G(g 0 ) is equivalent to say that g −1 ◦ g 0 , restricted to each
Ik , is a permutation (size of the proof: 450 lines of script).

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

  Using the same techniques, one deduces the following (250 lines of script).
                 X                n!
                                             ap11 ...apkk = (a1 + a2 + · · · + ak )n .      (3)
            p +p +···+p =n
                           p 1 ! · · · p k !
               1   2     k


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

   Application: the number   of subsets with p elements in a set with n elements
is n!/(p!(n − p)!) = np . 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
                                            Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
26         ·    José Grimm

be used directly. So, we define a functional graph fn with domain N such that
fn+1 (m) = fn (m) + fn (m − 1), and apply it to m. The anonymous function has an
unused parameter (the value of n), the second parameter being fn . 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 f0 (0) = 1 and fn+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.

   Our library contains many other formulas, using similar or different proof tech-
niques. For instance (3) holds in any ring (the only condition being that ai aj =
aj ai ) and can be shown by induction13 . 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 = In
and F = Im (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 In+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
               P          functions
                               P is the same as counting the number of functions
h such that      hi = m (or       hi ≤ 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.
  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 ofP  increasing functions (in fact, sorted lists) and the number of functions
such that     hi ≤ m.

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

  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 Sn,p be the
number of surjections In → Ip . There is an explicit formula, but it requires negative
numbers. On the other hand, there is an implicit formula relating Sn,i , the binomial

13 rings   are not implemented in Gaia; so proving it will be a challenge

Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
                        Theory of Sets / From natural numbers to real numbers             ·     27

coefficients and the number of functions In → Ip (every function is a surjection on
its image). There is also a simple recurrence relation, Sn,p = p(Sn−1,p + Sn−1,p−1 )
(proved in Gaia), and if Pn,p is the number of partitions of In into p parts, then
Sn,p = p!Pn,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).

3.    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 6= 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).

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

     Consider the following three functions, with range N2 , Z and N2 respectively:
                                       (
                                         (0, |x|) if x ∈ Z+
                          f : x ∈ Z 7→
                                         (|x|, 0) otherwise,
                                        (
                                      2  φ+ (y − x)           if x ≤ y
                      g : (x, y) ∈ N 7→
                                         φ− (x − y)           otherwise,

                   h : ((x, y), (x0 , y 0 )) ∈ N2 × N2 7→ (x + x0 , y + y 0 ).
Note that g is surjective as g(f (x)) = x, but not injective; however g(x, y) = g(x0 , y 0 )
is equivalent to x + y 0 = x0 + 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))
                                               Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
28      ·    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:

Definition BZsum x y:=
  let abs_sum := (BZ_val x) +c (BZ_val y) in
    let abs_diff1 := (BZ_val x) -c (BZ_val y) in
      let abs_diff2 := (BZ_val y) -c (BZ_val x) in
        Yo (inc x BZp /\ inc y BZp) (BZ_of_nat abs_sum)
        (Yo ( ~ inc x BZp /\ ~ inc y BZp) (BZm_of_nat abs_sum)
          (Yo (inc x BZp /\ ~ inc y BZp)
            (Yo ( (BZ_val y) <=c (BZ_val x))
              (BZ_of_nat abs_diff1) (BZm_of_nat abs_diff2))
            (Yo ( (BZ_val x) <=c (BZ_val y))
              (BZ_of_nat abs_diff2) (BZm_of_nat abs_diff1)))).
Lemma BZsum_alt x y: intp x -> intp y -> BZsum x y = Bzsum x y.

  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 7→ −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 BZ_ordering:=
  order_sum2 (opp_order (induced_order Nat_order Nats)) Nat_order.
Lemma zle_cN a b: natp a -> natp b ->
    (a <=c b <-> BZ_of_nat a <=z BZ_of_nat b).
Lemma zlt_opp x y: x <z y -> (BZopp y) <z (BZopp x).
Lemma zle_opp_iso:
  order_isomorphism (Lf BZopp BZ BZ) BZ_ordering (opp_order BZ_ordering).
Lemma zlt_succ1P a b: intp a -> intp b ->
  (a <z (BZsucc b) <-> a <=z b).
Lemma BZ_order_isomorphism_P f:
Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
                      Theory of Sets / From natural numbers to real numbers          ·     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 x0 = y0 = a, xn+1 is the successor of xn
and yn+1 is the predecessor of yn . 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.

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

                                          Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
30     ·     José Grimm

 If a and b are in Z, b 6= 0, there is a unique solution in Z of a = bq +r, 0 ≤ r < |b|.
We give here the definition and characteristic property.

Definition BZdivision_prop a b q r :=
  [/\ a = (b *z q) +z r, r <z (BZabs b) & inc r BZp].

Definition BZquo a b :=
  let q:= BZ_of_nat ((BZ_val a) %/c (BZ_val b)) in
    Yo (b = \0z) \0z
    (Yo (BZ_sg a = C1) (Yo (BZ_sg b = C1) q (BZopp q))
      (Yo ((BZ_val a %%c BZ_val b) = \0c) (Yo (BZ_sg b = C1) (BZopp q) q)
        (Yo (BZ_sg b = C1) (BZopp (BZsucc q)) (BZsucc q)))).
Lemma BZdvd_correct a b: intp a -> intp b -> b <> \0z ->
  [/\ inc (a %/z b) BZ, inc (a %%z b) BZp &
  (BZdivision_prop a b (a %/z b) (a %%z b))].
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. If x ∈ I,
and x = cq + r, then r ∈ I. But if r is the remainder of x by c, we get 0 ≤ r < |c|,
thus r = 0. It follows that I(a, b) = I(c, c). The quantity c is called the gcd of a
and b, and ab/c is called the lcm.

Definition BZgcd a b := select (fun z => BZ_ideal1 z = BZ_ideal2 a b) BZp.
Definition BZlcm a b := (a *z b) %/z (BZgcd a b).

  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
[Bou68] 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).

Definition BZgcd_prop a b p :=
Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
                     Theory of Sets / From natural numbers to real numbers          ·     31

   [/\ p %|z a, p %|z b & forall t, t %|z a -> t %|z b -> t %|z p].
Lemma BZgcd_prop3 a b: intp a -> intp b ->
   (BZgcd_prop a b (BZgcd a b)
       /\ forall g, BZgcd_prop a b g -> (BZgcd a b) = BZabs g).

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

Definition BZcoprime a b := BZgcd a b = \1z.
Definition Bezout_rel a b u v := (a *z u) +z (b *z v) = \1z.
Definition BZBezout a b :=
  exists u v, [/\ intp u, intp v & Bezout_rel a b u v].
Lemma BZ_Bezout_cofactors a b: intp a -> intp b ->
 (a<> \0z \/ b <> \0z) ->
  BZBezout (a %/z (BZgcd a b)) (b %/z (BZgcd a b)).
Lemma BZgcd_simp a b c: intp a -> intp b -> intp c ->
   BZcoprime a b -> BZgcd a (b *z c) = BZgcd a c.

  The Bezout relation is not unique: for every q, u0 = u + qb, v 0 = v − qa yields
another solution. Assume a 6= 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|.
  Assume a ∈ N, b ∈ N. We can coerce a and b into Z, compute the gcd, and
put it back on N. It satisfies the expected properties. Unless a and b are trivial,
the Bezout relation does not hold on N. However the variant au = 1 + bv holds.
Of course, this equation does not have a unique solution. One may assume u < b
when b > 1. (Note: ssreflect gives an algorithm, that returns such a pair, with
v < a, when a 6= 0).

Definition Ngcd_prop a b p :=
   [/\ natp p, p %|c a, p %|c b &
    forall t, natp t -> t %|c a -> t %|c b -> t %|c p].
Lemma Ngcd_P a b: natp a -> natp b ->
   (Ngcd_prop a b (Ngcd a b)
       /\ forall g, Ngcd_prop a b g -> (Ngcd a b) = g).
Lemma Nbezout a b: natp a -> natp b -> a <> \0c -> Ncoprime a b ->
   exists u v, [/\ natp u, natp v, a *c u = \1c +c b *c v&
      (b <=c \1c \/ u <c b)].

  Application: gcd(Fn , Fm ) = Fgcd(n,m) , where Fn is the n-th Fibonacci number.
In particular, two consecutive Fibonacci numbers are coprime. We give here a
formula for Fn−m ; if m is n − 1 or n − 2, we get a Bezout relation between Fn and
Fn+1 , of the form au = 1 + bv, u < b.

Lemma Ngcd_fib n m: natp n -> natp m ->
  Ngcd (Fib n) (Fib m) = Fib (Ngcd n m).
Lemma Fib_sub n m: natp n -> natp m -> m <=c n->
  Fib (n -c m) = Yo (evenp m)

                                         Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
32     ·     José Grimm

     (Fib n *c Fib (csucc m) -c Fib (csucc n) *c Fib m)
     (Fib (csucc n) *c Fib m -c Fib n *c Fib (csucc m)).

  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.

Definition BZ_of_Z (n:int) :=
  match n with
    | Posz p => BZ_of_nat (nat_to_B p)
    | Negz p => BZm_of_nat (nat_to_B p.+1)
end.

Lemma BZ_of_Z_surjective x : intp x -> exists y, BZ_of_Z y = x.
Lemma BZ_of_Z_injective x y : BZ_of_Z x = BZ_of_Z y -> x = y.
Lemma BZ_of_gcd (n m: nat) :
  BZgcd (BZ_of_Z n) (BZ_of_Z m) = BZ_of_Z (gcdn n m).
Lemma BZ_of_coprime (n m: nat) :
  BZcoprime (BZ_of_Z n) (BZ_of_Z m) <-> (coprime n m).

4.   THE SET OF RATIONAL NUMBERS Q

  We define Q as the set of pairs (a, b), such that a ∈ Z, b ∈ Z∗+ , a and b being
coprime. The two quantities a and b are called the numerator and denominator,
and denoted N (x) and D(x). Define ψ(a, b) = (a/g, b/g) where g is the gcd of a
and b. If a ∈ Z and b ∈ Z∗+ , then ψ(a, b) ∈ Q. We have ψ(a, b) = ψ(a0 , b0 ) when
ab0 = a0 b.

Definition BQ := Zo (BZ \times BZps) (fun z => BZcoprime (Qnum z) (Qden z)).
Definition BQ_of_pair a b :=
   J (a %/z (BZgcd a b)) (b %/z (BZgcd a b)).
Lemma BQ_of_pair_prop4 a b:
  intp a -> inc b BZps -> inc (BQ_of_pair a b) BQ.
Lemma BQ_of_pair_prop5 a b c d:
  intp a -> inc b BZps -> intp c -> inc d BZps ->
   (a *z d = b *z c <-> BQ_of_pair a b = BQ_of_pair c d).

  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.

Definition BQle_aux x y := (Qnum x) *z (Qden y) <=z (Qden x) *z (Qnum y).
Definition BQ_le x y := [/\ ratp x, ratp y & BQle_aux x y].
Notation "x <=q y" := (BQ_le x y) (at level 60).
Lemma BQle_P x y: gle BQ_ordering x y <-> x <=q y.
Lemma BQor_tor: total_order BQ_ordering.

  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 Formalized Reasoning Vol. 9, No. 2, 2016.
                     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 η.

                                         Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
34      ·    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 6= −1 and is strictly increasing (on either side of the cut). It is an isomorphism
Q+ → ]0, 1[. Define g(z) by: if z < 0, then 1/(1 − z), otherwise z + 1. Both pieces
are strictly increasing, the image of the first piece is ]0, 1[, the image of the second
piece is [1, →[, so that g is an order isomorphism Q → Q+ .

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 2c , 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 cc , this is 2c since c is an infinite cardinal. Obviously, z 7→ az + b is an
order isomorphism when a > 0.
   Let f be an element of 2c ; it can be considered as a function N → {0, 1}, so that
we can define, by induction, g(n + 1) = g(n) + f (n) + 1, g(0) = 0. Obviously f 7→ 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 7→ 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 7→ h is obviously injective.

Lemma BQ_iso3 a b: inc a BQps -> inc b BQ ->
    order_isomorphism (Lf (fun z => a*q z +q b) BQ BQ)
      BQ_ordering BQ_ordering.
Lemma BQ_iso4 (E := Zo (permutations BQ)
       (fun f => order_isomorphism f BQ_ordering BQ_ordering)):
   cardinal E = \2c ^c aleph0.

  A consequence of η + η = η is that Q∗ and Q are order isomorphic (here Q∗ is
the disjoint union of Q∗− and Q∗+ , Q∗− is isomorphic to Q∗+ via x 7→ −1/x, so that
Q∗ is order-isomorphic to the ordinal sum of two copies Q). As mentioned above,
the number of order isomorphisms f : Q∗ → Q is the cardinal of R. This is not a
coincidence.
  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 ai = f (−1/(i + 1)) and bi = f (1/(i + 1)), indexed by i ∈ N. They are
Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
                      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, ai < bj , and the infimum of bi − ai is zero. Given adjacent
sequences, we can define two disjoint sets, A, the set of all x such that x < ai for
some i and B, the set of all x such that bi < 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 : Q∗ → Q. The idea is to imposef (−1/(i + 1)) = ai and
f (1/(i+1)) = bi . On the intervals [1/(n+2), 1/(n+1)] and [−1/(n+1), −1/(n+2)],
f has the form z 7→ αz + β, on the intervals ]←, −1] and [1, →[ it has the form
z 7→ z + β.

Lemma multiple_interpolation_prop3 f1 f2
   (Zb := Zo BQ (fun z => exists2 n, natp n & f1 n <q z))
   (Za := Zo BQ (fun z => exists2 n, natp n & z <q f2 n)):
  (forall n, natp n -> f1 (csucc n) <q f1 n) ->
  (forall n, natp n -> f2 n <q f2 (csucc n)) ->
  (disjoint Za Zb) -> (Za \cup Zb = BQ) ->
  exists2 g, order_isomorphism g
    (induced_order BQ_ordering (BQ -s1 \0q)) BQ_ordering &
   image_by_fun g BQps = Zb.

  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 : Q∗ → Q such that f (Q∗+ ) = B. 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 r0 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 ψ : E → F ; let h = g −1 ◦ ψ ◦ f , so that
ψ = g ◦ h ◦ f −1 . The objective is to construct by induction a bijection h : N → N
such that f (i) < f (j) is equivalent to g(h(i)) < g(h(j)). 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 I3 such that i 7→ f (σ(i)) is strictly increasing, and a
necessary condition for h is that i 7→ g(h(σ(i))) is also strictly increasing. Assume
for instance σ(0) = 2, σ(1) = 0 and σ(2) = 1. This means f (2) < f (0) < f (1) and
g(h(2)) < g(h(0)) < g(h(1)). Let k be the position of x = f (3) relative to f (0),
f (1) and f (2). So, k = 0 means x < f (2), k = 1 means f (2) < x < f (0), k = 2
                                          Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
36     ·     José Grimm

means f (0) < x < f (1) and k = 3 means f (1) < x. Let yi = g(h(i)); the position
of y = g(h(3)) relative to y0 , y1 and y2 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 < y2 < b < y0 < c < y2 < 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 7→ f (σ(i)) is strictly increasing;
the last defines s = Sk (σ) by s(i) = σ(i) for i < k, s(i) = σ(i − 1) for i > k, and
s(k) = n.

Definition EPperm_M s n:=
   inc s (perm_int n) /\
   forall i j, i<c j -> j <c n -> glt r1 (Vf f (Vf s i)) (Vf f (Vf s j)).

Definition EPperm_extend_aux n k s :=
  fun z => Yo (z <c k) (Vf s z) (Yo (z = k) n (Vf s (cpred z))).
Definition EPperm_extend n k s :=
  Lf (EPperm_extend_aux n k s) (csucc n) (csucc n).

   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 kC (s, n). For completeness kC (s, 0) = 0.

Definition EPperm_compat0 r h n k x :=
   [/\ k <=c n,
    (k = \0c -> glt r x (h \0c)),
    (k = n -> k <>\0c -> glt r (h (cpred n)) x) &
    (k <c n -> k <> \0c -> (glt r (h (cpred k)) x) /\ glt r x (h k))].
Definition EPperm_compat s n k :=
   EPperm_compat0 r1 (fun i => (Vf f (Vf s i))) n k (Vf f n).
Definition EPperm_next_index n s :=
  Yo (n= \0c) \0c (select (EPperm_compat s n) Nat).

  We define by induction a sequence (sn )n of permutations of In , satisfying the
conditions stated above, via sn+1 = Sk (sn ), where k = kC (sn , n). Note that s0 and
s1 are both defined to be the identity function on I0 and I1 respectively.

Definition EPperm_rec :=
   induction_term (fun n s =>
       (Yo (n = \0c) (identity \1c)
          (EPperm_extend n (EPperm_next_index n s) s))) empty_function.
Lemma EPperm_recs_mon n: natp n -> EPperm_M (EPperm_rec n) n.

  We assume here that we know the restriction h1 of our function to In . Let sn be
as above, k = kC (sn , n); define h(i) = g(h1 (sn (i))). 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 h1 is replaced by h2 that takes the same value, we
get the same result.
Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
                      Theory of Sets / From natural numbers to real numbers          ·     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(h1 ) the quantity defined above. By transfinite induction, we
define a function h, such that h(n) = v(hn ) where hn is the restriction of h to In .
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.

Definition EPpermi_next ph n (s:= EPperm_rec n)
   (h := fun i => Vf g (Vf ph (Vf s i)))
   (k := (EPperm_next_index n s)) :=
  Yo (n = \0c) \0c (EPpermi_fct h n k).
Definition EPfun_aux :=
  transfinite_defined Nat_order (fun u => (EPpermi_next u (source u))).

   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 k1 such that q is the position of f (k1 )
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(k1 ) = n. Consider what happens when m is incremented. Let
k = kC (sm , m). If k = k1 , 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 k1 is left unchanged (the proof of this fact required 100 lines of script). We
cannot always be in this situation, since m < k1 (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.

Lemma Cantor_eta_pr r1 r2:
  eta_like r1 -> eta_like r2 -> r1 \Is r2.

4.2   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 [Ste58] and independently by
                                          Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
38      ·    José Grimm

Achille Brocot in 1861. If sn 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 [Gri14] for details), then the following
conditions hold: sk and sk+1 are coprime, and every rational number is uniquely a
quotient sk /sk+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 [Niq07, NB04].
  The sequence was rediscovered in 1976 by Dijkstra, under the name “fusc”
[Dij76a, Dij76b], with the following definition:
                         s1 = 1,     s2n = sn ,        s2n+1 = sn + sn+1 .         (4)
In the first paper Dijkstra writes: if f1 = fusc(n1 ) and f2 = fusc(n2 ), “if there
exists an N such that n1 + n2 = 2N , then f1 and f2 are relatively prime” and “if
f1 and f2 are relatively prime, then there exists an n1 , an n2 , and an N such that
n1 + n2 = 2N . 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 [Gri14]; we show the definition and the two claims of
Dijkstra.

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

     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 = 100112 , r(19) = 110012 = 25 and i(19) = 111012 = 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 · 24 ). From r(2k + 1) = 2log2 (k) + r(k), it follows the magic formula
                      r(n − 1) + i(r(n)) = 2log2 n           (n > 1, n odd).       (6)

  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 0 such that s(k) = s(k 0 + 1) and s(k + 1) = s(k 0 ); moreover
k + k 0 is odd.
Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
                      Theory of Sets / From natural numbers to real numbers          ·     39

   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.
  Let’s consider the following context:

Section Dijkstra.
Variable s: nat -> nat.

Definition Dijkstra_prop1:= forall n m p,
  n + m = 2^p -> coprime (s n) (s m).
Definition Dijkstra_prop2 := forall a b,
  coprime a b -> exists n m p, [/\ n + m = 2^p, a = s n & b = s m].
Definition Dijkstra_prop1bis :=
  forall k, coprime (s k) (s k.+1).
Definition Dijkstra_prop2bis := forall a b,
  coprime a b.+1 -> exists k, a = s k /\ b.+1 = s k.+1.

Hypothesis DH_FR: forall n, s (base2rev n) = s n.
Hypothesis DH_BI: forall n, s (bin_invert n) = s n.
Hypothesis DH_1: s 1 = 1.

   The key relation of the proofs is the following: assume n + m = 2p , n ≤ m and m
odd. Take m0 = r(i(m)); the magic relation says n = r(m0 − 1). So s(m) = s(m0 )
and s(n) = s(m0 − 1). Assumption DH_FR says s(2k) = s(k) (so that we can get
rid of the condition m odd) and DH_BI implies the palindrome condition, and its
consequence. Hence, there is m00 such that s(m) = s(m00 − 1) and s(n) = s(m00 ), so
that we can get rid of the condition n ≤ m. [size of the proof: 200 lines].

Lemma DH_prop1_from_bis: Dijkstra_prop1bis -> Dijkstra_prop1.
Lemma DH_prop2_from_bis: s 0 = 0 -> Dijkstra_prop2bis -> Dijkstra_prop2.
Lemma DH_prop1_to_bis: Dijkstra_prop1 -> Dijkstra_prop1bis.
Lemma DH_prop2_to_bis: s 0 = 0 -> Dijkstra_prop2 -> Dijkstra_prop2bis.
End Dijkstra.

   The Gaia definition is by transfinite induction: s(n) = V (sn ), where sn 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 sn 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 s0 = 0
causes no harm.

Definition fusc_next F n:=
  Yo (n = \0c) \0c (Yo (n = \1c) \1c (Yo (evenp n) (Vf F (chalf n))
   ((Vf F (chalf n)) +c (Vf F (csucc (chalf n)))))).

Definition fusc :=
  Vf (transfinite_defined Nat_order (fun u => (fusc_next u (source u)))).
                                          Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
40      ·      José Grimm

     Let xn = sn /sn+1 , this is the solution of:
                        1         1     1
            x2n =            (or     =    + 1),            x2n+1 = xn + 1   x0 = 0.   (7)
                    1 + 1/xn     x2n   xn
The function n 7→ xn is a bijection N → Q+ . First note that, by induction, the two
quantities sn and sn+1 are coprime. Let’s show (by induction) that the function is
injective. Assume xn = xm . Then n and m have the same parity (since x2k < 1
and x2k+1 ≥ 1). Assume for instance n = 2p and m = 2q. We have sp = sq and
sp + sp+1 = sq + sq+1 , thus sp+1 = sq+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 xk .
If x ≥ 1, then (p − q)/q = xn for some n, so that x = x2n+1 ; if 0 < x < 1, then
(q − p)/p = xn for some n, so that x = x2n ; 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 xn and xn+1 .
                                                                 1
                         F (xn ) = xn+1 ,        F (x) =                .             (8)
                                                           1 + 2bxc − x
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 (sn )n>0 as an infinite array, by considering Aij =
s2i +j . Thus row i is formed of values with index beween 2i and 2i+1 . A priori,
2i+1 is excluded, but recall that sn = 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 Ai+1,j = Ai,j + sj , or s2p+j = sp+j + sj
(whenever p is a power of two).

Lemma fusc_palindrome n a b (p := \2c ^c n): natp n ->
   p <=c a -> a <=c cdouble p -> p <=c b -> b <=c cdouble p ->
   a +c b = \3c *c p -> fusc a = fusc b.
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 ≤ 2n implies sk ≤ Fn+1 is rather obvious by induction on n: write s2m+1 =
sm + sm+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 sm = Fn
and sm+1 = Fn+1 , thus s2m+1 = Fn+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 cn+2 = cn+1 + 2cn . There is an
explicit solution cn = (4.2n − (−1)n )/3.

Definition Fib_fusc_rec :=
 induction_term (fun _ v => (J (csucc (cdouble (Q v))) (P v +c Q v)))
Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
                       Theory of Sets / From natural numbers to real numbers          ·     41

   (J \0c \0c).
Definition Fib_fusc n := P ( Fib_fusc_rec n).

Lemma fusc_bound1 n k: natp n -> k <=c \2c ^c n -> fusc k <=c Fib (csucc n).
Lemma Fib_fusc_val n: natp n -> (fusc (Fib_fusc n)) = Fib n.
Lemma Fib_fusc_bound n (p := \2c ^c n) (v := Fib_fusc (csucc (csucc n))):
   natp n -> (p <=c v /\ v <=c (cdouble p)).

   We have shown above   Pthat every integer n has a unique expansion to base 2, i.e.,
can be written as n = i<k ai 2i , with ai < 2, and ak−1 is non-zero. What happens
if ai < 2 is replaced by ai ≤ 2? The relation ak−1 non-zero says n ≥ 2k−1 , thus
k < n. Thus the sequence (ai )i<k belongs to some finite set Xn , whose cardinal is
sn+1 . We have shown the same property in pure ssreflect; the difficulty is the
following: we can only compute the cardinal of a subset Xn of a finite type T . We
cannot say: Xn is a subset of the set of functional graphs whose domain is a subset
of N with values in I3 (the Gaia definition), nor that Xn is a subset of the set of
sequences of length ≤ log2 n with values in I3 , because this finite set is not defined
in ssreflect (although defining it should not be too complicated). For this reason,
we replace the condition ak−1 non-zero by: the sequence has a fixed length. So, Xn
is a subset of the set of sequences of length k with values in I3 . Now Xn depends on
k, say becomes Xn,k but as explained above, if n has two representations of length
k1 and k2 , then the digits, starting with max(k1 , k2 ), are zero (a non-zero digit is
at position ≤ log2 n). As a consequence, if k ≥ log2 n, the cardinal of Xn,k becomes
independent of k. The pure ssreflect case is the following:

Fixpoint wbase2 (l: seq ’I_3) :=
  if l is a :: l’ then a + (wbase2 l’).*2 else 0.
Definition card_wbase2’ k n := #|[set t :k.-tuple ’I_3 | wbase2 t == n ]|.
Definition card_wbase2 n := card_wbase2’ (log2 n) n.
Lemma card_wbase2_val n: card_wbase2 n = fusc n.+1.

   Defining Xn and its cardinal C(n) in Gaia is a bit easier. In both cases, we
reason as follows. Consider a ∈ Xn , and let b be the sequence with the first
element removed. Then n = a0 + 2m and b ∈ Xm . If n is odd, then a0 = 1; it
follows that C(2m + 1) = C(m). On the other hand, if n is even, then a0 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).

  We consider here three sums where the index ranges beween 2n and 2n+1 − 1:
      X                X                     X
          si = 3n ,        1/(si si+1 ) = 1,     si /si+1 = (3 · 2n − 1)/2. (9)
         i                 i                         i

Let wi be the generic term of the sum. In the first case, wi is an integer and the
sum is over the interval [2n , 2n+1 [ (below is a sum over ‘Nintc n’, this is the
                                                                              P interval
[0, n]). In the two other cases, wi  is a rational number,  and we compute      i<p wp+i ,
where p = 2n and p is defined
                     P
                            P         by  induction over p.  There is no  generic sum in
Gaia, so the properties of      used here are proved only for Q.
                                           Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
42     ·     José Grimm

                                               P               P         P
   In the first case, wi = si . Write Tn =P wi as     P Tn =     w2i +      w2i+1 . The
first sum is Tn−1 , and the second sum is       wi + wi+1 = 2Tn−1 ; so Tn = 3Tn−1
hence Tn = 3n . In the second case, wi = 1/(si si+1 ). The sum of the i first terms
is si /sp+i provided i ≤ q, (where p = 2n , q = p/2). Since q is a power of two,
the partial sum up to q is sq /s3q = 1/2. The palindrome condition says that the
other part has the same sum, so that Tn = 1. We finally assume wi = si /si+1 . As
previously, we separate theP  cases, where i is even, and the P
                                                              case i is odd. Let P
                                                                                 a = si ,
b = si+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    Pcondition 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).

Definition fsimpl_sum p i :=
  qsum(fun j => BQinv (BQ_of_nat (fusc (p +c j) *c fusc (p +c (csucc j))))) i.

Lemma csum_fusc_row n: natp n ->
  csumb (interval_co Nat_order (\2c ^c n) (\2c ^c (csucc n))) fusc
  = \3c ^c n.
Lemma fusc_sum_simpl n (p := \2c ^c n):
  natp n -> fsimpl_sum p p = \1q.
Lemma qsum_fusc n (p := \2c ^c n) : natp n ->
 qsum (fun i => fusc_quo (p +c i)) p =
   BQhalf (BQ_of_nat (cpred (\3c *c p))).

  Let’s notice the following remarkable result. We consider the quantities ji 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 sn+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).

Lemma sum_diag_pascal n: natp n ->
  csumb (Nintc n) (fun k => binom (n -c k) k) = Fib (csucc n).
Definition sum_diag_pascal2 n :=
  csumb (Nintc n) (fun k => (binom (n -c k) k) %%c \2c).
Lemma sum_diag_pascal_prop n: natp n ->
   (sum_diag_pascal2 n) = fusc (csucc n).

5.    THE SET OF REAL NUMBERS

5.1   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

Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
                      Theory of Sets / From natural numbers to real numbers          ·     43

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, repre-
sented 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
Cx and Cx0 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 Cy0 ; we shall identify this interval with
Cy . This means that we shall only consider cuts where B has no least element; if
B has an infimum, it is of the form Cx , and is called a rational cut; otherwise, its
complement has no supremum and B is called an irrational cut.

Definition real_dedekind B :=
   [/\ sub B BQ, nonempty B, B <> BQ,
      (forall x y, inc x B -> x <q y -> inc y B) &
      (forall x, inc x B -> exists2 y, inc y B & y <q x)].
Definition irrationalp B := real_dedekind B /\
  (forall x, inc x (BQ -s B) -> exists2 y, inc y (BQ -s B) & x<q y).
Definition rationalp x := real_dedekind x /\ ~ (irrationalp x).
Definition BR_of_Q x := Zo BQ (fun z => x <q z).

  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 x such that bi < x for
some i, so is the union of the intervals ]bi , →[. Some authors assume the sequences
monotone instead of strictly monotone. There are two cases: if the sequence (bi )i is
not eventually constant, we can extract a strictly decreasing sequence that defines
the same cut. On the other hand, if bi = b for large i, then B is the interval ]b, →[,
the cut is rational, and we may replace the sequence by i 7→ b + 1/(i + 1) which is
a strictly decreasing sequence that gives the same cut.

Definition BQpair_aux C    :=
   [/\ fgraph C, domain    C = Nat,
       forall n, natp n    -> inc (Vg C n) (BQ \times BQ),
       forall n, natp n    -> P (Vg C n) <q P (Vg C (csucc n))&
       forall n, natp n    -> Q (Vg C (csucc n)) <q Q (Vg C n)].

Definition BQpair_aux2a C :=
   forall n, natp n -> P (Vg C n) <q Q (Vg C n).
Definition BQpair_aux2b C :=
   forall n m, natp n -> natp m -> P (Vg C n) <q Q (Vg C m).
Definition BQpair C := BQpair_aux C /\ BQpair_aux2b C.

Definition BQpairL   C :=
   Zo BQ (fun x =>   exists2 n, natp n & x <q P (Vg C n)).
Definition BQpairR   C :=
   Zo BQ (fun x =>   exists2 n, natp n & Q (Vg C n) <q x).

  Let (A, B) be the cut associated to the pair of sequences (a, b). If u and v are
                                          Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
44     ·     José Grimm

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 ≤ bi − ai . This last case contradicts the condition that the infimum
of bi − ai is zero. So either A ∪ B is Q (and B is irrational) or it is Q minus a
singleton x (and B = Cx ). The converse holds: if x is a real number, there is a
pair of adjacent sequences such that B = x; if x is rational, ai = x − 1/(i + 1),
bi = x + 1/(i + 1) 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].

Definition BQpair_aux3 C :=
   singletonp (BQ -s ((BQpairL C \cup BQpairR C))).

Lemma BQpair_irrational3 x: irrationalp x ->
  exists C, [/\ BQpairR C = x, BQpair C & BQpairL C \cup BQpairR C = BQ].
Lemma BQpair_rational2 x: ratp x ->
  exists C, [/\ BQpairR C = BR_of_Q x, BQpair C & BQpair_aux3 C].

   Note. Let f be a function N → {0, 1} and an = i≤n fi /3i , and bn = an + 1/3n .
                                                     P
Let B be, as above, the set of all t such that bi < t for at least one i. One can show
that bi ∈ B and ai 6∈ B (the sequence n 7→ an + (1/3n )/2 is decreasing). It follows
that B is a Dedekind cut and f 7→ B is injective. Hence card(R) = 2ℵ0 .
                       √                                                            √
   We show here: if 2 (denoted B) is the set of x such that 2 < x2 , then 2
is irrational in the sense given above. Firstly x2 = 2 has no solution since if
x = a/b where a and b are coprime, we have x2 = a2 /b2 where a2 and b2 are
coprime. We get a2 = 2 and b2 = 1, absurd. Secondly, B has no infimum. Since
(x − )2 − 2 ≥ x2 − 2 − 2x, whenever x > 0, it is possible to choose  such that
x −  ∈ B. If we choose  by x2 − 2 − 2x = 0 we are led to: if f (x) = (x2 + 2)/(2x),
then x ∈ B implies f (x) ≤ x and f (x) ∈ B. Note that f (x) = x says x2 = 2, which
is impossible. Thirdly, the complement of B has no supremum; it suffices to show
that the set A0 of all x > 0 such that x2 < 2 has no supremum. Our proof is as
follows. Take x = a/b in A0 and y = (a+1/4a)/b; we have x < y and (by)2 ≤ a2 +1;
since a is an integer, a2 < 2b2 says a2 + 1 ≤ 2b2 , so that we get y 2 < 2.
  Notes. Let g(x) = (f (x) + x)/2. If x is large enough, x ∈ A0 says g(x) ∈ A0 and
x ≤√g(x). The functions f and g can be used to create a pair of adjacent sequences
for 2. Since A0 is the set of all 2/x for x in B, A has a supremum if and only if
B has an infimum; the equivalent of f√is h(t)
                                            √ = 4t/(2
                                                   √ +   t2 ). Obviously, t ≤ h(t)√is
equivalent to t ≤ 2. Moreover h(t) = 2 − 2(t − 2) /(t2 + 2), so that h(t) ≤ 2
               2                                       2

(of course, this formula holds on R, but not on Q).

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

5.2   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

Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
                      Theory of Sets / From natural numbers to real numbers          ·     45

supremum or an infimum (intersection and union; note that the intersection could
be of the form Cx0 , case where Cx 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
y in x such that y −  is not in x. It implies that Q is dense in R (if x ∈ R,  > 0,
there is y in Q such that |y − x| < ).

Definition BR := Zo (powerset BQ) real_dedekind.
Definition BR_zero := BR_of_Q \0q.
Notation "\0r" := BR_zero.
Definition BRp := Zo BR (fun z => sub z BQp).

Definition BR_order := opp_order (sub_order BR).
Definition BR_le x y := [/\ realp x, realp y & sub y x].
Definition BR_lt x y := BR_le x y /\ x <> y.

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
                                                             0
complement of x. If y is rational, and x = Cy , 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).

Definition BRinv x (aux:= fun z => BQps -s fun_image z BQinv) :=
   Yo (rationalp x)
   (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):
                                          Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
46     ·     José Grimm

   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 n2 ≤ abd2 < (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.

5.3   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 |xn − 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 |xn − xm | < . If a limit exists it
is unique and the sequence is Cauchy.

Definition BR_seq x := [/\ fgraph x, domain x = Nat & sub (range x) BR].
Definition CauchyR x := BR_seq x /\
      forall e, inc e BQps -> exists2 N, natp N &
         forall n m, natp n -> natp m -> N <=c n -> N <=c m ->
            BRabs ((Vg x n) -r (Vg x m)) <r (BR_of_Q e).
Definition limitR x v:=
   forall e, inc e BQps -> exists2 N, natp N &
   forall n, natp n -> N <=c n -> BRabs ((Vg x n) -r v) <r (BR_of_Q e).

Lemma limitR_unique x v1 v2: BR_seq x -> realp v1 -> realp v2 ->
   limitR x v1 -> limitR x v2 -> v1 = v2.
Lemma CauchyR_when_limit x:
  BR_seq x -> (exists2 y, realp y & limitR x y) -> CauchyR x.

   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 , yn < 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 |xn − yn | < 1/(n + 1). This sequence is then Cauchy, and its
limit is the limit of x. [The proof requires 400 lines of script].

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


Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
                      Theory of Sets / From natural numbers to real numbers          ·     47

5.4   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 con-
tinuous (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 7→ x2 is continuous.

Definition BR_near x e y:= realp y /\ BRabs (x -r y) <=r e.
Definition continuous_at f x:=
   forall e, inc e BRps -> exists2 d, inc d BRps &
   forall y, BR_near x d y -> BR_near (f x) e (f y).
Definition continuous f:= forall x, realp x -> continuous_at f x.

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

Definition Bolzano_hyp f x    y:=
    [/\ continuous_right f    x, continuous_left f y &
    (forall z, x <r z -> z    <r y -> continuous_at f z)].
Lemma Bolzano2 f x y v: x     <=r y -> Bolzano_hyp f x y ->
    (BR_between v (f x) (f    y)) ->
    exists2 z, (x <=r z /\    z <=r y) & f z = v.

  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.

   Assume that f is a function such that a ≤ t implies a ≤ f (t) ≤ t. Fix x0 ≥ a and
define xn by xn+1 = f (xn ). Then the sequence (xn )n∈N is decreasing hence has a
limit x (namely inf i (xi )) such that a ≤ x. If f is continuous at x, then f (x) = x.
                                          Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
48     ·     José Grimm

[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 ≤ x0 ≤ 2, and a = 0 otherwise.]

Lemma decreasing_bounded_limit a xn (x := infimum BR_order (range xn)):
  BR_seq xn ->
  (forall n, natp n -> a <=r (Vg xn n)) ->
  (forall n, natp n -> Vg xn (csucc n) <=r Vg xn n) ->
  (a <=r x /\ limitR xn x).
Lemma decreasing_limit_bounded_fix a x0 f
  (seq:= induction_defined f x0) (xn := Lg Nat (Vf seq))
  (x := infimum BR_order (range xn)):
  (forall x, a <=r x -> a <=r f x /\ f x <=r x) -> a <=r x0 ->
  (continuous_at f x) ->
  [/\ a <=r x, f x = x & limitR xn x].
                                                                        √
   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 x2 = a. Let f (x) = (x2 + a)/(2x).
Let B be the set of all positive x such that x2 ≥ a. We have x−f (x) = (x2 −a)/(2x),
so that, if x ∈ B we have f (x) ≤ x. We have f (x)2 − a = (x2 − a)2 /(4x2 ), so that,
if x > 0, then f (x) ∈ B. If xn+1 = f (xn ), where x0 is big enough (say ≥ 1 + a)
then xn 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 x2 = a.
   Let now g(t) = (f (t) + t)/2 and yn+1 = g(yn ), Let A be the set of all positive
t such that a/9 ≤ t2 ≤ 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
y0 ∈ A, the sequence (yn )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.]

Lemma square_root_cv1 a b (f := fun z => (BRsquare       z +r a) /r (\2r *r z))
  (seq:= induction_defined f b) (xn := Lg Nat (Vf        seq))
  (x := infimum BR_order (range xn)):
  inc a BRp -> \1r +r a <=r b ->
  [/\ inc x BRp, limitR xn x & BRsquare x = a].
Lemma square_root_cv3 a b (f := fun z => (BRsquare       z +r a) /r (\2r *r z))
  (g := fun z => BRhalf ((f z) +r z)) (s := BRsqrt       a)
  (seq:= induction_defined g b) (xn := Lg Nat (Vf        seq))
  (x := supremum BR_order (range xn)):
  inc a BRp -> (s /r \3r) <=r b -> b <=r s ->
  [/\ inc x BRp, limitR xn x & x = s].




Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
                       Theory of Sets / From natural numbers to real numbers          ·     49

6.   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://www-
sop.inria.fr/marelle/gaia.
   In [Gri10] 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, multiplica-
tion, 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 xi .
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 [Gri14]. Some comments:
                                           Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
50     ·     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, insteadPof a functional graph on In ; for
 instance, the expansion to base b is a list a and     ai bi is defined by the Horner
 Scheme; the second relation of (2), namely En+1 (a) = a0 + bEn (a0 ) 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 In → Im . In each case, the objective
 is to compute cn = card(En ) for some finite set En . 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 En ⊂ T . In the
 first two cases, one can take T = In ; but this choice makes proofs by induction
 impossible; so one takes T = Im for some m ≥ n, this gives a cardinal cn,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 [Bou68] ask to prove some formulas   P on Z by using
 different ways to compute the cardinal of a same set; for instance k (−1)k nk = 0
 says that there are as many subsets of In 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(0). 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,

Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
                      Theory of Sets / From natural numbers to real numbers          ·     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.


ACKNOWLEDGMENT

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

References
[BLM14]      Sylvie Boldo, Catherine Lelay, and Guillaume Melquiond. Formal-
             ization of Real Analysis: A Survey of Proof Assistants and Li-
             braries. Mathematical Structures in Computer Science, page 38, 2014.
             https://hal.inria.fr/hal-00806920.
[Bou68]      N. Bourbaki. Elements of Mathematics, Theory of Sets. Springer, 1968.
[Bou70]      N. Bourbaki. Éléments de mathématiques, Théorie des ensembles. Dif-
             fusion CCLS, 1970.
[Bou89a]     N. Bourbaki. Elements of Mathematics, Algebra I. Springer, 1989.
[Bou89b]     N. Bourbaki. Elements of Mathematics, General Topology. Springer,
             1989. Translation of the 1966 French edition.
[Can97]      Georg Cantor. Contributions to the Founding of the Theory of Transfi-
             nite Numbers. Dover Publications Inc, 1897. Trans. P. Jourdain, 1955.

                                          Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
52     ·     José Grimm

[Coh12]  Cyril Cohen. Construction of real algebraic numbers in Coq. In Lennart
         Beringer and Amy Felty, editors, ITP - 3rd International Conference on
         Interactive Theorem Proving - 2012, Princeton, United States, August
         2012. Springer. https://hal.inria.fr/hal-00671809.
[Dij76a] Edsger W. Dijkstra. An exercise for Dr. R.M.Burstall. Available at
         http://www.cs.utexas.edu/users/EWD/ewd05xx/EWD570.PDF, May
         1976.
[Dij76b] Edsger W. Dijkstra. More about the function “fusc” (a sequel to
         EWD570). Available at
         http://www.cs.utexas.edu/users/EWD/ewd05xx/EWD578.PDF, Au-
         gust 1976.
[GGMR09] François Garillot, Georges Gonthier, Assia Mahboubi, and Laurence
         Rideau. Packaging mathematical structures. In Theorem Proving in
         Higher Order Logics, Lecture Notes in Computer Science 5674, 2009.
         https://hal.inria.fr/inria-00368403.
[GM10]   Georges Gonthier and Assia Mahboubi. An introduction to small scale
         reflection in Coq. Journal of Formalized Reasoning, 3(2):95–152, 2010.
         https://jfr.unibo.it/article/view/1979.
[Gri09]  José Grimm. Implementation of Bourbaki’s Elements of Mathematics
         in Coq: Part Two; Ordered Sets, Cardinals, Integers. Research Report
         RR-7150, INRIA, 2009. http://hal.inria.fr/inria-00440786/en/.
[Gri10]  José Grimm. Implementation of Bourbaki’s Elements of Mathematics
         in Coq, part one theory of sets. Journal of Formalized Reasoning,
         3(1):79–126, 2010.
[Gri14]  José Grimm. Fibonacci numbers and the Stern-Brocot tree in Coq.
         Research Report RR-8654, Inria Sophia Antipolis, December 2014.
[NB04]   Milad Niqui and Yves Bertot. Qarith: Coq formalisation of lazy rational
         arithmetic. In Stefano Berardi, Mario Coppo, and Ferruccio Damiani,
         editors, Types for Proofs and Programs, volume 3085 of Lecture Notes
         in Computer Science, pages 309–323. Springer Berlin Heidelberg, 2004.
[Niq07]  Milad Niqui. Exact arithmetic on the Stern-Brocot tree. Journal of
         Discrete Algorithms, 5(2), 2007.
[Sim04a] Carlos Simpson. Computer theorem proving in math. Technical report,
         CNRS, Laboratoire J.A. Dieudonne, 2004. arXiv:math/0311260v2.
[Sim04b] Carlos Simpson. Set-theorical mathematics in Coq. Technical report,
         CNRS, Laboratoire J.A. Dieudonne, 2004. arXiv:math/0402336v1.
[Ste58]  Moritz Stern. Ueber eine zahlentheorische Funktion. Journal für die
         reine und angewandte Mathematik, 55:193–220, 1858.




Journal of Formalized Reasoning Vol. 9, No. 2, 2016.
