\chapter{Logical Foundations of Mathematics}
\label{chap:logical-foundations-of-mathematics}

In this chapter, we dive deeper into the logical foundations of Lean. Most of
the features described here are especially relevant for defining mathematical
objects and proving theorems about them. For even more details, we refer to
Carneiro's MSc thesis \cite{carneiro-2019}.

\section{Universes}
\label{sec:universes}

In dependent type theory, not only all terms have a type, but also all types
have types themselves. We have already seen some occurrences of this principle.
The PAT principle tells us to view proofs as terms and propositions as types.
For example, the lemma
%
\[\hbox{\lic{@and.intro : ∀a b, a → b → a ∧ b}}\]
%
is really a term \li{@and.intro} of type \li{∀a b, a → b → a ∧ b}, which in
turn has a type:
%
\[\hbox{\lic{∀a b, a → b → a ∧ b : Prop}}\]
%
What is the type of \li{Prop} then? \li{Prop} has the same type as virtually
all other types we have constructed so far:
%
\[\text{\lic|Prop : Type|}\]
%
What is the type of \li{Type}? The simplest solution would be to let
\li{Type : Type}, but this choice leads to Girard's paradox, the type theory
equivalent of Russel's paradox. To avoid inconsistencies, we need a fresh type
to contain \mbox{\li{Type},} which we call \li{Type 1}. \li{Type 1} itself has
type \li{Type 2}, and so on:
%
\begin{center}
\begin{tabular}{@{}l@{}c@{}l@{}}
\lic|Type| & \lic| : | & \lic|Type 1| \\
\lic|Type 1| & \lic| : | & \lic|Type 2| \\
\lic|Type 2| & \lic| : | & \lic|Type 3| \\
& $\vdots$
\end{tabular}
\end{center}

In fact, \li{Type} with no argument is an abbreviation for \li{Type 0}. If we
want to incorporate \li{Prop} in this hierarchy, we can use the syntax
\li{Sort u}, where \li{Sort 0} is an alias for \li{Prop} and \li{Sort (u + 1)}
is an alias for \li{Type u}. The hierarchy is captured by the following typing
judgment:
%
\begin{gather*}
\prftree[r]{\textsc{Sort}}
  {\text{\lic{C ⊢ Sort u : Sort (u + 1)}}}
\end{gather*}

All of these types containing other types are called
\emph{universes}, and the \li{u} in the expression \li{Sort u} is a
\emph{universe level}. Although universe levels look like terms of type \li{ℕ},
they are in fact not even terms. By convention,
universes are capitalized---hence we have \li{Prop} but \li{bool}.
%Universe levels can be constructed
%using universe variables (e.g., \li{u}), zero (\li{0}), and
%successor (\li{_ + 1}).
% and the operators \li{max} and \li{imax}.

Instead of using \li{Type} everywhere, you can make your theorems slightly more
general without having to think about universe levels by writing \li{Type _} or
\mbox{\li{Type*}}. It leaves it to Lean to figure the right universe level or
to create a fresh universe variable. This helps maintain the illusion that we
work in a convenient logic where \li{Type : Type} holds, but without
introducing any paradoxes. In practice, \li{Type 0} is large enough for most of
computer science and mathematics.

% Lean's type hierarchy is \emph{noncumulative}: Each type lives only in one universe

% (This is different in Coq, where \li{p : Type u} implies \li{p : Type v} for all \li{v ≥ u})

% We can use \li{ulift : Type u → Type (max u v)} to transport types between universes

% Constants can also be polymorphic in the universe, and can be annotated with universes—e.g., \li|eq.{u}|.

\section{The Peculiarities of Prop}
\label{sec:the-peculiarities-of-prop}

Although \li{Prop} may seem to fit nicely into the universe hierarchy,
it differs from the other universes in several important respects.

\subsection{Impredicativity}
\label{ssec:impredicativity}

When constructing a new type from other types (e.g., \li{α → β}
from \li{α : Type u} and \li{β : Type v}), the newly constructed type is
more complex than each of its components, and it is natural to put it into
the largest universe involved (e.g., \li{α →} \hbox{\li{β : Type (max u v)}}).
This is exactly what Lean does. The following typing rule expresses this idea
generally for dependent types:
%
\begin{gather*}
\prftree[r]{\textsc{Forall-Type}}
  {\text{\lic{C ⊢ α : Type u}}}
  {\text{\lic{C, a : α ⊢ β a : Type v}}}
  {\text{\lic{C ⊢ (∀a : α, β a) : Type (max u v)}}}
\end{gather*}
%
This behavior of the \li{Type} universes is called \emph{predicativity}. In
general, predicativity means that an object \emph{must not} be defined in terms
of a quantifier ranging over that same object.

However, it is convenient to have \li{Prop} behave differently. We would like
the expression \li{∀a : Prop, a → a} to be of type \li{Prop}---it is, after all,
a proposition. Unfolding the syntactic sugar \li{→}, this expression is the
same as \li{∀(a : Prop) (x : a), a}. If we had \li{Type u} instead of
\li{Prop}, the above typing rule would yield
%
\[\hbox{\lic{(∀(a : Type u) (x : a), a) : Type (u + 1)}}\]
%
because \li{Type u : Type (u + 1)} and \li{max (u + 1) (max u u) = u + 1}.
Thus, the universe level is increased by one when typing this expression.
To force expressions such as \li{∀a : Prop, a → a}
to be of type \li{Prop} anyway, we need a special typing rule
for \li{∀}-expressions with a \li{Prop} body:
%
\begin{gather*}
\prftree[r]{\textsc{Forall-Prop}}
  {\text{\lic{C ⊢ α : Sort u}}}
  {\text{\lic{C, (a : α) ⊢ β a : Prop}}}
  {\text{\lic{C ⊢ (∀a : α, β a) : Prop}}}
\end{gather*}
%
The rule yields
%
\[\hbox{\lic{(∀(a : Prop) (x : a), a) : Prop}}\]
%
as desired. The two typing rules for \li{∀}-expressions above can be summarized
as the single rule
%
\begin{gather*}
\prftree[r]{\textsc{Forall}}
  {\text{\lic{C ⊢ α : Sort u}}}
  {\text{\lic{C, a : α ⊢ β a : Sort v}}}
  {\text{\lic{C ⊢ (∀a : α, β a) : Sort (imax u v)}}}
\end{gather*}
%
where \li{imax u 0 = 0} and \li{imax u (v + 1) = max u (v + 1)}.
%
This behavior is called \emph{impredicativity} of \li{Prop}. In general,
impredicativity means that an object \emph{may} be defined via a quantifier
ranging over itself.

\subsection{Proof Irrelevance}
\label{ssec:proof-irrelevance}

A second difference between \li{Prop} and \li{Type} is \emph{proof
irrelevance}. It means that any two proofs of the same proposition \li{a} are
equal:
%
\lstinputlisting[linerange=proof_irrel-q]{../lean/love11_logical_foundations_of_mathematics_demo_master.lean}
%
In Lean, this equality is a syntactic equality up to computation, allowing us
to use the \li{refl} tactic. When viewing a proposition as a type and a proof
as an element of that type, proof irrelevance means that a proposition is
either an empty type or has exactly one inhabitant. If it is empty, it is
false. If it has exactly one inhabitant, it is true. Proof irrelevance is very
helpful when reasoning about dependent types.

In Chapter~\ref{chap:inductive-predicates}, we saw a diagram depicting the
interpretation of \li{bool} and \li{Prop} side by side. The diagram did not take
proof irrelevance into account and showed multiple proofs for the same
proposition. We now know this is not accurate. Here is a revised diagram:
%
\begin{align*}
&
\hbox{\li{bool}:~~}
\vcenter{\hbox{\begin{tikzpicture}[
    inner sep=1mm]
  \path node at (0, 0) [shape=circle,draw,minimum size=2.9em,fill=white] {\Huge$\cdot\,\cdot$};
\end{tikzpicture}}}
&&
\hbox{\li{Prop}:~~}
\vcenter{\hbox{\begin{tikzpicture}[
    inner sep=1mm]
  \path node at (0, 0) [shape=rectangle,draw,minimum size=7em,minimum width=9em,fill=gray!20] {};
  \path node at (-1, +0.625) [shape=circle,draw,minimum size=2.9em,fill=white] {};
  \path node at (-1, -0.625) [shape=circle,draw,minimum size=2.9em,fill=white] {\Huge$\cdot$};
  \path node at (0.25, +0.625) [shape=circle,draw,minimum size=2.9em,fill=white] {\Huge$\cdot$};
  \path node at (0.25, -0.625) [shape=circle,draw,minimum size=2.9em,fill=white] {};
  \path node at (1.3, +0.625) {\large$\cdots$};
  \path node at (1.3, -0.625) {\large$\cdots$};
\end{tikzpicture}}}
\end{align*}

To make proof irrelevance work, Lean must give up the ``no confusion'' property
for inductive predicates. Indeed, various proofs of the same proposition should
definitely be ``confused.'' This only concerns inductive predicates, not
inductive types in general.

An unfortunate consequence of proof irrelevance is that it prevents us from
performing rule induction by pattern matching. Induction by pattern matching
relies on a ``measure''---a function to \li{ℕ} that assigns a size to the
arguments. Without large elimination, the measure cannot be defined
meaningfully. This explains why we always use the \li{induction'} tactic for
rule induction.

Other systems and logics make different choices. For example, Coq is
proof-relevant by default but compatible with proof irrelevance. Homotopy type
theory and other constructive or intuitionistic type theories build on data in
equality proofs and are therefore incompatible with proof irrelevance.

\subsection{No Large Elimination}
\label{ssec:no-large-elimination}

A further difference between \li{Prop} and \li{Type} is that \li{Prop} does not
allow \emph{large elimination}: It is generally impossible to extract
information from a proof of a proposition and use it in a program (i.e., a
value of a type from \li{Type}). After all, because of proof irrelevance, all
proofs of a given proposition are equal, so they cannot carry specific
information that would distinguish them.

Imagine we could extract information from proofs inside a program. We could for
instance use the \li{match} construct in function definitions such as the
following:
%
\lstinputlisting[linerange=unsquare-q]{../lean/love11_logical_foundations_of_mathematics_demo_master.lean}
%
The \li{unsquare} takes a square number \li{i} and a proof \li{hsq} that \li{i} is
actually a square number and returns the number \li{j} before squaring,
extracted from the proof. Lean raises the error
%
\begin{quote}
\tabletsmall\ttfamily\raggedright
induction tactic failed, recursor 'Exists.dcases\_on' can only eliminate into Prop
\end{quote}
%
If it accepted the definition, we could derive \li{false} as follows. Let
%
\begin{center}
\begin{tabular}{@{}r@{}c@{}l@{}}
\lic|hsq₁| & \lic| := | & \lic|Exists.intro 3 (by linarith)| \\
\lic|hsq₂| & \lic| := | & \lic|Exists.intro (-3) (by linarith)| \\
\end{tabular}
\end{center}
%
be two proofs of \li{∃j, (9 : ℤ) = j * j}. Notice that they use different
witnesses for~\li{j} (\hbox{\li{3}} versus \li{-3}). We then have
\li{unsquare 9 hsq₁ =} \li{3} and \hbox{\li{unsquare 9 hsq₂ = -3}.} Yet, by
proof irrelevance, \li{hsq₁ = hsq₂}. Hence, \li{unsquare 9 hsq₂} equals \li{3}.
But we already determined that it equals \li{-3}. This means \li{3 = -3}, a
contradiction.

As a compromise, Lean allows \emph{small elimination}, which eliminates only
into \li{Prop}---whereas large elimination can eliminate into an arbitrary
large universe \li{Sort u}. This means we can use \li{match} to analyze
the structure of a proof, extract existential witnesses, and so on, as long as
the \li{match} expression itself is a proof. We have seen several examples of
this in Section~\ref{sec:elimination}.

As a further compromise, Lean allows large elimination for \emph{syntactic
subsingletons}:\ types in \li{Prop} for which it can be established
syntactically that they have cardinality 0 or 1. These are propositions
such as \li{false} and \li{a ∧ b} that can be proved in at most one way.
For example, \li{false} has no proof, and all proofs of \li{a ∧ b} have the form
\li{and.intro _ _}. (Recursively, there might be several ways to prove \li{a}
and \li{b}.) More precisely, a syntactic subsingleton is an inductive
definition with at most one constructor whose arguments are either \li{Prop} or
appear as immediate arguments in the result type. When we match \li{h : a ∧ b}
against the pattern \li{and.intro ha hb}, no information is leaked about \li{h}.

\section{The Axiom of Choice}
\label{sec:the-axiom-of-choice}

Lean's logic includes the axiom of choice, which makes it possible to obtain an
arbitrary element of any nonempty type. Consider the following predicate:
%
\begin{lstlisting}
inductive nonempty (α : Sort u) : Prop
| intro (val : α) : nonempty
\end{lstlisting}
%
The predicate states that \li{α} has at least one element. To
prove \li{nonempty α}, we must provide an \li{α} value to \li{nonempty.intro}:
%
\lstinputlisting[linerange=nat.nonempty-q]{../lean/love11_logical_foundations_of_mathematics_demo_master.lean}
%
Since \li{nonempty} lives in \li{Prop}, large elimination is not available, and
thus we cannot extract the element that was used from the proof of
\li{nonempty α}.

In Lean, the axiom of choice takes the form of a function that returns an
arbitrary \li{α}-typed value given a proof of \li{nonempty α}:
%
\begin{lstlisting}
constant classical.choice {α : Sort u} : nonempty α → α
\end{lstlisting}
%
We have no way to know whether this is the same element that was used to prove
\li{nonempty α}. It will just be an arbitrary element of \li{α}, thereby
avoiding inconsistencies. Using the axiom of choice, we can state properties
that are unprovable but whose negation is \emph{also} unprovable---e.g.,
\li{classical.choice nat.nonempty = 42}.

The constant \li{classical.choice} is noncomputable. If we ask Lean for its
value using \li{#reduce} or \li{#eval}, it will refuse to compute it. In other
words, proofs may be terms, but they are not necessarily programs. This is one
of the reasons why some logicians prefer to work without this axiom. By
contrast, the vast majority of mathematicians have no objections against the
axiom.

Unlike proof irrelevance and large and small elimination, the axiom of choice
is not built into the Lean kernel; it is only an axiom in the core library,
giving us the freedom to work without it. Lean requires us to mark definitions
using the \li{noncomputable} keyword if they use \li{classical.choice} to
define constants in \li{Type}, much in the same way as \li{meta} for
metadefinitions (Chapter~\ref{chap:metaprogramming}).

The following tools rely on \li{classical.choice}:

\begin{itemize}
\item The function \li{classical.some}, often called Hilbert's choice operator,
can help us find a witness of \li{∃a : α, p a}, if we do not care which one.
Its companion \li{classical.some_spec} gives a proof that the witness is indeed
a witness.
%
\begin{center}
\tabletsmall
\begin{tabular}{@{}r@{}l@{}}
\lic|classical.some| & \lic| : (∃a : α, p a) → α| \\
\lic|classical.some_spec| & \lic| : ∀h : (∃a : α, p a), p (classical.some h)| \\
\end{tabular}
\end{center}
%
Intuitively, the choice operator tells us, ``Convince me that there exists an
element satisfying \li{p} and I will give you such an element.''

\item We can also derive the traditional axiom of choice:
%
\begin{center}
\tabletsmall
\begin{tabular}{@{}l@{}}
\lic|classical.axiom_of_choice (α β : Type) {r : α → β → Prop} :| \\
\noindent\hbox{}\quad \lic|(∀x : α, ∃y : β, r x y) → (∃f, ∀x, r x (f x))| \\
\end{tabular}
\end{center}

\item From the axiom of choice and propositional and functional extensionality
(\li{propext}, \li{funext}), we can derive the law of excluded middle:
%
\begin{center}
\begin{tabular}{@{}r@{}l@{}}
\lic|classical.em| & \lic| : ∀a : Prop, a ∨ ¬ a| \\
\end{tabular}
\end{center}
%
With the law of excluded middle, every proposition is decidable. This means
that we can construct proofs based on a case distinction on whether a certain
proposition is true. We introduced this technique in Chapters
\ref{chap:functional-programming}~and~\ref{chap:inductive-predicates}.
\end{itemize}

In Section~\ref{ssec:proof-irrelevance}, we saw a diagram depicting the
interpretation of \li{bool} and \li{Prop} side by side. The diagram suggested
the existence of an infinite number of propositions, but we now know that there
are exactly two propositions:\ \li{false} and \li{true}, the latter of which has
a proof. Here is a revised diagram:
%
\begin{align*}
&
\hbox{\li{bool}:~~}
\vcenter{\hbox{\begin{tikzpicture}[
    inner sep=1mm]
  \path node at (0, 0) [shape=circle,draw,minimum size=2.9em,fill=white] {\Huge$\cdot\,\cdot$};
\end{tikzpicture}}}
&&
\hbox{\li{Prop}:~~}
\vcenter{\hbox{\begin{tikzpicture}[
    inner sep=1mm]
  \path node at (0, 0) [shape=rectangle,draw,minimum size=3.5em,minimum width=7em,fill=gray!20] {};
  \path node at (-0.625, 0) [shape=circle,draw,minimum size=2.9em,fill=white] {};
  \path node at (+0.625, 0) [shape=circle,draw,minimum size=2.9em,fill=white] {\Huge$\cdot$};
\end{tikzpicture}}}
\end{align*}
%
If we mentally connect \li{bool}'s two elements (\li{ff} and \li{tt}) with
\hbox{\li{Prop}'s} two types (\li{false} and \li{true}), we see that \li{Prop} is
nearly the same as \li{bool}, except that propositions of type \li{Prop} can
store proofs, in accordance with the PAT principle. The following table
summarizes the situation:

\begin{center}
\begin{tabular}{@{}l@{}l@{}l@{}}
& {\color{white}\relax{\li| : |}}\lic|false| & \lic| : Prop| \\
\lic|true.intro| & \lic| : true| & \lic| : Prop| \\
\lic|ff| & \lic| : bool| & \lic| : Type| \\
\lic|tt| & \lic| : bool| & \lic| : Type| \\
\end{tabular}
\end{center}

\section{Subtypes}
\label{sec:subtypes}

Inductive types are a very convenient definitional mechanism when they are
applicable, but lots of mathematical constructions do not fit that mold. Lean
provides two alternatives to cater for these:\ subtypes and quotients.

Subtyping is a mechanism to create new types from existing ones. Given a
predicate on the elements of a base type, the \emph{subtype} contains only
those elements of the base type that fulfill this property. More precisely, the
subtype contains element--proof pairs that combine an element of the base type
and a proof that it fulfills the property.

The following diagram depicts a subtype that was created by keeping two of the
base type's five elements:

\begin{center}
\begin{tabular}{@{}c@{\qquad\qquad}c@{}}
\begin{tikzpicture}[
    inner sep=1mm]
  \path node at (0, 0) [shape=circle,draw,minimum size=4.5em,fill=white] {\Huge${\cdot}$\kern.7ex\smash{\rlap{\raise-1.2ex\hbox{$\cdot$}}\rlap{\raise1.2ex\hbox{$\cdot$}}${\cdot}\kern.7ex{\cdot}$}};
\end{tikzpicture}
&
\begin{tikzpicture}[
    inner sep=1mm]
  \path node at (-0.27, -0.27) [shape=ellipse,draw,rotate=45,minimum size=1.4em,minimum height=3.6em] {};
  \path node at (0, 0) [shape=circle,minimum size=4.5em] {\Huge${\cdot}$\kern.7ex\smash{\rlap{\raise-1.2ex\hbox{$\cdot$}}\rlap{\raise1.2ex\hbox{$\color{white}\cdot$}}${\color{white}\cdot}\kern.7ex{\color{white}\cdot}$}};
\end{tikzpicture}
\\
base type
&
subtype
\end{tabular}
\end{center}

Subtyping is useful for those types that cannot be defined as an inductive
type. For example, any attempt at defining the type of finite sets along the
lines of
%
\lstinputlisting[linerange=finset-q]{../lean/love11_logical_foundations_of_mathematics_demo_master.lean}
%
is doomed, because a given set may have multiple representations. For example,
\li|{1, 2}| can be represented in any of the following ways, and more:
%
\begin{center}
\lic|finset.insert 1 (finset.insert 2 empty)| \\
\lic|finset.insert 2 (finset.insert 1 empty)| \\
\lic|finset.insert 1 (finset.insert 1 (finset.insert 2 empty))|
\end{center}

Instead, we can define finite sets as the subtype of (possibly infinite) sets
that are finite. In general, subtypes have the syntax
%
\[\hbox{\verb${$\ttvar{variable}\lic$ : $\ttvar{base-type}\lic$ // $\ttvar{property-applied-to-variable}\verb$}$}\]
%
We saw an example in Section~\ref{sec:dependent-types}, namely,
\li|{i : ℕ // i ≤ n}|, which consists of the natural numbers \li{i}
fulfilling \li{i ≤ n}, where \li{n} is fixed in the context. The base type is
\li{ℕ}, and the property is \li{λi, i ≤ n}. A less suggestive but perhaps less
confusing syntax for the same type is \hbox{\lic|@subtype ℕ (λi, i ≤ n)|}.
Our motivating example, the type of finite sets over some type \li|α|, is
specified as \li|{A : set α // set.finite A}|, where \li|set.finite| returns
\li|true| if and only if its argument is finite.

\subsection{First Example: Full Binary Trees}
\label{ssec:first-example-full-binary-trees}

To illustrate subtypes, we will define a type of full binary trees, building on
the type \li{btree} from Section~\ref{sec:binary-trees}.
In Section~\ref{ssec:full-binary-trees}, we introduced a predicate \li{is_full}
that is true if each node of a tree has either zero or two child nodes. Based
on this type and this predicate, we can construct a subtype \li{full_btree},
containing only full binary trees, as follows:
%
\lstinputlisting[linerange=full_btree-q]{../lean/love11_logical_foundations_of_mathematics_demo_master.lean}
%
This is syntactic sugar for
%
\begin{lstlisting}
def full_btree (α : Type) : Type :=
@subtype (btree α) is_full
\end{lstlisting}
%
where \li{subtype} is defined as follows:
%
\begin{lstlisting}
inductive subtype {α : Type} (p : α → Prop) : Type
| mk : ∀x : α, p x → subtype
\end{lstlisting}

Elements of \li{full_btree} are essentially dependently typed pairs, where
the first component is a tree \li{t} and the second component is a
proof that \li{t} is full:
%
\lstinputlisting[linerange=empty_full_btree-q]{../lean/love11_logical_foundations_of_mathematics_demo_master.lean}
%
From a given element of \li{full_btree}, we can retrieve its two components via
\li{subtype.val} and \li{subtype.property}:
%
\lstinputlisting[linerange=val_prop-q]{../lean/love11_logical_foundations_of_mathematics_demo_master.lean}

The most appealing aspect of subtypes is that we can \emph{lift} the operations
from the base type to the subtype instead of having to build a library from
scratch, as long as they preserve the subtype property. We only need to define
``wrappers'' around constants from the base type. In general, defining such a
wrapper given an operation \li{f} on the base type involves three steps:
%
\begin{itemize}
\item[1.] extract the base type values from the wrapper arguments;
\item[2.] invoke \li{f} on those base type values;
\item[3.] encapsulate the result using \li{subtype.mk}, together with a proof
  that the resulting base type value fulfills the subtype property.
\end{itemize}

Using this procedure, we can lift \li{btree} functions to \hbox{\li{full_btree}}
functions if they preserve the property \li{is_full}. To lift the \hbox{\li{mirror}}
operation from the type \hbox{\li{btree →}} \hbox{\li{btree}} to the type
\li{full_btree → full_btree}, we must
%
\begin{itemize}
\item[1.] extract the \li{btree} from the wrapper argument;
\item[2.] invoke \li{mirror} on that \li{btree};
\item[3.] encapsulate the result using \li{subtype.mk}, together with a proof
  that the resulting \li{btree} fulfills \li{is_full}.
\end{itemize}
%
For step 3, we must extract the proof of \li{is_full} from the argument and
use the lemma \li{is_full_mirror} proved in Section
\ref{ssec:full-binary-trees}. Putting everything together, we get
%
\lstinputlisting[linerange=full_btree_mirror-q]{../lean/love11_logical_foundations_of_mathematics_demo_master.lean}

The input is an element \li{t} of the subtype \li{full_btree}. We decompose
\li{t} into \li{subtype.val t : btree} and
\li{subtype.property t : is_full t}. We use the \li{mirror} function to reverse
the tree component of \li{t} and use the lemma \hbox{\li{is_full_mirror},}
together with the proof component of \li{t}, to show the condition
\hbox{\li{is_full (mirror}} \hbox{\li{(subtype.val t))}.}

Finally, we build a pair containing the resulting tree and the proof that this
tree is full using \li{subtype.mk}. The \li{subtype.mk} constructor can be seen
both as a pair-like constructor and as a cast from \li{btree} to
\li{full_btree}, with a second argument that guarantees that the cast is safe.

For proofs about subtypes, the following lemma is useful:

\begin{center}
\begin{tabular}{@{}r@{}l@{}}
\lic|subtype.eq| & \lic| : subtype.val ?a = subtype.val ?b → ?a = ?b| \\
\end{tabular}
\end{center}
%
It states that two subtype values are equal if their \li{subtype.val}
components are equal. It is convenient that proofs are irrelevant in Lean,
because we would not want to have spurious duplicate values in the
subtype, differing only in their proofs. Here is how \li{subtype.eq} can be
used to prove that the mirror image of the mirror image of a \li{full_btree} is
the \li{full_btree} itself:
%
\lstinputlisting[linerange=full_btree_mirror_mirror-q]{../lean/love11_logical_foundations_of_mathematics_demo_master.lean}
%
Applying the lemma \li{subtype.eq} and then unfolding the definition of
\li{full_}\allowbreak\li{btree.}\allowbreak\li{mirror} yields the subgoal
%
\[\hbox{\li{mirror (mirror (subtype.val t)) = subtype.val t}}\]
%
which matches the statement of the lemma \li{mirror_mirror} from
Section~\ref{sec:binary-trees}.

\subsection{Second Example: Vectors}
\label{ssec:second-example-vectors}

As a second example, consider the definition of vectors from Lean's core
libraries:
%
\lstinputlisting[linerange=vec-q]{../lean/love11_logical_foundations_of_mathematics_demo_master.lean}
%
A vector is defined as a list of a given length. With lists, there is only one
type for a list of all lengths. For vectors, we have one dedicated type for
every length of a vector. The advantage of this scheme is that some operations,
such as addition or scalar product of vectors, rely on the two involved vectors
having the same length. We saw a morally equivalent but less practical
definition of vectors in Section~\ref{sec:dependent-inductive-types}.

Vectors can be built from lists using \li{subtype.mk}:
%
\lstinputlisting[linerange=vector_123-q]{../lean/love11_logical_foundations_of_mathematics_demo_master.lean}
%
Basic operations on vectors can be defined by decomposing them with \li{subtype.}\allowbreak\li{val}
and \li{subtype.property}, manipulating the underlying lists, and then
recomposing them with \li{subtype.mk}.
For example, we can define the componentwise negation of an integer vector as
follows:
%
\lstinputlisting[linerange=vector.neg-q]{../lean/love11_logical_foundations_of_mathematics_demo_master.lean}
%
We use the function \li{list.map} to negate every entry of the underlying list
and the lemma \li{list.length_map} to show that this operation does not change
the list's length.

Using \li{subtype.eq}, we can prove the following lemma about \li{vector.neg}:
%
\lstinputlisting[linerange=vector.neg_neg-q]{../lean/love11_logical_foundations_of_mathematics_demo_master.lean}
%
The application of \li{subtype.eq} reduces the goal to showing the corresponding property
on the underlying lists. We can then use \li{simp} to finish the proof.

\section{Quotient Types}
\label{sec:quotient-types}

Quotients are a powerful construction in mathematics used to define \li{ℤ},
\li{ℝ}, and many other sets. Lean supports \emph{quotient types}, an analogous
mechanism on types. Like subtyping, quotienting constructs a new type from an
existing type. Unlike a subtype, a quotient type contains all of the elements
of the base type, except that some elements that are different in the base type
may be considered equal in the quotient type. In mathematical terms, the
quotient type is isomorphic to a partition of the base type. The diagram below
shows a quotient type built from a three-way partition:

\begin{center}
\begin{tabular}{@{}c@{\qquad\qquad}c@{\qquad\qquad}c@{}}
\begin{tikzpicture}[
    inner sep=1mm]
  \path node at (0, 0) [shape=circle,draw,minimum size=4.5em,fill=white] {\Huge${\cdot}$\kern.7ex\smash{\rlap{\raise-1.2ex\hbox{$\cdot$}}\rlap{\raise1.2ex\hbox{$\cdot$}}${\cdot}\kern.7ex{\cdot}$}};
\end{tikzpicture}
&
\begin{tikzpicture}[
    inner sep=1mm]
  \path node at (-0.27, -0.27) [shape=ellipse,draw,rotate=45,minimum size=1.4em,minimum height=3.6em] {};
  \path node at (0, 0) [shape=circle,minimum size=4.5em] {\Huge${\cdot}$\kern.7ex\smash{\rlap{\raise-1.2ex\hbox{$\cdot$}}\rlap{\raise1.2ex\hbox{$\color{white}\cdot$}}${\color{white}\cdot}\kern.7ex{\color{white}\cdot}$}};
\end{tikzpicture}
&
\begin{tikzpicture}[
    inner sep=1mm]
  \path node at (-0.27, -0.27) [shape=ellipse,draw,rotate=45,minimum size=0.85em,minimum height=3.2em,fill=gray!40] {};
  \path node at (+0.27, +0.30) [shape=ellipse,draw,rotate=45,minimum size=0.85em,minimum height=3.2em,fill=gray!40] {};
  \path node at (0, +0.02) [shape=ellipse,draw,rotate=45,minimum size=0.6em,minimum height=1.2em,fill=gray!40] {};
  \path node at (0, 0) [shape=circle,draw,minimum size=4.5em] {\Huge${\cdot}$\kern.7ex\smash{\rlap{\raise-1.2ex\hbox{$\cdot$}}\rlap{\raise1.2ex\hbox{$\cdot$}}${\cdot}\kern.7ex{\cdot}$}};
\end{tikzpicture}
\\
base type
&
subtype
&
quotient type
\end{tabular}
\end{center}
%
The depicted quotient type has only three elements, represented by gray
ellipses. Each of these elements corresponds to one or more base type elements.

The prerequisites to construct a quotient type are a base type \li{τ} and an
equivalence relation \li{r : τ → τ → Prop} specifying which elements of the
base type will be considered equal in the quotient. To construct the quotient
type, we first need to prove that \li{r} is an equivalence relation on \li{τ}.
A type \li{τ} equipped with an equivalence relation is called a \emph{setoid}.
In Lean, \li{setoid} is a type class. We can declare an instance as follows:
%
\begin{lstlisting}
@[instance] def τ.setoid : setoid τ :=
{ r     := r,
  iseqv := … }
\end{lstlisting}
%
In addition, this instance declaration introduces the notation \li{a ≈ b} for
\hbox{\li{r a b}.} More importantly, we can now use the quotient type
\li{quotient τ.setoid}.

Every element \li{a : τ} belongs to some element in \li{quotient τ.setoid}, given
by
%
\[\hbox{\lic{quotient.mk : τ → quotient τ.setoid}}\]
%
As an abbreviation for \li{quotient.mk a}, we can write \li{⟦a⟧}.

The following axiom guarantees that pairs of elements for which
\li{r} holds are indeed equal in the quotient type:
%
\[\hbox{\li|quotient.sound {a b : τ} : a ≈ b → ⟦a⟧ = ⟦b⟧|}\]
%
A lemma states the converse:
%
\[\hbox{\li|quotient.exact {a b : τ} : ⟦a⟧ = ⟦b⟧ → a ≈ b|}\]

Finally, we can lift functions of type \li{τ → υ}, where \li{υ} is some
arbitrary type, to \li{quotient τ.setoid → υ} using \li{quotient.lift}, which
has the following computation rule. Given some \li{f : τ → υ} such that
\li{h : ∀a b, a ≈ b → f a = f b}, we have
%
\[\hbox{\lic{quotient.lift f h ⟦a⟧ = f a}}\]
%
for all \li{a : τ}. The argument \li{h} is a proof that \li{f} is
\emph{compatible} with \li{≈}; in other words, it does not distinguish between
\li{≈}-equivalent arguments.

\subsection{First Example: Integers}
\label{ssec:first-example-integers}

As an example for a quotient type, we will construct the integers. A
convenient approach is to construct a quotient over pairs of natural numbers.
The idea is that a pair \li{(p, n)} of natural numbers represents the integer
\li{p - n}. In this way, we can represent all nonnegative integers \li{p} by
\li{(p, 0)} and all negative integers \li{- n} by \li{(0, n)}. In addition, we
get many more representations of the same integers; for example, \li{(7, 0)},
\li{(8, 1)}, \li{(9, 2)}, and \li{(10, 3)} all represent the integer~\li{7}.

First, we need to register the equivalence relation that we want to use. We
want two pairs \li{(p₁, n₁)} and \li{(p₂, n₂)} to be equal when \li{p₁ - n₁}
and \li{p₂ - n₂} yield the same integer. However, the condition
\hbox{\li{p₁ - n₁ =}} \hbox{\li{p₂ - n₂}} does not work because subtraction on
\li{ℕ} is ill-behaved (e.g., \li{0 - 1 = 0}). Instead, we use the condition
\hbox{\li{p₁ + n₂ = p₂ + n₁},} which relies on addition.

We provide the definition of our equivalence relation, followed by a proof that
it is reflexive, symmetric, and transitive:
%
\lstinputlisting[linerange=int.rel-q]{../lean/love11_logical_foundations_of_mathematics_demo_master.lean}
%
We can now write \li{≈} for the equivalence relation:
%
\lstinputlisting[linerange=int.rel_iff-q]{../lean/love11_logical_foundations_of_mathematics_demo_master.lean}
%
Using the name \li{int.rel} of our \li{setoid} instance that we registered above,
we can then define the integers as
%
\lstinputlisting[linerange=int_def-q]{../lean/love11_logical_foundations_of_mathematics_demo_master.lean}

We can define the integer zero as
%
\lstinputlisting[linerange=int.zero-q]{../lean/love11_logical_foundations_of_mathematics_demo_master.lean}
%
In fact, any term of the form \li{⟦(m, m)⟧} represents the same integer:
%
\lstinputlisting[linerange=int.zero_eq-q]{../lean/love11_logical_foundations_of_mathematics_demo_master.lean}

Next, we define addition on our new integers. To define functions on a quotient
type, we cannot simply define them by pattern matching, as for inductive types.
Instead, we define the function on the base type first and then \emph{lift} the
definition to the quotient. To achieve this, we must prove that the definition
of the function \li{f} does not depend on the chosen representative of an
equivalence class (i.e., \li{a ≈ b → f a = f b}). The functions
\hbox{\li{quotient.}}\hbox{\li{lift}} (for unary functions) and
\li{quotient.lift₂} (for binary functions) can be used to lift functions in this
way.

Addition can be defined as adding the pairs of natural numbers componentwise.
We then need to provide a proof that this can be lifted to a function on the
quotient by showing that \li{pn₁ ≈} \li{pn₁'} and \li{pn₂ ≈ pn₂'} imply
%
{\tabletsmall
\begin{align*}
  & \text{\lic{\⟦(prod.fst pn₁}\phantom{\lic{'}}~\lic{+ prod.fst pn₂}\phantom{\lic{'}}\lic{, prod.snd pn₁}\phantom{\lic{'}}~\lic{+ prod.snd pn₂}\phantom{\lic{'}}\lic{)⟧}} \\
\text{\lic{=}\phantom{\lic{X}}}
  & \text{\lic{\⟦(prod.fst pn₁' + prod.fst pn₂', prod.snd pn₁' + prod.snd pn₂')⟧}}
\end{align*}}
%
Formally:
%
\lstinputlisting[linerange=int.add-q]{../lean/love11_logical_foundations_of_mathematics_demo_master.lean}
%
The resulting function \li{int.add} has the intended behavior:
%
\lstinputlisting[linerange=int.add_eq-q]{../lean/love11_logical_foundations_of_mathematics_demo_master.lean}
%
It would be very convenient if Lean let us enter this lemma as the definition of
\li{int.add} in the first place, presumably with the following syntax:
%
\lstinputlisting[linerange=int.add₂-q]{../lean/love11_logical_foundations_of_mathematics_demo_master.lean}
%
This would be a nice and intuitive syntax, but without a proof that the
definition is compatible with \li{≈}, we could define nonsensical functions and
use them to derive \li{false}. For example, we could define
%
\lstinputlisting[linerange=int.fst-q]{../lean/love11_logical_foundations_of_mathematics_demo_master.lean}
%
Observe that \li{int.fst ⟦(0, 0)⟧ = 0} and \li{int.fst ⟦(1, 1)⟧ = 1}. However,
since \hbox{\li{⟦(0,}} \hbox{\li{0)⟧ = ⟦(1, 1)⟧},} we get \li{0 = 1}, a
contradiction.

We can use the characteristic lemma \li{int.add_eq} to prove other lemmas
about \li{int.add}, such as
%
\lstinputlisting[linerange=int.add_zero-q,keywords={lemma,begin,end}]{../lean/love11_logical_foundations_of_mathematics_demo_master.lean}
%
The somewhat ill-named lemma \li{quotient.induction_on} is applied to perform
a case distinction on \li{i}, replacing \li{i} by \li{⟦pn⟧}, where \li{pn} is an
arbitrary value of the base type \li{ℕ × ℕ}. In general:
%
\begin{center}
\begin{tabular}{@{}r@{}l@{}}
\lic|quotient.induction_on| & \lic| : ∀q : quotient ?s, (∀a, ?p ⟦a⟧) → ?p q| \\
\end{tabular}
\end{center}
%
A more intuitive syntax for the first proof step would have been \li{cases' i},
but this is not supported by Lean.

\subsection{Second Example: Unordered Pairs}
\label{ssec:second-example-unordered-pairs}

\emph{Unordered pairs} are pairs for which no distinction is made between the
first and second components. They are usually written \{\textit{a},
\textit{b}\}. We will introduce the type \li{upair α} of unordered pairs over
\li{α} as the quotient of pairs \li{(a, b)} with respect to the relation
``contains the same elements as'':
%
\lstinputlisting[linerange=upair.rel-q]{../lean/love11_logical_foundations_of_mathematics_demo_master.lean}
%
\lstinputlisting[linerange=upair.rel_iff-q]{../lean/love11_logical_foundations_of_mathematics_demo_master.lean}
%
\lstinputlisting[linerange=upair_def-q]{../lean/love11_logical_foundations_of_mathematics_demo_master.lean}

We define \li{upair.mk a b} to construct an unordered pair containing \li{a}
and \li{b}:
%
\lstinputlisting[linerange=upair.mk-q]{../lean/love11_logical_foundations_of_mathematics_demo_master.lean}
%
It is easy to prove that \li{upair.mk} is symmetric, meaning that our pairs are
really unordered:
%
\lstinputlisting[linerange=upair.mk_symm-q]{../lean/love11_logical_foundations_of_mathematics_demo_master.lean}

Another representation of unordered pairs is as sets of cardinality 1 or 2.
The following operation converts \li{upair α} values to that representation:
%
\lstinputlisting[linerange=set_of_upair-q]{../lean/love11_logical_foundations_of_mathematics_demo_master.lean}

\subsection{Alternative Definitions via Normalization~and~Subtyping}
\label{ssec:alternative-definitions-via-normalization-and-subtyping}

Each element of a quotient type correspond to a class of \li{≈}-equi\-valent
elements of the base type. If there exists a systematic way to obtain a
canonical representative for each \li{≈}-equivalence class, we can use a
subtype instead of a quotient, keeping only the canonical representatives and
filtering out the other elements.

Consider the quotient type \li{int} of integers constructed above. We observed
that \li{(7, 0)}, \li{(8, 1)}, \li{(9, 2)}, and \li{(10, 3)} all represent the
integer~\li{7}, but intuitively \li{(7, 0)} seems preferable to the others.
We will say that a pair \li{(p, n)} is \emph{canonical} if \li{p} or \li{n}
(or both) is \li{0}:
%
\lstinputlisting[linerange=int.is_canonical-q]{../lean/love11_logical_foundations_of_mathematics_demo_master.lean}
%
The integers consist of the canonical pairs of natural numbers:
%
\lstinputlisting[linerange=int_subtype_def-q]{../lean/love11_logical_foundations_of_mathematics_demo_master.lean}
%
Clearly, each integer can be represented in one and only one way.
Operations on integers, such as addition and multiplication, must provide
canonical results. Fortunately, normalizing pairs of natural numbers is easy:
%
\lstinputlisting[linerange=int_normalization-q]{../lean/love11_logical_foundations_of_mathematics_demo_master.lean}

For unordered pairs, there is no obvious normal form, except to always put the
smaller element first (or last). This requires a linear order \li{≤} on \li{α}:
%
\lstinputlisting[linerange=upair_subtype_def-q]{../lean/love11_logical_foundations_of_mathematics_demo_master.lean}

Returning to the \li{int.is_canonical} predicate, notice that there are two
proofs that \li{(0, 0)} is canonical, using either \li{nonpos} or \li{nonneg}.
By proof irrelevance, these proofs must be equal. But this would seem to
contradict the ``no confusion'' property of inductive definitions. Fortunately,
as we saw in Section~\ref{ssec:proof-irrelevance}, this property does not apply
to inductive predicates, so there is no reason to worry.

\section{Summary of New Lean Constructs}

\begingroup
\summarysize

\subsection*{Declaration}

\noindent
\begin{xltabular}{\textwidth}{@{}p{9em}X@{}}
\lic|noncomputable| & prefixes noncomputable declarations \\
\end{xltabular}

\subsection*{Constants}

\noindent
\begin{xltabular}{\textwidth}{@{}p{9em}X@{}}
\li|classical.choice| & function that returns an arbitrary element of a nonempty~type \\
\li|classical.some| & function that returns a witness given a proof of \hbox{an existential} \\
\li|quotient| & function that creates a quotient type of a given \hbox{setoid instance} \\
\li|quotient.lift| & function that lifts a unary function to a quotient type \\
\li|quotient.lift₂| & function that lifts a binary function to a quotient type \\
\li|setoid| & type class for a type with an equivalence relation on it \\
\li|Sort u| & universe at level \li{u} \\
\end{xltabular}

\subsection*{Notations}

\noindent
\begin{xltabular}{\textwidth}{@{}p{9em}X@{}}
\li|\{x : α // P[x]\}| & subtype of all \li{x} in \li{\α} fulfilling \li{P[x]} \\
\li|\≈| & equivalence relation on a setoid (used for quotienting) \\
\li|Prop| & abbreviation for \li{Sort 0} \\
\li|Type u| & abbreviation for \li{Sort (u + 1)} \\
\end{xltabular}

\subsection*{Lemmas}

\noindent
\begin{xltabular}{\textwidth}{@{}p{9em}X@{}}
\li|classical|\rlap{\li|.axiom_of_choice|} \\
  & traditional axiom of choice \\
\li|classical|\rlap{\li|.some_spec|} \\
  & characteristic property of \li|classical.some| \\
\li|quotient.exact| & equality on quotient type implies \li|\≈| on base type \\
\li|quotient|\rlap{\li|.induction_on|} \\
  & case distinction on a quotient type value \\
\li|quotient.sound| & \li|\≈| on base type implies equality on quotient type \\
\li|subtype.eq| & equality on base type implies equality of subtype \\
\end{xltabular}

\endgroup
