\chapter{Rational and Real Numbers}
\label{chap:rational-and-real-numbers}
In the previous chapters, we have seen how the natural numbers \li{ℕ} can be
defined as an inductive type and how the integers \li{ℤ} can be defined as a
quotient over \li{ℕ} \li{×} \li{ℕ}. In this chapter, we present the
construction of the rational numbers \li{ℚ} and the real numbers \li{ℝ}. The
tools used for these constructions are the same as for \li{ℕ} and \li{ℤ}:\
inductive types and quotients.

A general recipe to construct new types with specific properties is as follows:
%
\begin{enumerate}
\item Create a new type that can represent all elements, but not necessarily in   a unique manner.

\item Quotient this representation, equating elements that should be considered
  equal.

\item Define operators on the quotient type by lifting functions from the base
  type, and prove that they respect the quotient relation.
\end{enumerate}
%
We have used this approach before to construct \li{ℤ}. It can be used to
construct \li{ℚ} and \li{ℝ} as well.

\section{Rational Numbers}
\label{sec:rational-numbers}

A rational number is a number that can be expressed as a fraction
\textit{n}$/$\textit{d} of integers \textit{n} and \textit{d} $\not=$ 0:
%
\lstinputlisting[linerange=fraction-q]{../lean/love13_rational_and_real_numbers_demo_master.lean}
%
 The number \textit{n} is called the numerator, and the number \textit{d} is
called the denominator. The representation of a rational number as a fraction
is not unique. For example, the rationals 1$/$2, 2$/$4, and $-$1$/-$2 are all
equal. This representation as a fraction will serve as the base type from which
we will derive a quotient.

Two fractions \textit{n}$_\text{1}/$\textit{d}$_\text{1}$ and
\textit{n}$_\text{2}/$\textit{d}$_\text{2}$ represent the same rational
number if the ratio between numerator and denominator are the same, meaning
that \textit{n}$_\text{1}$ $*$ \textit{d}$_\text{2}$ $=$
\textit{n}$_\text{2}$ $*$ \textit{d}$_\text{1}$.
To construct the quotient of the type \li{fraction} with respect to this
relation, we show that the relation is an equivalence relation. This is
achieved by declaring \li{fraction} an instance of the \li{setoid} type class:
%
\lstinputlisting[linerange=fraction_setoid-q]{../lean/love13_rational_and_real_numbers_demo_master.lean}
%
Then we can define \li{ℚ} as the quotient over this setoid. To avoid a name
clash, we call it \li{myℚ}:
%
\lstinputlisting[linerange=rat-q]{../lean/love13_rational_and_real_numbers_demo_master.lean}
%
To define zero, one, addition, multiplication, and other operations, we first
define them on the \li{fraction} type. To add two fractions, we convert the
fractions to a common denominator and add the numerators. The easiest common
denominator to use is simply the product of the two denominators:
%
\lstinputlisting[linerange=has_add_fraction-q]{../lean/love13_rational_and_real_numbers_demo_master.lean}
%
We register these operations directly as instances of the syntactic type
classes such as \li{has_add} to be able to use convenient notation such as
\li{+} on \li{fraction}. Similarly, we define zero as \li{0 := 0 / 1}, one as
\li{1 := 1 / 1}, and multiplication as the pairwise multiplication of
numerators and denominators.

To lift these operations to \li{myℚ}, we first need to show that they respect the relation \li{≈}:
%
\lstinputlisting[linerange=setoid_fraction-q]{../lean/love13_rational_and_real_numbers_demo_master.lean}
%
Then we can use \li{quotient.lift_on} and \li{quotient.lift_on₂} to define the
operations on \li{myℚ}, and we can instantiate the relevant the syntactic type
classes:
%
\lstinputlisting[linerange=has_add_rat-q]{../lean/love13_rational_and_real_numbers_demo_master.lean}
%
From here, we can proceed and prove all the properties needed to make \li{myℚ}
an instance of \li{field} or, if we are more ambitious,
\li{discrete_linear_ordered_field}.

\subsection{Alternative Definitions of the Rational Numbers}

We will discuss two more approaches to construct the rational numbers.

The first approach is the one used in \li{mathlib}. It is similar to the
approach described above, but adds an additional property
\li{cop : coprime num denom} to the structure, which states that that numerator
and denominator do not have a common divisor (except \li{1} and \li{-1}):
%
\begin{lstlisting}
structure rat :=
(num : ℤ)
(denom : ℕ)
(pos : 0 < denom)
(cop : coprime num denom)
\end{lstlisting}
%
On the positive side, no quotient construction is required, computation may be
more efficient, and more theorems are definitional equalities. A disadvantage
is that function definitions become more complicated.

A second alternative approach is to define all elements syntactically,
including the desired operations:
%
\begin{lstlisting}
inductive pre_rat : Type
| zero : pre_rat
| one : pre_rat
| add : pre_rat → pre_rat → pre_rat
| sub : pre_rat → pre_rat → pre_rat
| mul : pre_rat → pre_rat → pre_rat
| div : pre_rat → pre_rat → pre_rat
\end{lstlisting}
%
Then we define an equivalence relation and take its quotient to enforce congruence rules and the field axioms.
%
\begin{lstlisting}
inductive equiv : pre_rat → pre_rat → Prop
| add_congr {a b c d : pre_rat} :
    equiv a b → equiv c d → equiv (add a c) (add b d)
| add_assoc {a b c : pre_rat} :
    equiv (add a (add b c)) (add (add a b) c)
| zero_add {a : pre_rat} : equiv (add zero a) a
| add_comm {a b : pre_rat} : equiv (add a b) (add b a)
| etc : equiv sorry sorry

def rat : Type :=
quot equiv
\end{lstlisting}
%
The advantages are that this construction does not require \li{ℤ} and that it
is easy to declare as an instance of \li{field}. Most importantly, though, this
approach can be used for other algebraic constructions, such as free monoids
and free groups. A disadvantage is that the definition of orders and lemmas
about them become more complicated.

\section{Real Numbers}
\label{sec:real-numbers}

There are sequences of rational numbers that seem to converge because the
numbers in the sequence get closer and closer to each other, and yet do not
converge to a rational number. The sequence
\begin{align*}
    \textit{a}_\text{0} &= \text{1} \\
    \textit{a}_\text{1} &= \text{1.4} \\
    \textit{a}_\text{2} &= \text{1.41} \\
    \textit{a}_\text{3} &= \text{1.414} \\
    \textit{a}_\text{4} &= \text{1.4142} \\
    \textit{a}_\text{5} &= \text{1.41421} \\
    \textit{a}_\text{6} &= \text{1.414213} \\
    \textit{a}_\text{7} &= \text{1.4142135}\\
    \textit{a}_\text{8} &= \text{1.41421356} \\[-\jot]
	& \;\,\,\vdots
\end{align*}
where $\textit{a}_\textit{n}$ is the largest number with \textit{n} 
digits after the decimal point
such that $\textit{a}_\textit{n}^\text{2} < \text{2}$, is such a sequence. It
seems to converge because each $\textit{a}_\textit{n}$ is at most
$\text{10}^{-\textit{n}}$ away from any of the following numbers, but the limit
is $\sqrt{\text{2}}$, which is not a rational number.

In that sense, the rational numbers are incomplete, and the reals are their
\emph{completion}. To construct the reals, we need to fill in the gaps that are
revealed by these sequences that seem to converge, but do not.

Cauchy sequences capture the notion of a sequence that seems to converge. A
sequence $\textit{a}_\text{0}, \textit{a}_\text{1}, \dots$ is \emph{Cauchy} if
for any $\varepsilon > \text{0}$, there exists an $\textit{N} \in \mathbb{N}$
such that for all $\textit{m} \geq \textit{N}$, we have
$\left|\textit{a}_\textit{N} - \textit{a}_\textit{m} \right| < \varepsilon$. In
other words, no matter how small we choose $\varepsilon$, we can always find a
point in the sequence from which all following numbers do not deviate more
than~$\varepsilon$.

We formalize sequences of rational numbers as functions \li{f : ℕ → ℚ} and
denote the absolute value $\left|\phantom{\cdot} \right|$ by \li{abs}. This
yields the following Lean definition of Cauchy sequences:
%
\lstinputlisting[linerange=is_cau_seq-q]{../lean/love13_rational_and_real_numbers_demo_master.lean}
%
We define a type of Cauchy sequences as a subtype:
%
\lstinputlisting[linerange=cau_seq-q]{../lean/love13_rational_and_real_numbers_demo_master.lean}
%
It will be convenient to have an auxiliary function that extracts the actual sequence from a \li{cau_seq}:
%
\lstinputlisting[linerange=to_seq-q]{../lean/love13_rational_and_real_numbers_demo_master.lean}
%
The idea of this construction is to let the real numbers be represented by
Cauchy sequences. Each Cauchy sequence represents the real number that is its
limit; for example, the sequence $\textit{a}_\textit{n} = \text{1}/\textit{n}$
represents the real number 0, and the sequence 1, 1.4, 1.41, {\dots}\
represents the real number $\sqrt{\text{2}}$. Two different Cauchy sequences
can represent the same real number; for example, the sequence
$\textit{a}_\textit{n} = \text{1}/\textit{n}$ and the constant sequence
$\textit{b}_\textit{n} = \text{0}$ both represent $\text{0}$. Therefore, we
need to take the quotient over sequences representing the same real number.
Formally, two sequences represent the same real number when their difference
converges to zero:
%
\lstinputlisting[linerange=cau_seq_equiv-q]{../lean/love13_rational_and_real_numbers_demo_master.lean}
%
Using this \li{setoid} instance, we can now define the real numbers:
%
\lstinputlisting[linerange=real-q]{../lean/love13_rational_and_real_numbers_demo_master.lean}
%
Like for the rational numbers, we need to define zero, one, addition, multiplication, and other operators.
We define them on \li{cau_seq} first and lift them to \li{myℝ} afterwards.
For the constants \li{0} and \li{1}, we can define them simply as a constant sequence. Any constant sequence is a Cauchy sequence:
%
\lstinputlisting[linerange=const-q]{../lean/love13_rational_and_real_numbers_demo_master.lean}
%
We can declare \li{myℝ} instances of the syntactic type classes \li{has_zero} and \li{has_one} as follows:
%
\lstinputlisting[linerange=has_zero_my_real-q]{../lean/love13_rational_and_real_numbers_demo_master.lean}
%
Defining addition of real numbers requires a little more effort. We define
addition on Cauchy sequences by adding the elements of the sequence pairwise:
%
\lstinputlisting[linerange=cau_seq_has_add-q]{../lean/love13_rational_and_real_numbers_demo_master.lean}
%
This definition requires a proof that the result is a Cauchy sequence, given
that \li{f} and \li{g} are Cauchy sequences. We omit that proof here. Next, we
need to show that this addition is compatible with our equivalence relation:
%
\lstinputlisting[linerange=cau_seq_add_equiv_add-q]{../lean/love13_rational_and_real_numbers_demo_master.lean}
%
We will discuss this proof in a bit more detail. It has a similar flavor to the two proofs
we omitted above. To show that \li{f₁ + g₁ ≈ f₂ + g₂}, we are given an
\li{ε₀ > 0} and must prove that there exists an \li{N : ℕ} such that
%
\[\hbox{\li{∀m : ℕ, m ≥ N → abs ((f₁ + g₁).val m - (f₂ + g₂).val m) < ε₀}}\]
%
To obtain such an \li{N}, we use the facts \li{f₁ ≈ f₂} and \li{g₁ ≈ g₂}. The
fact \li{f₁ ≈ f₂} gives us for any \li{ε > 0} a number \li{Nf} such that
\li{abs (to_seq f₁ m - to_seq f₂ m) < ε} for all \li{m ≥ Nf}. The fact \li{g₁ ≈ g₂}
gives us a number \li{Ng} with a similar property. For the calculations to work
out in the end, we take the numbers \li{Nf} and \li{Ng} for \li{ε} \li{:=}
\li{ε₀ / 2}. Then we choose \li{N} to be the maximum of \li{Nf} and \li{Ng}, so
that we get the inequalities for any \li{m ≥ N}. The \li{calc} block
at the end of the proof establishes that
\li{abs (to_seq (f₁ + g₁)} \li{m} \li{- to_seq (f₂ + g₂) m) < ε₀} for all \li{m ≥ N}.

Using the lemma, we can then define addition on \li{myℝ}:
%
\lstinputlisting[linerange=has_add_my_real-q]{../lean/love13_rational_and_real_numbers_demo_master.lean}
%
Multiplication can be defined similarly.

% Unlike \li{ℚ}, \li{ℝ} is \emph{complete}—i.e., all Cauchy sequence on \li{ℝ} have a limit:

% \begin{lstlisting}
%     ∀f : ℕ → ℝ, cauchy f → ∃x, ∀ε > 0, ∃N, ∀m ≥ N, |f m - x| < ε
% \end{lstlisting}

\subsection{Alternative Definitions of the Real Numbers}

In \li{mathlib}, the construction of the real numbers is essentially as
described above. Only some definitions are stated in a more general fashion to
allow construction of other algebraic structures, such as the \textit{p}-adic
numbers.

Alternatively, the real numbers can be defined using Dedekind cuts.
Essentially, a number \li{r : ℝ} is then represented as \li${x : ℚ | x < r}$.

Another alternative definition of the reals is to define them using binary
sequences \li{ℕ → bool}. The elements of the sequence represent the digits of
the real number. This works particularly well if we only need the real numbers
in the interval $[0, 1]$. This construction does not require the rational
numbers.
