\chapter{Rational and Real Numbers}
\label{chap:rational-and-real-numbers}

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 review the construction of the rational numbers
\li{ℚ} and the real numbers \li{ℝ}. The tools used for these constructions are
inductive types, subtypes, and quotients.

This procedure can be followed to construct types with specific properties:
%
\begin{itemize}
\item[1.] Create a new type that is large enough to represent all elements, but
  not necessarily in a unique manner.

\item[2.] Take the quotient of this representation, equating elements as needed.

\item[3.] Define operators on the quotient type by lifting functions from the base
  type, and prove that they are compatible with the quotient relation.
\end{itemize}
%
We used this approach to construct the type \li{ℤ} in
Section~\ref{ssec:first-example-integers}. It can be used for
\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}, where \textit{d}
$\neq$ 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:
\textit{n}$_\text{1}$ $*$ \textit{d}$_\text{2}$ $=$
\textit{n}$_\text{2}$ $*$ \textit{d}$_\text{1}$.
To construct the quotient over 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=namespace_fraction-q]{../lean/love13_rational_and_real_numbers_demo_master.lean}
\betweenlistings
\lstinputlisting[linerange=fraction_setoid-q]{../lean/love13_rational_and_real_numbers_demo_master.lean}
\betweenlistings
\lstinputlisting[linerange=end_fraction-q]{../lean/love13_rational_and_real_numbers_demo_master.lean}
%
Then we can define the type of rationals as the quotient over this setoid:
%
\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{rat}, we must prove them compatible with~\li{≈}:
%
\lstinputlisting[linerange=namespace_fraction-q]{../lean/love13_rational_and_real_numbers_demo_master.lean}
\betweenlistings
\lstinputlisting[linerange=setoid_fraction-q]{../lean/love13_rational_and_real_numbers_demo_master.lean}
\betweenlistings
\lstinputlisting[linerange=end_fraction-q]{../lean/love13_rational_and_real_numbers_demo_master.lean}
%
(The \li{ac_refl} tactic is a variant of \li{refl} that reasons up to
associativity and commutativity, much like \li{cc}.) Then we can use
\li{quotient.lift}(\li{₂}) to define the \hbox{\li{rat}} operations, and we can
instantiate the relevant syntactic type classes, such as
%
\lstinputlisting[linerange=namespace_rat-q]{../lean/love13_rational_and_real_numbers_demo_master.lean}
\betweenlistings
\lstinputlisting[linerange=has_add_rat-q]{../lean/love13_rational_and_real_numbers_demo_master.lean}
\betweenlistings
\lstinputlisting[linerange=end_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{rat}
an instance of \li{field} or, if we are more ambitious,
\li{discrete_linear_ordered_field}.

\paragraph{Alternative Definitions of the Rational Numbers}

In \li{mathlib}, another approach is used to defined the rationals. The type
\li{rat} is defined as a subtype of \li{fraction}, with the requirement
that the denominator is positive and that the numerator and the denominator
are coprime (i.e., they have no common divisors except 1 and $-$1):
%
\lstinputlisting[linerange=alternative_1.rat_def-q]{../lean/love13_rational_and_real_numbers_demo_master.lean}
%
We discussed this general strategy in
Section~\ref{ssec:alternative-definitions-via-normalization-and-subtyping}.
In this way, no quotient is required, computation is more efficient, and more
properties are syntactic equalities up to computation. A disadvantage is that
function definitions become more complicated due to the need to normalize
fractions.

Another alternative is to define all elements syntactically, including the
desired operations:
%
\lstinputlisting[linerange=pre_rat_def-q]{../lean/love13_rational_and_real_numbers_demo_master.lean}
%
Then we define an equivalence relation and take its quotient to enforce
congruence rules and the field axioms:
%
\lstinputlisting[linerange=rat.rel-q]{../lean/love13_rational_and_real_numbers_demo_master.lean}
%
This construction does not require \li{ℤ} and that it can easily be registered
as a \li{field}. Moreover, the same approach can be used for other algebraic
constructions, such as free monoids and free groups. A drawback is that the
definition of orders and lemmas about them become more complicated.

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

Some sequences of rational numbers 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} \\[-\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}} \notin \mathbb{Q}$. 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 deviate by less
than~$\varepsilon$.

We formalize sequences of rational numbers as functions \li{f : ℕ → ℚ} and
denote the absolute value $\left|\phantom{x} \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}
%
Not every sequence is a Cauchy sequence:
%
\lstinputlisting[linerange=id_not_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=seq_of-q]{../lean/love13_rational_and_real_numbers_demo_master.lean}

The basic idea of the construction is to represent the real numbers 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. Two
sequences represent the same real number when their difference converges to
zero:
%
\lstinputlisting[linerange=namespace_cau_seq-q]{../lean/love13_rational_and_real_numbers_demo_master.lean}
\betweenlistings
\lstinputlisting[linerange=cau_seq_equiv-q]{../lean/love13_rational_and_real_numbers_demo_master.lean}
\betweenlistings
\lstinputlisting[linerange=end_cau_seq-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{real} afterwards. For the constants \li{0} and \li{1}, we can
define them simply as constant sequences. Any constant sequence is a Cauchy
sequence:
%
\lstinputlisting[linerange=namespace_cau_seq-q]{../lean/love13_rational_and_real_numbers_demo_master.lean}
\betweenlistings
\lstinputlisting[linerange=const-q]{../lean/love13_rational_and_real_numbers_demo_master.lean}
%
We can declare \li{real} instances of the syntactic type classes
\li{has_}\allowbreak\li{zero} and \li{has_one}:
%
\lstinputlisting[linerange=has_zero_real-q]{../lean/love13_rational_and_real_numbers_demo_master.lean}
%
Defining addition (and, similarly, multiplication) 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. It is omitted.

Next, we need to show that this addition is compatible with \li{≈}:
%
\lstinputlisting[linerange=cau_seq_add_equiv_add-q]{../lean/love13_rational_and_real_numbers_demo_master.lean}
\betweenlistings
\lstinputlisting[linerange=end_cau_seq-q]{../lean/love13_rational_and_real_numbers_demo_master.lean}
%
To prove that \li{f + g ≈ f' + g'}, we are given an \li{ε₀ > 0} and must show
that there exists a number \li{N} such that
%
\[\hbox{\tabletsmall\lic{∀m, m ≥ N → abs (subtype.val (f + g) m - subtype.val (f' + g') m) < ε₀}}\]
%
To obtain \li{N}, we use \li{f ≈ f'} and \li{g ≈ g'}. The
equivalence \li{f ≈ f'} gives us for any \li{ε > 0} a number \li{Nf} such that
\li{abs (seq_of f m - seq_of 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, for all \li{m ≥ N},
%
\[\hbox{\lic{abs (seq_of (f + g) m - seq_of (f' + g') m) < ε₀}}\]

Using this lemma, we can define addition on \li{real}:
%
\lstinputlisting[linerange=namespace_real-q]{../lean/love13_rational_and_real_numbers_demo_master.lean}
\betweenlistings
\lstinputlisting[linerange=has_add_real-q]{../lean/love13_rational_and_real_numbers_demo_master.lean}
\betweenlistings
\lstinputlisting[linerange=end_real-q]{../lean/love13_rational_and_real_numbers_demo_master.lean}

In summary, real numbers are defined as a quotient over Cauchy sequences, which
are in turn defined as a subtype of \li{ℕ → ℚ}.

\paragraph{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 \cite{lewis-2019}.

Alternatively, the real numbers can be defined using Dedekind cuts. A number
\li{r : ℝ} is then represented as the set of numbers \li{x : ℚ} such that
\li{x < r}. Another alternative, which does not depend on \li{ℚ}, is to define
\li{ℝ} using binary sequences \hbox{\li{ℕ → bool}.} The elements of the sequence
represent the number's digits. This works particularly well if we only need the
real interval $[0, 1]$.

\section{Summary of New Lean Constructs}

\begingroup
\summarysize

\subsection*{Tactic}

\noindent
\begin{xltabular}{\textwidth}{@{}p{9em}X@{}}
\li|ac_refl| & proves equalities \li|l = r| up to associativity and \hbox{commutativity} \\
\end{xltabular}

\endgroup
