\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 define the rationals. The type
\li{rat} is defined as a subtype of \hbox{\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.

\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} \\[-\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{Final Exhortation}

We have now reached the end of this course. You now know fundamental theory and
techniques in interactive theorem proving as well as some application areas.
Although we used Lean, your skills should help you with other systems,
especially those based on simple or dependent type theory. You should also be
able to read many if not most scientific papers in the area.

Even if you do not choose to pursue a career in theorem proving, the authors
hope you will bring proof assistants with you and use them when it makes sense,
either because of their high trustworthiness or because of their convenience for
keeping track of complex proof goals.

If you continue using Lean, the natural next step would be to familiarize
yourself with \li{mathlib} and its documentation. If you use Lean outside a
class context, you will often find yourself looking up lemmas and tactics. The
\li{#find} command will surely be useful.%
\footnote{\url{https://leanprover-community.github.io/mathlib_docs/commands.html##find}}
And the Lean Zulip chat%
\footnote{\url{https://leanprover.zulipchat.com/}}
is the meeting place of Lean users.

\section{Summary of New Lean Constructs}

\begingroup
\summarysize

\subsection*{Command}

\noindent
\begin{xltabular}{\textwidth}{@{}p{9em}X@{}}
\lic|#find| & looks up a lemma by pattern matching \\
\end{xltabular}

\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
