\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 theorem
%
\[\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.
%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 _}.
Lean then creates 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 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{Arrow-Type}}
  {\text{\lic{C ⊢ σ : Type u}}}
  {\text{\lic{C, x : σ ⊢ τ[x] : Type v}}}
  {\text{\lic{C ⊢ (x : σ) → τ[x] : 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 for \li{∀}, this expression is the
same as \hbox{\li{(a : Prop)}} \hbox{\li{→ a}} \hbox{\li{→ a}.}
If we had \li{Type u} instead of \li{Prop}, the above typing rule would yield
%
\[\hbox{\lic{(a : Type u) → a → a : Type (u + 1)}}\]
%
since \li{Type u : Type (u + 1)} and \hbox{\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{Arrow-Prop}}
  {\text{\lic{C ⊢ σ : Sort u}}}
  {\text{\lic{C, x : σ ⊢ τ[x] : Prop}}}
  {\text{\lic{C ⊢ (∀x : σ, τ[x]) : Prop}}}
\end{gather*}
%
The rule yields
%
\[\hbox{\lic{∀a : Prop, a → a : Prop}}\]
%
as desired. The two typing rules above can be summarized as the single rule
%
\begin{gather*}
\prftree[r]{\textsc{Arrow}}
  {\text{\lic{C ⊢ σ : Sort u}}}
  {\text{\lic{C, x : σ ⊢ τ[x] : Sort v}}}
  {\text{\lic{C ⊢ (x : σ) → τ[x] : 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/LoVe/LoVe12_LogicalFoundationsOfMathematics_DemoMaster.lean}
%
In Lean, this equality is a syntactic equality up to computation, allowing us
to use the \li{rfl} 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 Section~\ref{sec:rule-induction}, 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=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{false} and \hbox{\li{true})} 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|false| & \lic| : Bool| & \lic| : Type| \\
\lic|true| & \lic| : Bool| & \lic| : Type| \\
\end{tabular}
\end{center}

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 (e.g.,
\li{Even}), not inductive types in general (e.g., \li{List α}).

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 belonging to \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/LoVe/LoVe12_LogicalFoundationsOfMathematics_DemoMaster.lean}
%
The \li{unsquare} function 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
tactic 'induction' failed, recursor 'Exists.casesOn' 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.

An unfortunate consequence of the absence of large elimination is that we cannot
perform rule induction by pattern matching and recursion. This kind of induction
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.

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{Type 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 in 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} 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 multiple 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 about \li{h} is leaked.

\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}[keywords={inductive,Sort,Prop}]
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/LoVe/LoVe12_LogicalFoundationsOfMathematics_DemoMaster.lean}
%
Since \li{Nonempty} lives in \li{Prop}, large elimination is not available, and
thus we cannot extract the element that was used in the proof of
\li{Nonempty α}.

In Lean, the axiom of choice takes the form of a function that returns an
arbitrary \li{α} value given a proof of \li{Nonempty α}:
%
\begin{center}
\lic|Classical.choice {α : Sort u} : Nonempty α → α|
\end{center}
%
We have no way to know whether the returned element is the same element that was
used to prove \li{Nonempty α}. It will just be an arbitrary element of \li{α}.

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 the axiom of choice. 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,
and we are free to work without it. Lean requires us to mark definitions
with the \li{noncomputable} keyword if they use \li{Classical.choice} to
define constants in \li{Type}.

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

\begin{itemize}
\item The function \li{Classical.choose}, 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.choose_spec} gives a proof that the witness is indeed
a witness.
%
\begin{center}
\tabletfootnotesize
\begin{tabular}{@{}r@{}l@{}}
\lic|Classical.choose| & \lic| : (∃a : α, p a) → α| \\
\lic|Classical.choose_spec| & \lic| : ∀h : (∃a : α, p a), p (Classical.choose 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.axiomOfChoice (α β : 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}

\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 satisfy the predicate. More precisely, the
subtype contains element--proof pairs that combine an element of the base type
and a proof that the predicate is true for that element.

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/LoVe/LoVe12_LogicalFoundationsOfMathematics_DemoMaster.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 Finset.empty)| \\
\lic|Finset.insert 2 (Finset.insert 1 Finset.empty)| \\
\lic|Finset.insert 1 (Finset.insert 1 (Finset.insert 2 Finset.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{fun i ↦ i ≤ n}. A less suggestive but perhaps less
confusing syntax for the same type is \hbox{\lic|@Subtype ℕ (fun i ↦ i ≤ n)|}.
Our motivating example, the type of finite sets over some type \li|α|, is
specified as \li|{A : Set α // Set.Finite| \li|A}|, where \li|Set.Finite| is
\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 \li{BTree} type from Section~\ref{sec:binary-trees}.
In Section~\ref{ssec:full-binary-trees}, we introduced a predicate \li{IsFull}
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{FullBTree},
containing only full binary trees, as follows:
%
\lstinputlisting[linerange=FullBTree-q]{../lean/LoVe/LoVe12_LogicalFoundationsOfMathematics_DemoMaster.lean}
%
This is syntactic sugar for
%
\begin{lstlisting}
def FullBTree (α : Type) : Type :=
  @Subtype (BTree α) IsFull
\end{lstlisting}
%
where \li{Subtype} is defined as follows:
%
\begin{lstlisting}
inductive Subtype {α : Type} (p : α → Prop) : Type
  | mk : (x : α) → p x → Subtype p
\end{lstlisting}

Elements of \li{FullBTree} 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_FullBTree-q]{../lean/LoVe/LoVe12_LogicalFoundationsOfMathematics_DemoMaster.lean}
%
Given a value of type \li{FullBTree}, we can retrieve its two components via
\li{Subtype.}\allowbreak\li{val} and \li{Subtype.property}:
%
\lstinputlisting[linerange=val_prop-q]{../lean/LoVe/LoVe12_LogicalFoundationsOfMathematics_DemoMaster.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 around 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{FullBTree}}
functions if they preserve the property \li{IsFull}. For example, to lift the
\hbox{\li{mirror}} operation from the type \hbox{\li{BTree →}} \hbox{\li{BTree}}
to the type \li{FullBTree → FullBTree}, 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{IsFull}.
\end{itemize}
%
For step 3, we must extract the proof of \li{IsFull} from the argument and
use the theorem \li{IsFull_mirror} from Section
\ref{ssec:full-binary-trees}. Putting everything together, we get
%
\lstinputlisting[linerange=FullBTree_mirror-q]{../lean/LoVe/LoVe12_LogicalFoundationsOfMathematics_DemoMaster.lean}

The input is an element \li{t} of the subtype \li{FullBTree}. We decompose
\li{t} into \li{Subtype.val t : BTree} and
\hbox{\li{Subtype.property t :}} \li{IsFull t}. We use the earlier \li{mirror} function to reverse
the tree component of \li{t} and use the theorem \li{IsFull_}\allowbreak\li{mirror},
together with the property component of \li{t}, to show the condition
\li{IsFull} \li{(mirror} \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{FullBTree}, with a second argument that guarantees that the cast is safe.

For proofs about subtypes, the following theorem 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 crucial 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{FullBTree} is
the \li{FullBTree} itself:
%
\lstinputlisting[linerange=FullBTree_mirror_mirror-q]{../lean/LoVe/LoVe12_LogicalFoundationsOfMathematics_DemoMaster.lean}
%
Applying the theorem \li{Subtype.eq} and 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 theorem \li{mirror_mirror} from
Section~\ref{sec:binary-trees}.

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

As a second example, consider the following definition of vectors:
%
\lstinputlisting[linerange=vec-q]{../lean/LoVe/LoVe12_LogicalFoundationsOfMathematics_DemoMaster.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 and scalar product of vectors, require that two involved vectors
have the same length. We saw a 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/LoVe/LoVe12_LogicalFoundationsOfMathematics_DemoMaster.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/LoVe/LoVe12_LogicalFoundationsOfMathematics_DemoMaster.lean}
%
We use the function \li{List.map} to negate every entry of the underlying list
and the theorem \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 theorem about \li{Vector.neg}:
%
\lstinputlisting[linerange=vector.neg_neg-q]{../lean/LoVe/LoVe12_LogicalFoundationsOfMathematics_DemoMaster.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 grayed
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 using the
command
%
\begin{lstlisting}
instance τ.Setoid : Setoid τ :=
  { r     := R
    iseqv :=
      { refl  := …
        symm  := …
        trans := … } }
\end{lstlisting}
%
where the ellipses stand for missing proofs of the respective properties.
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 \li{Quotient.mk τ.Setoid a}, with
%
\[\hbox{\lic|Quotient.mk {α : Type} → (s : Setoid α) → α → Quotient s|}\]
%
The expression \li{Quotient.mk τ.Setoid a} is quite a mouthful. Fortunately,
Lean lets us abbreviate it to to \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 theorem 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
satisfies the following syntactic equality up to computation. Given some
\li{f : τ → υ} such that \li{h : ∀a b, a ≈} \li{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 of 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)}. We also
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.Setoid-q]{../lean/LoVe/LoVe12_LogicalFoundationsOfMathematics_DemoMaster.lean}
%
We can now write \li{≈} for the equivalence relation:
%
\lstinputlisting[linerange=Int.Setoid_Iff-q]{../lean/LoVe/LoVe12_LogicalFoundationsOfMathematics_DemoMaster.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/LoVe/LoVe12_LogicalFoundationsOfMathematics_DemoMaster.lean}

We can define the integer zero as
%
\lstinputlisting[linerange=Int.zero-q]{../lean/LoVe/LoVe12_LogicalFoundationsOfMathematics_DemoMaster.lean}
%
In fact, any term of the form \li{⟦(m, m)⟧} represents zero:
%
\lstinputlisting[linerange=Int.zero_Eq-q]{../lean/LoVe/LoVe12_LogicalFoundationsOfMathematics_DemoMaster.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.}}\allowbreak\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/LoVe/LoVe12_LogicalFoundationsOfMathematics_DemoMaster.lean}
%
The resulting function \li{Int.add} has the intended behavior:
%
\lstinputlisting[linerange=Int.add_Eq-q]{../lean/LoVe/LoVe12_LogicalFoundationsOfMathematics_DemoMaster.lean}

It would be very convenient if Lean let us enter this theorem as the definition of
\li{Int.add} in the first place, presumably with the following syntax:
%
\lstinputlisting[linerange=Int.add₂-q]{../lean/LoVe/LoVe12_LogicalFoundationsOfMathematics_DemoMaster.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/LoVe/LoVe12_LogicalFoundationsOfMathematics_DemoMaster.lean}
%
Notice that \li{Int.fst ⟦(0, 0)⟧ = 0} and \li{Int.fst ⟦(1, 1)⟧ = 1}. However,
since \hbox{\li{⟦(0,}} \li{0)⟧ = ⟦(1, 1)⟧}, we get \li{0 = 1}, a contradiction.

We can use the characteristic theorem \li{Int.add_Eq} to prove other theorems
about \li{Int.add}, such as
%
\lstinputlisting[linerange=Int.add_zero-q]{../lean/LoVe/LoVe12_LogicalFoundationsOfMathematics_DemoMaster.lean}
%
We invoke the \li{induction} tactic with \li{Quotient.inductionOn} as the
induction principle 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{ℕ × ℕ}. Then we perform a case distinction on \li{pn}, obtaining a
pair \li{(p, n)}. Finally, we simplify the goal, using the definition of
\li{Int.zero} and the characteristic equation of \li{Int.add}.

\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.Setoid-q]{../lean/LoVe/LoVe12_LogicalFoundationsOfMathematics_DemoMaster.lean}
%
\lstinputlisting[linerange=UPair.Setoid_Iff-q]{../lean/LoVe/LoVe12_LogicalFoundationsOfMathematics_DemoMaster.lean}
%
\lstinputlisting[linerange=UPair_def-q]{../lean/LoVe/LoVe12_LogicalFoundationsOfMathematics_DemoMaster.lean}

It is easy to prove that our pairs are really unordered:
%
\lstinputlisting[linerange=UPair.mk_symm-q]{../lean/LoVe/LoVe12_LogicalFoundationsOfMathematics_DemoMaster.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/LoVe/LoVe12_LogicalFoundationsOfMathematics_DemoMaster.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}
is \li{0}:
%
\lstinputlisting[linerange=Int.IsCanonical-q]{../lean/LoVe/LoVe12_LogicalFoundationsOfMathematics_DemoMaster.lean}
%
The integers then consist of the canonical pairs of natural numbers:
%
\lstinputlisting[linerange=int_subtype_def-q]{../lean/LoVe/LoVe12_LogicalFoundationsOfMathematics_DemoMaster.lean}
%
Clearly, each integer can be represented in one and only one way.
Operations on integers such as addition and multiplication must then provide
canonical results. Fortunately, normalizing pairs of natural numbers is easy:
%
\lstinputlisting[linerange=int_normalization-q]{../lean/LoVe/LoVe12_LogicalFoundationsOfMathematics_DemoMaster.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/LoVe/LoVe12_LogicalFoundationsOfMathematics_DemoMaster.lean}

Returning to the \li{Int.IsCanonical} predicate, we observe that there are two
proofs that \li{(0, 0)} is canonical, using either \li{Int.IsCanonical.nonpos}
or \li{Int.}\allowbreak\li{IsCanonical.nonneg}. This is not an issue because by
proof irrelevance these proofs must be equal.

\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.choose| & 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} \\
\li|Subtype.mk| & function that constructs a subtype value \\
\li|Subtype.property| & function that extracts the property from a subtype value \\
\li|Subtype.val| & function that extracts the base value from a subtype value \\
\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) \\
\lic|Prop| & abbreviation for \li{Sort 0} \\
\lic|Type u| & abbreviation for \li{Sort (u + 1)} \\
\end{xltabular}

\subsection*{Theorems}

\noindent
\begin{xltabular}{\textwidth}{@{}p{9em}X@{}}
\li|Classical|\rlap{\li|.axiomOfChoice|} \\
  & traditional axiom of choice \\
\li|Classical|\rlap{\li|.choose_spec|} \\
  & characteristic property of \li|Classical.choose| \\
\li|Quotient.exact| & equality on quotient type implies \li|\≈| on base type \\
\li|Quotient|\rlap{\li|.inductionOn|} \\
  & induction principle 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
