\chapter{Functional Programming}
\label{chap:functional-programming}

We take a closer look at the essence of typed functional programming:\
inductive types, proofs by induction, recursive functions, pattern matching,
structures (records), and type classes. The concepts covered here are described
in more detail in Chapters 7~to~10 of \emph{Theorem Proving in Lean 4}
\cite{theorem-proving-in-lean}.

\section{Inductive Types}
\label{sec:inductive-types}

Inductive types are modeled after the data types of typed functional
programming languages (e.g., Haskell, ML, OCaml). They are also reminiscent of
sealed classes in Scala. In
Chapter~\ref{chap:programs-and-theorems}, we saw some basic inductive
types:\ the natural numbers, a type of arithmetic expressions, and the finite
lists. In this chapter, we revisit the lists and study binary trees. We also
take a brief look at vectors of length \textit{n}, a dependent type.

Recall the definition of natural numbers as an inductive type:
%
\lstinputlisting[linerange=nat_def-q]{../lean/LoVe/LoVe02_ProgramsAndTheorems_DemoMaster.lean}
%
This defines the type \li{Nat} and the two constants
\li{Nat.zero} and \li{Nat.}\allowbreak\li{succ}, called constructors.
The definition also asserts some properties of the constructors. In addition,
it introduces further constants that are used internally to support induction
and recursion.

As we saw in Section~\ref{sec:type-definitions}, an inductive type is a type
whose members are all the values that can be built by a finite number of
applications of its constructors, and only those. Mottos:
%
\begin{itemize}
\item \emph{No junk}: The type contains no values beyond those expressible
  using the constructors.

\item \emph{No confusion}: Values built using a different combination of
  constructors are different.
\end{itemize}
%
For natural numbers, ``no junk'' means that there are no special values (such
as $-1$, \li{ε}, \li{∞}, or \li{NaN}) that cannot be expressed using a finite
combination of \li{Nat.zero} and \li{Nat.succ},
and ``no confusion'' ensures that \li{Nat.zero} ≠ \li{Nat.succ n} for all \li{n}
and that \li{Nat.succ} is injective.
%
In addition, values of inductive types are always finite. The
infinite term
%
\[\hbox{\lic{Nat.succ (Nat.succ (Nat.succ (Nat.succ …)))}}\]
%
is not a value. Nor does there exist a value \li{n} such that
\li{Nat.}\allowbreak\li{succ n = n}, as we will show below.

Inductive types are very convenient to use, because they support induction and
recursion and their constructors are well behaved, but not all types can be
defined as an inductive type. In particular, mathematical types such as \li{ℚ}
(the rationals) and \li{ℝ} (the real numbers) require more elaborate
constructions, based on quotienting and subtyping. This will be explained in
Chapters
\ref{chap:logical-foundations-of-mathematics}~and~\ref{chap:rational-and-real-numbers}.

\section{Structural Induction}
\label{sec:structural-induction}

\emph{Structural induction} is a generalization of mathematical induction to
arbitrary inductive types. To prove a goal \li{n : ℕ ⊢ P[n]} by structural
induction on \li{n}, it suffices to show two subgoals, traditionally called the
base case and the induction step:
%
\begin{align*}
& \hbox{\lic|\ ⊢ P[0]|} \\
\hbox{\ctxt{k} \lic|: ℕ, |\ctxt{ih} \lic|: P[k]|} & \hbox{\lic|\ ⊢ P[k + 1]|}
\end{align*}
%
We can of course also write \li{Nat.zero} and \li{Nat.succ k} instead
of \li{0} and \li{k + 1}.

In general, the situation is more complex. The goal might contain some extra
hypotheses (e.g., \li{Q}) that do not depend on \li{n} and others (e.g.,
\li{R[n]}) that do. Assuming we have one hypothesis of each kind, this gives the
initial goal
%
\[\hbox{\ctxt{hQ} \lic{: Q,} \ctxt{n} \lic{: ℕ,} \ctxt{hR} \lic{: R[n] ⊢ S[n]}}\]
%
Structural induction on \li{n} then produces the two subgoals
%
\begin{align*}
\hbox{\ctxt{hQ} \lic|: Q,| \ctxt{hR} \lic|: R[0]|} & \hbox{\lic|\ ⊢ S[0]|} \\
\hbox{\ctxt{hQ} \lic|: Q,| \ctxt{k} \lic|: ℕ,| \ctxt{ih} \lic|: R[k] → S[k],| \ctxt{hR} \lic|: R[k + 1]|} & \hbox{\lic|\ ⊢ S[k + 1]|}
\end{align*}
%
The hypothesis \li{Q} is simply carried over unchanged from the initial goal,
whereas \li{R[n] ⊢ S[n]} is treated almost the same as if the goal's target
had been \li{R[n] →} \li{S[n]}. This is easy to check by taking
\li{P[n] := R[n] → S[n]} in the first example above. Since this general format
is very verbose and hardly informative (now that we understand how it works),
from now on we will present goals in the simplest form possible, without extra
hypotheses.

For lists, given a goal \li{xs : list α ⊢ P[xs]}, structural induction on
\li{xs} yields
%
\begin{align*}
& \hbox{\lic|\ ⊢ P[[]]|} \\
\hbox{\ctxt{y} \lic|: α,| \ctxt{ys} \lic|: list α,| \ctxt{ih} \lic|: P[ys]|} & \hbox{\lic|\ ⊢ P[y :: ys]|}
\end{align*}
%
We can of course also write \li{List.nil} and \li{List.cons y ys}. There is no
induction hypothesis associated with \li{y}, because \li{y} is not of list type.

For arithmetic expressions, the base cases are
%
\begin{align*}
\hbox{\ctxt{i} \lic|: ℤ|} & \hbox{\lic|\ ⊢ P[AExp.num i]|} &
\hbox{\ctxt{x} \lic|: String|} & \hbox{\lic|\ ⊢ P[AExp.var x]|}
\end{align*}
%
and the induction steps are
\begin{align*}
& \hbox{\ctxt{e$_\texttt{1}$} \ctxt{e$_\texttt{2}$} \lic|: AExp,| \ctxt{ih$_\texttt{1}$}
  \lic|: P[e$_\texttt{1}$],| \ctxt{ih$_\texttt{2}$} \lic|: P[e$_\texttt{2}$] ⊢ P[AExp.add e₁ e₂]|} \\
& \hbox{\ctxt{e$_\texttt{1}$} \ctxt{e$_\texttt{2}$} \lic|: AExp,| \ctxt{ih$_\texttt{1}$}
  \lic|: P[e$_\texttt{1}$],| \ctxt{ih$_\texttt{2}$} \lic|: P[e$_\texttt{2}$] ⊢ P[AExp.sub e₁ e₂]|} \\
& \hbox{\ctxt{e$_\texttt{1}$} \ctxt{e$_\texttt{2}$} \lic|: AExp,| \ctxt{ih$_\texttt{1}$}
  \lic|: P[e$_\texttt{1}$],| \ctxt{ih$_\texttt{2}$} \lic|: P[e$_\texttt{2}$] ⊢ P[AExp.mul e₁ e₂]|} \\
& \hbox{\ctxt{e$_\texttt{1}$} \ctxt{e$_\texttt{2}$} \lic|: AExp,| \ctxt{ih$_\texttt{1}$}
  \lic|: P[e$_\texttt{1}$],| \ctxt{ih$_\texttt{2}$} \lic|: P[e$_\texttt{2}$] ⊢ P[AExp.div e₁ e₂]|}
\end{align*}
Notice the two induction hypotheses, about \li{e₁} and \li{e₂}.

In general, structural induction produces one subgoal per constructor. In each
subgoal, induction hypotheses are available for all constructor arguments of
the type we are performing the induction on.

Given an inductive type \li{τ}, the procedure to compute the subgoals is always
the same:
%
\begin{itemize}
\item[1.] Replace the hole in \li{P[ ]} with each possible constructor applied to
  fresh variables (e.g., \li{y :: ys}), yielding as many subgoals as there
  are constructors.

\item[2.] Add these new variables (e.g., \li{y}, \li{ys}) to the local context.

\item[3.] Add induction hypotheses for all new variables of type \li{τ}.
\end{itemize}

As an example, we will prove that \li{Nat.succ n ≠ n} for all \li{n : ℕ}. We
start with an informal proof:

\begin{quote}
The proof is by structural induction on \li{n}.

\textsc{Case} \li{0}: \,We must show \li{Nat.succ 0 ≠ 0}. This follows
from the ``no confusion'' property of the constructors of inductive types.

\begin{sloppypar}
\textsc{Case} \li{Nat.succ k}: \,The induction hypothesis is
\hbox{\li{Nat.succ k ≠ k}.} We must show \li{Nat.succ (Nat.succ k) ≠ Nat.succ k}.
By the injectivity of \li{Nat.succ}, we have that
\li{Nat.succ (Nat.succ k) = Nat.succ k} is equivalent to \li{Nat.succ k = k}.
%
Thus, it suffices to prove \li{Nat.succ k ≠ k}, which corresponds exactly to
the induction hypothesis. \qed
\end{sloppypar}
\end{quote}

Notice the main features of this informal proof, which you should aim to
reproduce in your own informal arguments:
%
\begin{itemize}
\item The proof starts with an unambiguous announcement of the type of proof we
  are carrying out (e.g., which kind of induction and on which variable).

\item The cases are clearly identified, and for each case, both the goal's
  target and the hypotheses are stated.

\item The key theorems on which the proof relies are explicitly invoked (e.g.,
  injectivity of \li{Nat.succ}).
\end{itemize}
%
Now let us carry out the proof in Lean:
%
\lstinputlisting[linerange=Nat.succ_neq_self-q]{../lean/LoVe/LoVe05_FunctionalProgramming_DemoMaster.lean}
%
The routine reasoning about constructors is all carried out by \li{simp}.

\section{Structural Recursion}
\label{sec:structural-recursion}

\emph{Structural recursion} is a form of recursion that allows us to peel off
one constructor from the value on which we recurse. The factorial function
below is structurally recursive:
%
\begin{lstlisting}
def fact : ℕ → ℕ
  | 0     => 0
  | n + 1 => (n + 1) * fact n
\end{lstlisting}
%
The constructor we peel off here is \li{Nat.succ} (written \li{+ 1}). Such
functions are guaranteed to call themselves only finitely many times before the
recursion stops; for example, \li{fact 12345} will call itself 12345 times.
The function is said to \emph{terminate}. This property helps ensure logical
consistency.

With structural recursion, there are as many equations as there are
constructors. Novices are often tempted to supply additional, redundant cases,
as in the following example:
%
\begin{lstlisting}
def factThreeCases : ℕ → ℕ
  | 0     => 0
  | 1     => 1
  | n + 1 => (n + 1) * factThreeCases n
\end{lstlisting}
%
It is in your own best interest to resist this temptation. The more cases you
have in your definitions, the more work it will be to reason about them.
Keep in mind the saying that \relax{one good definition is worth three theorems}.

For structurally recursive functions, Lean can automatically prove termination.
For more general recursive schemes, the termination check may fail. Sometimes it
does so for a good reason, as in the following example:

\lstinputlisting[linerange=illegal-q]{../lean/LoVe/LoVe05_FunctionalProgramming_DemoMaster.lean}
%
If Lean were to accept this definition, we could exploit it to prove that
\li{0 = 1}, by subtracting \li{illegal n} from each side of the equation
\li{illegal n = illegal n +} \hbox{\li{1}.} From \li{0 = 1}, we could derive \hbox{\li{False},}
and from \li{False}, we could derive anything. Clearly, we do not want that.

If we had used \li{opaque} and \li{axiom}, nothing could have saved us:
%
\lstinputlisting[linerange=immoral-q]{../lean/LoVe/LoVe05_FunctionalProgramming_DemoMaster.lean}

Another reason for preferring \li{def} over \li{opaque} and \li{axiom} is that
the defining equations can be used in computations. Tactics such as \li{rfl}
that unify up to computation become stronger each time we introduce a
definition, and the diagnostic commands \li{#eval} and \li{#reduce} can be used
on defined constants.

The observant reader will have noticed that the above definitions of factorial
are mathematically wrong: \li{fact} and \li{factThreeCases} shockingly return
\li{0} regardless of the argument. We quite literally \li{fact}ed up. These
embarrassing mistakes remind us to \emph{test} our definitions and \emph{prove}
some of their properties. Although flawed axioms arise now and then, what is
much more common are definitions that fail to capture the intended concepts.
Just because a function is called \li{fact} does not mean that it actually
computes factorials.

\section{Pattern Matching Expressions}
\label{sec:pattern-matching-expressions}

Pattern matching is possible not only at the top level of a \hbox{\li{def}} command
but also deeply within terms, via a \li{match} expression. The
construct has the following general syntax:
%
\begin{center}
\begin{tabular}{@{}l@{}}
\lic|match| \,\ttvar{term}$_\texttt{1}$\li|,| $\ldots$\li|,|
  \ttvar{term}$_\ttvar{m}$ \,\lic|with| \\
\phantom{\li{xx}}\lic$|$\, \ttvar{pattern}$_\texttt{11}$\li|,| $\ldots$\li|,|
  \ttvar{pattern}$_{\texttt{1}\ttvar{m}}$
  \,\lic|=>|\, \ttvar{result}$_\texttt{1}$ \\
\phantom{\li{xx}}\phantom{\texttt{|}\, \ttvar{pa}}$\vdots$ \\
\phantom{\li{xx}}\lic$|$\, \ttvar{pattern}$_{\ttvar{n}\texttt{1}}$\li|,| $\ldots$\li|,|
  \ttvar{pattern}$_\ttvar{nm}$
  \,\lic|=>|\, \ttvar{result}$_\ttvar{n}$
\end{tabular}
\end{center}
%
The construct is reminiscent of \li{match} in some modern programming
languages. An English translation of the above \li{match} expression follows:
%
\begin{quote}
Consider the terms \ttvar{term}$_\texttt{1}$\li|,| $\ldots$\li|,| \ttvar{term}$_\ttvar{m}$.

If they are respectively of the forms
  \hbox{\ttvar{pattern}$_\texttt{11}$\li|,| $\ldots$\li|,|
  \ttvar{pattern}$_{\texttt{1}\ttvar{m}}$,} \\
  then yield \ttvar{result}$_\texttt{1}$.

\noindent\hbox{}\qquad$\vdots$

If they are respectively of the forms
  \hbox{\ttvar{pattern}$_{\ttvar{n}\texttt{1}}$\li|,| $\ldots$\li|,|
  \ttvar{pattern}$_\ttvar{nm}$,} \\
  then yield \ttvar{result}$_\ttvar{n}$.
\end{quote}

The patterns may contain variables, constructors, and
nameless placeholders (\li{_}). The
\ttvar{result}$_\ttvar{i}$ expressions may refer to the
variables introduced in the corresponding patterns.

The following function definition demonstrates the syntax of pattern matching
within expressions:
%
\lstinputlisting[linerange=bcount-q]{../lean/LoVe/LoVe05_FunctionalProgramming_DemoMaster.lean}
%
The \li{bcount} function counts the number of elements in a list that satisfy
the given predicate \li{p}. The predicate's codomain is \hbox{\li{Bool}.} As a general
rule, we will use type \li{Bool}, of Booleans, within programs and use the type
\li{Prop}, of propositions, when stating properties of programs. The two values
of type \li{Bool} are called \li{false} and \li{true} (in lowercase).%
\footnote{Lean also allows us to use \li{True} and \li{False}, but these are
then implicitly converted from \li{Prop} to \li{Bool}. We generally recommend
avoiding such implicit coercions. Unfortunately, there is no way to disable
them.}
The connectives are called \li{or} (infix:\ \li{||}), \li{and} (infix:\
\li{&&}), and \li{not} (prefix:\ \li{!}).

The following diagram shows the interpretations of \li{Bool} and \li{Prop}:
%
\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\,\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*}

\noindent
Dots represents elements, circles represents types, and the rectangle represents
a type of types, or universe. We see that \li{Bool} is interpreted as a set
with two values, whereas \li{Prop} consists of an infinite number of
propositions (the types), each of which has zero or more proofs (the elements).
We will refine this picture in Chapter~\ref{chap:inductive-predicates}.

We cannot \li{match} on a proposition (of type \li{Prop}), but we can use
\li{if}--\li{then}--\li{else} instead. For example, the \li{min}
operator on natural numbers operator can be defined as follows:
%
\lstinputlisting[linerange=min-q]{../lean/LoVe/LoVe05_FunctionalProgramming_DemoMaster.lean}
%
This requires a decidable (i.e., executable) proposition. This is the case for
\li{≤}: Given concrete arguments such as \li{35} and \li{49}, Lean can reduce
\hbox{\li{35}} \hbox{\li{≤ 49}} to \li{True}. Lean keeps track of decidability
using a mechanism called type classes, which will be explained below.

\section{Structures}
\label{sec:structures}

Lean provides a convenient syntax for defining \emph{structures} (also called
records). These are essentially nonrecursive single-constructor inductive types
with some syntactic sugar.

The definition below introduces a structure called \li{RGB} with three fields
of type \li{ℕ} called \li{red}, \li{green}, and \li{blue}:
%
\lstinputlisting[linerange=RGB_def-q]{../lean/LoVe/LoVe05_FunctionalProgramming_DemoMaster.lean}
%
This definition has roughly the same effect as the following commands:
%
\lstinputlisting[linerange=RGB_as_inductive-q]{../lean/LoVe/LoVe05_FunctionalProgramming_DemoMaster.lean}

We can define a new structure as the extension of an existing structure. The
definition below extends \li{RGB} with a fourth field, called \li{alpha}:

\lstinputlisting[linerange=RGBA_def-q]{../lean/LoVe/LoVe05_FunctionalProgramming_DemoMaster.lean}

The general syntax to define structures is
%
\begin{quote}
\lic{structure} {\color{procnamecolor}\,\ttvar{structure-name}}
  \,\tabletbreak{\qquad}\lic{(}\ttvar{params}$_\texttt{1}$ \lic{:} \ttvar{type}$_\texttt{1}$\lic{)} $\ldots$
\lic{(}\ttvar{params}$_\ttvar{k}$ \lic{:} \ttvar{type}$_\ttvar{k}$\lic{)} \\
\noindent\hbox{}\quad$\bigl[$\lic{extends} \ttvar{structure}$_\texttt{1}$\lic{, …,} \ttvar{structure}$_\ttvar{m}\bigr]$
%  \,$\bigl[$\lic{:}\, \ttvar{universe}$\bigr]$
  \,\lic{where} \\
\noindent\phantom{\lic{xx}}\ttvar{f{}ield-name}$_\texttt{1}$ \,\lic{:}\, \ttvar{f{}ield-type}$_\texttt{1}$ \\
\noindent\hbox{}\phantom{\lic{xxxx}}$\vdots$ \\
\noindent\phantom{\lic{xx}}\ttvar{f{}ield-name}$_\ttvar{n}$ \,\lic{:}\, \ttvar{f{}ield-type}$_\ttvar{n}$
\end{quote}
%
The parameters \ttvar{params}$_\texttt{1}$, \ldots, \ttvar{params}$_\ttvar{k}$
are effectively additional fields, but unlike
\ttvar{f{}ield-name}$_\texttt{1}$, \ldots, \ttvar{f{}ield-name}$_\ttvar{n}$,
they are stored in the type, as arguments to the type constructor
\hbox{(\ttvar{structure-name}).}
%For \ttvar{universe}, we usually put \li{Type} or let Lean infer it for us.

Values can be specified in a variety of syntaxes:
%
\lstinputlisting[linerange=pure_red_etc_def-q]{../lean/LoVe/LoVe05_FunctionalProgramming_DemoMaster.lean}
%
The definition of \li{semitransparentGreen} copies all the values from
\li{pureGreen} except for the \li{alpha} field, which it sets explicitly.

Next, we define an operation called \li{shuffle}:
%
\lstinputlisting[linerange=shuffle_def-q]{../lean/LoVe/LoVe05_FunctionalProgramming_DemoMaster.lean}
%
The definition relies on the generated selectors
\li{RGB.}\allowbreak\li{red}, \li{RGB.}\allowbreak\li{green}, and
\li{RGB.}\allowbreak\li{blue}. Instead of \li{RGB.red c}, we could also write
\li{c.red}, and similarly for the other fields. Sometimes we will see this
notation in Lean's output, even if we do not use it ourselves.

Applying \li{shuffle} three times in a row is the same as not applying it at
all:
%
\lstinputlisting[linerange=shuffle_shuffle_shuffle-q]{../lean/LoVe/LoVe05_FunctionalProgramming_DemoMaster.lean}

\section{Type Classes}
\label{sec:type-classes}

Type classes are a mechanism that was popularized by Haskell and that is
present in several proof assistants. In Lean, a \emph{type class} is a
structure type combining abstract constants and their properties.%
\footnote{Despite its name, Lean's type class mechanism is more closely related
to Scala's implicit arguments than to Haskell's type classes.}
A type can be declared an instance of a type class by providing concrete
definitions for the constants and proving that the properties hold. Based on the
type, Lean retrieves the relevant instance.

A simple example is the type class \li{Inhabited}, which requires only a
constant \li{Inhabited.default} and no properties:
%
\begin{lstlisting}
class Inhabited (α : Type) : Type where
  default : α
\end{lstlisting}
%
The syntax is the same as for structures, except with the keyword \li{class}
instead of \li{structure}. The parameter \li{α} represents an arbitrary type
that could be a member of this class. This particular type class has a single
parameter and a single field, but in general a type class can have multiple
parameters and multiple fields.

Any type that has at least one element can be registered as an instance of the
\li{Inhabited} type class. For example, we can register \li{ℕ} by choosing an
arbitrary number to be the default value:
%
\lstinputlisting[linerange=inhabited_nat-q]{../lean/LoVe/LoVe05_FunctionalProgramming_DemoMaster.lean}
%
This specifies a value called \li{Nat.Inhabited} of type
\hbox{\li{Inhabited ℕ}.} Because we use the keyword \li{instance} instead of
\li{def}, the structure value is registered as \emph{the} canonical instance to
use whenever a structure of type \li{Inhabited ℕ} is desired. In the global
table storing type class instances, there is now an entry
%
\[\hbox{\lic{Inhabited ℕ} \;\lic{↦}\; \lic{Nat.Inhabited}}\]

For lists, the empty list is an obvious default value that can be constructed
even if \li{α} is not inhabited:
%
\lstinputlisting[linerange=inhabited_list-q]{../lean/LoVe/LoVe05_FunctionalProgramming_DemoMaster.lean}
%
This adds the following entry to the global table:
%
\[\hbox{\lic{Inhabited (List ?α)} \;\lic{↦}\; \lic{List.Inhabited}}\]

%Sometimes we may want to supply several instances of a given type class for the
%same type. Lean will then choose the first matching instance it finds.

As an example, observe that finite functions of type \li{α → β} can be represented
by their function tables, of type \li{β × ⋯ × β} (with \li{|α|} copies of \li{β}).
Accordingly, \li{|α → β| = |β|}$^{\text{\li{|α|}}}$. To make this \li{0}, we
must have both \li{|β| = 0} and \li{|α| ≠ 0}. In other words, the
type \li{α →} \li{β} is inhabited if either (1)~\li{β} is inhabited or
(2)~\li{α} is \emph{not} inhabited. We focus on case~(1):
%
\lstinputlisting[linerange=Fun.Inhabited_1-q]{../lean/LoVe/LoVe05_FunctionalProgramming_DemoMaster.lean}
%
The instance relies itself on an instance of the same type class but on a
different type. This occurs frequently.

The type \li{α × β} of pairs, also called the product type, contains values
of the form \hbox{\li{(a, b)},} where \li{a : α} and \li{b : β}. Given a
pair~\li{ab :} \li{α × β}, the first and second components can be extracted by
writing \li{Prod.fst ab} and \li{Prod.snd ab}. To provide an inhabitant of
\li{α × β}, we need both an inhabitant of \li{α} and an inhabitant of~\li{β}:

\lstinputlisting[linerange=Prod.Inhabited-q]{../lean/LoVe/LoVe05_FunctionalProgramming_DemoMaster.lean}

Using the \li{Inhabited} type class, we can define the head operation on
lists:\ the function that returns the first element of a list. Because an empty
list contains no elements, there is no meaningful value we can return in that
case. Given a type that belongs to the \li{Inhabited} type class, we can simply
return the default value:
%
\lstinputlisting[linerange=head-q]{../lean/LoVe/LoVe05_FunctionalProgramming_DemoMaster.lean}
%
We require that \li{α} belongs to \li{Inhabited} by writing \li{[Inhabited α]}.
This allows us to access \li{Inhabited.default} in the definition.

The syntax \li{[Inhabited α]} adds an implicit argument of the \li{head}
constant. But unlike for other implicit arguments, Lean performs a type class
search through all declared instances to determine the value of this argument.
Thus, when running the command
%
\lstinputlisting[linerange=head_eval-q]{../lean/LoVe/LoVe05_FunctionalProgramming_DemoMaster.lean}
%
Lean will look for an \li{Inhabited ℕ} instance and find
\hbox{\li{Nat.Inhabited},} the instance we declared above. In that declaration,
we set \hbox{\li{default}} to be \li{0} and hence this is what \li{#eval}
prints. If multiple instances are applicable and Lean chooses the wrong one, we
can use the \hbox{\li{@}} syntax to transform type class arguments into explicit
arguments and supply the desired type class instance.

Let us take a closer look at \li{Inhabited.default}:
%
\[\hbox{\lic|Inhabited.default {α : Type} [Inhabited α] : α|}\]
%
Notice that the selectors of plain structures use parentheses \hbox{\li{( )}}
whereas those of type classes use square brackets \li{[ ]}. When we used
\li{Inhabited.default α} to define \li{head}, Lean looked for an instance of
\li{Inhabited α} in the global table of registered instances and in the local
context. The global table contained an entry for \li{Inhabited ℕ} but none that
matched \hbox{\li{Inhabited α}.} On the other hand, the local context contained
an anonymous parameter of type \li{Inhabited α}, which could be used.

Lean's core library defines \li{List.head} exactly as we did. In practice,
almost all types are nonempty (with the notable exception of
\li{False}), so the \li{Inhabited} restriction is hardly an issue.

We can prove abstract theorems about the \li{Inhabited} type class, such as
%
\lstinputlisting[linerange=head_head-q]{../lean/LoVe/LoVe05_FunctionalProgramming_DemoMaster.lean}
%
The assumption \li{[Inhabited α]} is needed to use the operator \li{head} on
lists of type \li{List α}. If we omit this assumption, Lean will raise an error
telling us that type class synthesis failed.

There are more type classes with only a constant but no properties,
including
%
\begin{lstlisting}[multicols=2]
class Zero (α : Type) where
  zero : α

class Neg (α : Type) where
  neg : α → α

class Add (α : Type) where
  add : α → α → α
class One (α : Type) where
  one : α

class Inv (α : Type) where
  inv : α → α

class Mul (α : Type) where
  mul : α → α → α
\end{lstlisting}
%
These \emph{syntactic} type classes introduce constants that are used in
different contexts with different semantics. For example, \li{one} can stand
for the natural number~1, the integer~1, the real~1, the identity matrix, and
many other concepts of oneness. The main purpose of these type classes is to
form the foundation for a rich hierarchy of algebraic type classes (groups,
monoids, rings, fields, etc.)\ and to allow the overloading of common
mathematical symbols such as \li{+}, \li{*}, \li{0}, \li{1}, and \li{⁻¹}.

Syntactic type classes do not impose severe restrictions on the types that
can be declared instances. In contrast, the \emph{semantic} type classes contain
properties that restrict how the given constants behave.

In Section~\ref{sec:proofs-by-mathematical-induction}, we encountered the
following semantic type classes:
%
\begin{lstlisting}
class IsCommutative (α : Type) (f : α → α → α) where
  comm : ∀a b, f a b = f b a

class IsAssociative (α : Type) (f : α → α → α) where
  assoc : ∀a b c, f (f a b) c = f a (f b c)
\end{lstlisting}
%
This time, the associations are not from a type to a constant, but from a
type \emph{and a function} to a property. Lean does not mind the abuse:
Although they are called type classes, Lean's type classes are very flexible
and can be used to express all kinds of constraints.

Conceptually, \li{IsCommutative} is a dependent type of triples
\li{(α,} \li{f, comm)}, and similarly for \li{IsAssociative}. The type of \li{f}
depends on \li{α}, and the type of \li{comm} depends on \li{α} and \li{f}.
Although they are parameters, \li{α} and \li{f} are also stored along with
\li{comm}.
% But the type class mechanism treats the parameters differently from
% the fields: The parameters are treated as input to the type class search,
% whereas the fields are output.

In Section~\ref{sec:proofs-by-mathematical-induction}, we registered our
\li{add} function on \li{ℕ} as a commutative and associative operation:

\lstinputlisting[linerange=is_commutative_associative-q]{../lean/LoVe/LoVe03_BackwardProofs_DemoMaster.lean}
%
Whenever we try to access \li{@IsCommutative.comm ℕ add}, we obtain
\hbox{\li{add_comm},} and similarly for \li{@IsAssociative.assoc ℕ add}. The
\li{ac_rfl} tactic tries to look up the \li{comm} and \li{assoc} properties for all
binary operators in the problem and exploits the properties whenever they are
present.

The general syntax to define a type class is as follows:
%
\begin{quote}
\lic{class} {\color{procnamecolor}\,\ttvar{class-name}}
  \,\tabletbreak{\qquad}\lic{(}\ttvar{params}$_\texttt{1}$ \lic{:} \ttvar{type}$_\texttt{1}$\lic{)} $\ldots$
\lic{(}\ttvar{params}$_\ttvar{k}$ \lic{:} \rlap{\ttvar{type}$_\ttvar{k}$\lic{)}} \\
\noindent\hbox{}\quad$\bigl[$\lic{extends} \ttvar{structure}$_\texttt{1}$\lic{, …,} \ttvar{structure}$_\ttvar{m}\bigr]$
  %\,\lic{:}\, \ttvar{type}
  \,\lic{where} \\
\noindent\phantom{\lic{xx}}\ttvar{constant-name}$_\texttt{1}$ \,\lic{:}\, \ttvar{constant-type}$_\texttt{1}$ \\
\noindent\phantom{\lic{xxxx}}$\vdots$ \\
\noindent\phantom{\lic{xx}}\ttvar{constant-name}$_\ttvar{n}$ \,\lic{:}\, \ttvar{constant-type}$_\ttvar{n}$ \\
\noindent\phantom{\lic{xx}}\ttvar{property-name}$_\texttt{1}$ \,\lic{:}\, \ttvar{proposition}$_\texttt{1}$ \\
\noindent\phantom{\lic{xxxx}}$\vdots$ \\
\noindent\phantom{\lic{xx}}\ttvar{property-name}$_\ttvar{p}$ \,\lic{:}\, \ttvar{proposition}$_\ttvar{p}$
\end{quote}
%
The general syntax to instantiate a type class is as follows:
%
\begin{quote}
\lic{instance}\, {\color{procnamecolor}\,\ttvar{instance-name}} \,\tabletbreak{\qquad}\lic{:}\,
  \ttvar{type-class} \,\ttvar{arguments} \,\lic{:=} \\
\noindent\phantom{\lic{xx}}\lic${$ \ttvar{constant}$_\texttt{1}$ \,\lic{:=}\, \ttvar{definition}$_\texttt{1}$\lic{,} \\
\noindent\phantom{\lic{xx}}\phantom{\texttt{X} \phantom{co}}$\vdots$ \\
\noindent\phantom{\lic{xx}}\phantom{\texttt{X}} \ttvar{constant}$_\ttvar{n}$ \,\lic{:=}\, \ttvar{definition}$_\ttvar{n}$\lic{,} \\
\noindent\phantom{\lic{xx}}\phantom{\texttt{X}} \ttvar{property}$_\texttt{1}$ \,\lic{:=}\, \ttvar{proof}$_\texttt{1}$\lic{,} \\
\noindent\phantom{\lic{xx}}\phantom{\texttt{X} \phantom{co}}$\vdots$ \\
\noindent\phantom{\lic{xx}}\phantom{\texttt{X}} \ttvar{property}$_\ttvar{p}$ \,\lic{:=}\, \ttvar{proof}$_\ttvar{p}$ \lic$}$
\end{quote}

\section{Lists}
\label{sec:lists}

Lean provides a rich library of functions on finite lists. In this section, we
will review some of them, and we will define some of our own; these are good
exercises to familiarize ourselves with functional programming in Lean.

In the first example, we perform a case distinction on a list:
%
\lstinputlisting[linerange=head_head_cases-q]{../lean/LoVe/LoVe05_FunctionalProgramming_DemoMaster.lean}
%
The proof relies on \li{cases}, a relative of \hbox{\li{induction}.} It
performs a case distinction on its argument but does not generate induction
hypotheses. The invocation
\hbox{\li{cases}} \hbox{\li{xs}} transforms a goal \hbox{\li{⊢ P[xs]}} into two subgoals,
\li{⊢ P[[]]} and \li{⊢ P[x} \li{::} \hbox{\li{xs']}.}
We could also have used \li{induction xs}. If you
find yourself hesitating between \li{induction} and \li{cases}, you can always
choose \hbox{\li{induction}} and see afterwards if you needed the induction
hypotheses---if you did not need it, it is good style to document that fact by
replacing \li{induction} by \li{cases}.

In a structured proof, we can use \li{match} expressions to perform a case distinction:
%
\lstinputlisting[linerange=head_head_match-q]{../lean/LoVe/LoVe05_FunctionalProgramming_DemoMaster.lean}

In the next example, we show how to exploit injectivity of constructors. The
\li{cases} tactic uses injectivity to simplify equations in which both
sides have the same constructor applied. In the proof below, the equation
before simplification is \li{x ::} \li{xs = y :: ys}:
%
\lstinputlisting[linerange=injection_example-q]{../lean/LoVe/LoVe05_FunctionalProgramming_DemoMaster.lean}
%
The \li{cases} tactic replaces \li{y} by \li{x} and \li{ys}
by \li{xs} throughout the goal, yielding the subgoal
%
\[\hbox{\lic{⊢ x = x ∧ xs = xs}}\]
%
which \li{simp} can easily prove.

The \li{cases} tactic is also useful when the constructors are different, to
detect the impossible case:
%
\lstinputlisting[linerange=distinctness_example-q]{../lean/LoVe/LoVe05_FunctionalProgramming_DemoMaster.lean}

Next, we define the \emph{map function} on lists:\ a function that applies
its argument \li{f}---which is itself a function---to all elements stored in a
collection.

\lstinputlisting[linerange=map-q]{../lean/LoVe/LoVe05_FunctionalProgramming_DemoMaster.lean}
%
Notice that because \li{f} does not change in the recursive call, we put it in as
a parameter of the entire definition. The alternative, which is the only option
for arguments that change in recursive calls, would be as follows:

\lstinputlisting[linerange=map_args-q]{../lean/LoVe/LoVe05_FunctionalProgramming_DemoMaster.lean}

A basic property of map functions is that they have no effect if their argument
is the identity function (\li{fun x ↦ x}):

\lstinputlisting[linerange=map_ident-q]{../lean/LoVe/LoVe05_FunctionalProgramming_DemoMaster.lean}

Another basic property is that successive maps can be compressed into a single
map, whose argument is the composition of the functions involved:

\lstinputlisting[linerange=map_comp-q]{../lean/LoVe/LoVe05_FunctionalProgramming_DemoMaster.lean}

When introducing new operations, it is useful to show how these behave when
used in combination with other operations. An example follows:

\lstinputlisting[linerange=map_append-q]{../lean/LoVe/LoVe05_FunctionalProgramming_DemoMaster.lean}

Remarkably, the last three proofs are textually identical. These are typical
\li{induction}--\li{rfl}--\li{simp} proofs.

The next list operation removes the first element of a list, returning the tail:
%
\lstinputlisting[linerange=tail-q]{../lean/LoVe/LoVe05_FunctionalProgramming_DemoMaster.lean}
%
For \li{[]}, we simply return \li{[]} as its own tail.

The counterpart of \li{tail} is a function that extracts the first element of a
list. We already reviewed one solution in Section~\ref{sec:type-classes}, using
the \li{Inhabited} type class. Another possible definition uses an \li{Option}
wrapper:

\lstinputlisting[linerange=headOpt-q]{../lean/LoVe/LoVe05_FunctionalProgramming_DemoMaster.lean}
%
The type \li{Option α} has two constructors: \li{Option.}\allowbreak\li{none} and
\li{Option.}\allowbreak\li{some a}, where \li{a : α}. We use \li{Option.none}
when we have no meaningful value to return and \li{Option.some} otherwise. We
can think of \li{Option.none} as the null pointer of functional programming,
but unlike null pointers (and null references), the type system guards against
unsafe dereferences. To retrieve the value stored in an \hbox{\li{Option},} we
must pattern-match. Schematically:
%
\begin{center}
\begin{tabular}{@{}l@{}}
\licw$match headOpt xs with$ \\
\licw$  | Option.none   => handleTheError$ \\
\licw$  | Option.some x => doSomethingWithValue x$ \\
\end{tabular}
\end{center}
%
We cannot simply write \li{doSomethingWithValue (headOpt xs)}, because this
would be type-incorrect. The type system forces us to think about error
handling.

Using the power of dependent types, we have another way to implement a partial
function---namely, we can specify a precondition. The caller must then pass a
proof that the precondition is satisfied as argument:
%
\lstinputlisting[linerange=headPre-q]{../lean/LoVe/LoVe05_FunctionalProgramming_DemoMaster.lean}
%
The \li{headPre} function takes two explicit arguments. The first argument,
\li{xs}, is a list. The second argument, \li{hxs}, is a proof of \hbox{\li{xs ≠}} \li{[]}.
Since the type \li{xs ≠ []} of the second argument depends on the first
argument, we must use the dependent type syntax \hbox{\li{(xs : List}} \li{α) →} rather than
\li{List α →} so that we can name the first argument. The result of the function
is a value of type \li{α}; thanks to the precondition, there is no need for an
\li{Option} wrapper.

The second argument is used to rule out the case where \hbox{\li{xs}} is
\li{[]}. In that case, the argument (called \li{hxs}) is a proof of
\hbox{\li{[] ≠}} \li{[]}, which is impossible. The proof derives a contradiction
and exploits it to derive an arbitrary \li{α}. From a contradiction, we can
derive anything, even an inhabitant of \li{α}.

We can then invoke the function as follows:
%
\lstinputlisting[linerange=headPre_eval-q]{../lean/LoVe/LoVe05_FunctionalProgramming_DemoMaster.lean}
%
This prints \li{3}. The second argument, \li{by simp}, is a proof that
\hbox{\li{[3, 1,}} \li{4]} is not \li{[]}.

%Let us move on.
Now, given two lists
\li{[x}$_\texttt{1}$\li{,} $\ldots$, \li{x}$_\ttvar{n}$\li{]} and
\li{[y}$_\texttt{1}$\li{,} $\ldots$, \hbox{\li{y}$_\ttvar{n}$\li{]}}
of the same length, the zip operation constructs a list of pairs
\hbox{\li{[(x}$_\texttt{1}$\li{, y}$_\texttt{1}$\li{),}} $\ldots$,
\li{(x}$_\ttvar{n}$\li{, y}$_\ttvar{n}$\li{)]}:

\lstinputlisting[linerange=zip-q]{../lean/LoVe/LoVe05_FunctionalProgramming_DemoMaster.lean}
%
The function is also defined if one list is shorter than the other. For example,
\li{zip} \li{[a, b, c] [x, y] = [(a, x), (b, y)]}. Notice that the recursion,
with three cases, deviates from the structural recursion schema.

The length of a list is defined by recursion:
%
\lstinputlisting[linerange=length-q]{../lean/LoVe/LoVe05_FunctionalProgramming_DemoMaster.lean}
%
We can say something interesting about the length of \li{zip}'s
result---namely, it is the minimum of the lengths of the two input lists:

\lstinputlisting[linerange=length_zip-q]{../lean/LoVe/LoVe05_FunctionalProgramming_DemoMaster.lean}
%
The proof above teaches us yet another trick. The induction hypothesis
is
%
\[\hbox{\tabletfootnotesize\ctxt{ih}\lic| : ∀ys : list β, length (zip xs ys) = min (length xs) (length ys)|}\]
%
Why is there a \li|∀|~quantifier? The \hbox{\li{induction xs generalizing ys}} tactic
generalized the theorem statement so that the induction hypothesis is not
restricted to some fixed \li{ys} as the proof goal but can be used for arbitrary
values of \li{ys}. Such flexibility is needed here because we want to
instantiate the quantifier with \li{ys}'s tail (called \li{ys'}) and not with
\li{ys} itself.

The proof relies on a theorem about the \li{min} function that we need to prove
ourselves:
%
\lstinputlisting[linerange=min_add_add-q]{../lean/LoVe/LoVe05_FunctionalProgramming_DemoMaster.lean}
%
Recall the definition \li{min a b = (if a ≤ b then a else b)}. To
reason about \li{min}, we often need to perform a case distinction on the condition
\li{a ≤ b}. This is achieved using \li{cases Classical.em} \li{(a ≤ b)}. This
creates two subgoals:\ one with \li{a ≤ b} as a hypothesis and one
with \li{¬ a ≤ b}. The hypothesis is available in each case as \li{h}.

In a structured proof, there are two ways to perform a case distinction on a
proposition:
%
\lstinputlisting[linerange=min_add_add_match-q]{../lean/LoVe/LoVe05_FunctionalProgramming_DemoMaster.lean}
\betweenlistings
\lstinputlisting[linerange=min_add_add_if-q]{../lean/LoVe/LoVe05_FunctionalProgramming_DemoMaster.lean}

We see again that the mechanisms that are available to write functional
programs, such as \li{match} and \li{if}--\li{then}--\li{else}, are also
available for writing structured proofs (which are, after all, terms).
We can now add a few rows to the table presented at the end of
Section~\ref{sec:the-pat-principle}:

\vskip4\smallskipamount

\centerline{\tabletsmall\begin{tabular}{@{}p{11em}@{\enskip}p{11em}@{\enskip}p{11em}@{}}
\toprule
Tactical proof & Structured proof & Raw proof term \\
\midrule
\lic|cases t| & \lic|match t with| & \lic|match t with| \\
\lic|cases Classical.em Q|\kern-200em & \lic|if Q then … else| & \lic|if Q then … else| \\
\bottomrule
\end{tabular}}

\vskip4\smallskipamount

We conclude with a distributivity law about \li{map} and \li{zip}, expressed
using the \li{Prod.fst} and \li{Prod.snd} selectors on pairs:

\lstinputlisting[linerange=map_zip-q]{../lean/LoVe/LoVe05_FunctionalProgramming_DemoMaster.lean}
%
The patterns on the left correspond exactly to the patterns used in the
definition of \li{zip}. This is simpler than performing the induction on \li{xs}
and the case distinction on \li{ys} separately, as we did when we proved
\li{length_zip}. Good proofs often follow the structure of the definitions they
are based on.

In the definition of \li{zip} and in the proof of \li{map_zip}, we were careful
to specify three nonoverlapping patterns. It is also possible to write equations
with overlapping patterns, as in

\begin{lstlisting}
def f {α : Type} : List α → ⋯
  | [] => …
  | xs => … xs …
\end{lstlisting}
%
Since the patterns are applied sequentially, the above command defines the same
function as

\begin{lstlisting}
def f {α : Type} : List α → ⋯
  | []      => …
  | x :: xs => … (x :: xs) …
\end{lstlisting}
%
We generally recommend the latter, more explicit style, because it leads to
fewer surprises.

\section{Binary Trees}
\label{sec:binary-trees}

Inductive types with constructors taking several recursive arguments define
tree-like objects. \emph{Binary trees} have nodes with at most two children. Lean's
definition of binary trees follows:

\begin{lstlisting}
inductive Tree (α : Type) : Type
  | nil  : Tree α
  | node : α → Tree α → Tree α → Tree α
\end{lstlisting}
%
With binary trees, structural induction produces two induction hypotheses, one
for each subtree of an inner node. To prove a goal \li{t : Tree α ⊢ P[t]} by
structural induction on \li{t}, we need to show the subgoals
%
{\tabletsmall
\begin{align*}
& \hbox{\lic|\ ⊢ P[Tree.nil]|} \\
\hbox{\ctxt{a} \lic|: α,| \ctxt{l} \ctxt{r} \lic|: Tree α,| \ctxt{ih\_l} \lic|: P[l],| \ctxt{ih\_r} \lic|: P[r]|}
& \hbox{\lic|\ ⊢ P[Tree.node a l r]|}
\end{align*}}%
%
\noindent\kern\parindent
The tree counterpart to list reversal is the mirror operation:

\lstinputlisting[linerange=mirror-q]{../lean/LoVe/LoVe05_FunctionalProgramming_DemoMaster.lean}

Mirroring can be defined directly, without appealing to some append operation.
As a result, reasoning about \li{mirror} is simpler than reasoning about
\li{reverse}, as we can see below:

\lstinputlisting[linerange=mirror_mirror-q]{../lean/LoVe/LoVe05_FunctionalProgramming_DemoMaster.lean}

A more detailed informal proof is as follows:

\begin{quote}
The proof is by structural induction on \li{t}.

\textsc{Case} \li{Tree.nil}: We must show that
\li{mirror (mirror} \li{Tree.}\allowbreak\li{nil)} \hbox{\li{= Tree.nil}}. This follows
directly from the definition of \hbox{\li{mirror}.}

\textsc{Case} \li{Tree.node a l r}: \,The induction hypotheses are
{\tabletsmall
\begin{align*}
  & \text{(\li{ih_l})~\,\li{mirror (mirror l) = l}}
& & \text{(\li{ih_r})~\,\li{mirror (mirror r) = r}}
\end{align*}}%
%
We must show \li{mirror (mirror (Tree.node a l r)) = Tree.}\allowbreak\li{node a l} \li{r}. We
have

{\tabletsmall
\noindent\phantom{\li{=}}\, \li{mirror (mirror (Tree.node a l r))} \\
\li{=}\, \li{mirror (Tree.node a (mirror r) (mirror l))}
  \tabletbreak{}\hfill(by def.\ of \li{mirror}) \\
\li{=}\, \li{Tree.node a (mirror (mirror l)) (mirror (mirror r))}
  \tabletbreak{}\hfill(ditto) \\
\li{=}\, \li{Tree.node a l (mirror (mirror r))}
  \hfill(by \li{ih_l}) \\
\li{=}\, \li{Tree.node a l r}
  \hfill(by \li{ih_r}) \\
{\color{white}x} \qed}
\end{quote}
%
To achieve the same level of detail in the Lean proof, we could
use a calculational block (Section~\ref{sec:calculational-proofs})
instead of \li{simp}:

\lstinputlisting[linerange=mirror_mirror_calc-q]{../lean/LoVe/LoVe05_FunctionalProgramming_DemoMaster.lean}

We conclude with the following theorem, which will be useful in Chapter~\ref{chap:inductive-predicates}:

\lstinputlisting[linerange=mirror_eq_empty_iff-q]{../lean/LoVe/LoVe05_FunctionalProgramming_DemoMaster.lean}

\section{Cases Tactic}
\label{sec:cases-tactic}

\subsection*{cases}

\smallskip

\begin{quote}
\begin{tabular}{@{}l@{}}
\lic|cases| \,\ttvar{term} \,$\bigl[$\lic|with| \\
\lic$|$\, \ttvar{constructor}$_\texttt{1}$ \ttvar{names}$_\texttt{1}$
  \,\lic|=>|\, \ttvar{tactics}$_\texttt{1}$ \\
\noindent\hbox{}\phantom{\texttt{|}\, \ttvar{pa}}$\vdots$ \\
\lic$|$\, \ttvar{constructor}$_{\ttvar{n}}$ \ttvar{names}$_{\ttvar{n}}$
  \,\lic|=>|\, \ttvar{tactics}$_\ttvar{n}\bigr]$
\end{tabular}
\end{quote}
%
The \li{cases} tactic performs a case distinction on the specified term. This
gives rise to as many subgoals as there are constructors in the definition of
the term's type. The tactic is similar to \li{induction} except that it does
not produce induction hypotheses and it automatically excludes impossible cases.
%
The optional names \ttvar{names}$_\texttt{1}$, \ldots, \ttvar{names}$_\ttvar{n}$
are used for any emerging variables or hypotheses.

\begin{quote}
\lic{cases} \,\ttvar{hypothesis-of-the-form-l-equals-r}
\end{quote}
%
The \li{cases} tactic can also be used on a hypothesis~\li{h} of the form
\li{l = r}. It matches \li{r} against \li{l} and
replaces all occurrences of the variables occurring in
\li{r} with the corresponding terms in \li{l} everywhere in the goal. The
remaining hypothesis \li{l = l} can be removed using \li{clear h} if desired.

\begin{quote}
\begin{tabular}{@{}l@{}}
\lic|cases| \lic|Classical.em| \lic|(|\ttvar{proposition}\lic|)| \lic|with| \\
\lic$|$\, \lic|inl| \ttvar{name-if-true~}
  \,\lic|=>|\, \ttvar{tactics-if-true} \\
\lic$|$\, \lic|inr| \ttvar{name-if-false}
  \,\lic|=>|\, \ttvar{tactics-if-false}
\end{tabular}
\end{quote}
%
The \li{cases} tactic can also be used to perform a case distinction on a
proposition. Two cases emerge:\ one in which the proposition is true and one in
which it is false. The optional names \ttvar{name-if-true} and
\ttvar{name-if-false} are used for the hypothesis in the true and false cases,
respectively.

\section{Dependent Inductive Types}
\label{sec:dependent-inductive-types}

The inductive types \li{List α} and \li{Tree α} fall within the simply typed
fragment of Lean. Inductive types may also depend on (non-type) terms. A
typical example is the type of lists of length~\textit{n}, or \emph{vectors}:

\lstinputlisting[linerange=Vec-q]{../lean/LoVe/LoVe05_FunctionalProgramming_DemoMaster.lean}
%
Thus, the term \li{Vec.cons 3 (Vec.cons 1 Vec.nil)} has type
\li{Vec ℕ 2}. By encoding the vector length in the type, we can provide more
precise information about the result of functions. A function such as
\li{Vec.reverse}, which reverses a vector, would map a value \li{Vec α n}
to another value of the same type, with the same \li{n}. And \li{Vec.zip}
could require its two arguments to have the same length. Fixed-length vectors
and matrices are useful in computer science and mathematics.

Unfortunately, this more precise information comes at a cost. Dependent
inductive types cause difficulties when the terms they depend on are provably
equal but not syntactically equal up to computation (e.g., \li{m + n} vs.\
\li{n + m}). In this guide, we will generally avoid dependent inductive types.
They are briefly covered in this section for completeness. To put it
unambiguously: \relax{This is not exam material.}

The definitions below introduce conversions between lists and vectors:
%
\lstinputlisting[linerange=listOfVec-q]{../lean/LoVe/LoVe05_FunctionalProgramming_DemoMaster.lean}
\betweenlistings
\lstinputlisting[linerange=vecOfList-q]{../lean/LoVe/LoVe05_FunctionalProgramming_DemoMaster.lean}

The \li{listOfVec} conversion takes a type \li{α}, a length~\li{n}, and a
vector of length \li{n} over \li{α} as arguments and returns a list over
\hbox{\li{α}.} Although we do not care about the length \li{n}, it still needs to be
an argument because it appears in the type of the third argument. We make the first
two arguments, \li{α} and \li{n}, implicit since they can be inferred from the
type of the third argument.

The \li{vecOfList} conversion takes a type \li{α} and a list over \li{α} as
arguments and returns a vector of the same length as the list.
Lean's type checker is strong enough to determine that the two right-hand sides
have the desired type.

By the PAT principle, proofs are analogous to function definitions. Let us
verify that converting a vector to a list preserves its length:

\lstinputlisting[linerange=length_listOfVec-q]{../lean/LoVe/LoVe05_FunctionalProgramming_DemoMaster.lean}

To prove a goal \li{v : Vec α n ⊢ P[v]} by structural induction on \li{v}, we
might naively think that it suffices to show the following two subgoals:
%
\begin{align*}
& \hbox{\lic|\ ⊢ P[Vec.nil]|} \\
\hbox{\ctxt{m} \lic|: ℕ,| \ctxt{a} \lic|: α,| \ctxt{u} \lic|: Vec α m,| \ctxt{ih} \lic|: P[u]|}
  & \hbox{\lic|\ ⊢ P[Vec.cons a u]|}
\end{align*}
%
This is naive because the subgoals are not even type-correct:
The hole in \hbox{\li{P[ ]}} has type \li{Vec α n} (the type of its original
dweller, \hbox{\li{v}),} so we cannot simply plug \hbox{\li{Vec.nil},} \li{u}, or
\li{Vec.cons a u}---which have types \li{Vec α 0}, \li{Vec α m}, and
\li{Vec α} \hbox{\li{(m + 1)}}---into that hole. We must massage \li{P} each time,
replacing \li{n} with \li{0}, \li{m}, or \li{m + 1}. Using
the notation \li{P}$_\texttt{t}$\li{[ ]} for the variant of \li{P[ ]} where all
occurrences of \li{n} are replaced by term \li{t}, we get
%
\begin{align*}
& \hbox{\lic|\ ⊢ P|$_\texttt{0}$\li|[Vec.nil]|} \\
\hbox{\ctxt{m} \lic|: ℕ,| \ctxt{a} \lic|: α,| \ctxt{u} \lic|: Vec α m,| \ctxt{ih} \lic|: P|$_\texttt{m}$\lic|[u]|}
  & \hbox{\lic|\ ⊢ P|$_\texttt{m+1}$\li|[Vec.cons a u]|}
\end{align*}

Proofs by case distinction using the \li{cases} tactic are similar,
but without the induction hypothesis. Often, the length \li{n} will be not
a variable but a complex term. Then the replacement of \li{n} in \li{P[ ]}
might not be intuitively meaningful. With \hbox{\li{cases},} the corresponding
subgoal is silently eliminated. Thus, a case distinction on a value of type
\hbox{\li{Vec α 0}} will yield only one subgoal, of the form
\li{⊢} \li{P[Vec.nil]}, since \li{0} could never be equal to a term of the form
\li{m + 1}.

Dependently typed pattern matching is subtle, because the type of the value we
match on may change according to the constructor. Given \li{v : Vec α n}, we
might be tempted to write
%
\begin{center}
\begin{tabular}{@{}l@{}}
\licw$match v with$ \\
\licw$| Vec.nil      => …$ \\
\licw$| Vec.cons a u => …$
\end{tabular}
\end{center}
%
but this is just as naive as our first induction proof attempt above. Since
the term \li{n} in the type \li{Vec α n} may change depending on the
constructor, we must pattern-match on \li{n} as well:
%
\begin{center}
\begin{tabular}{@{}l@{}}
\licw$match n, v with$ \\
\licw$| 0,     Vec.nil      => $\li$…$ \\
\licw$| m + 1, Vec.cons a u => $\li$…$
\end{tabular}
\end{center}
%
Showing the implicit arguments, we have
%
\begin{center}
\begin{tabular}{@{}l@{}}
\licw$match n, v with$ \\
\licw$| 0,     @Vec.nil α        => $\li$…$ \\
\licw$| m + 1, @Vec.cons α a m u => $\li$…$
\end{tabular}
\end{center}
%
Often, it is sufficient to put placeholders in the first column:
%
\begin{center}
\begin{tabular}{@{}l@{}}
\licw$match n, v with$ \\
\licw$| _, Vec.nil      => …$ \\
\licw$| _, Vec.cons a u => …$
\end{tabular}
\end{center}
%
It may seem paradoxical to pattern-match on \li{n} only to ignore the result,
but without it Lean cannot infer the second implicit argument of
\li{Vec.cons}. In this respect, \li{cases} is more user-friendly than
\li{match}.

%Incidentally, Lean's core libraries define a type of fixed-length vectors,
%called \li{vector α n}, as a subtype of \li{List α}:
%
%\begin{lstlisting}
%def vector (α : Type) (n : ℕ) :=
%  {xs : list α // List.length xs = n}
%\end{lstlisting}
%
%In other words, the type \li{vector α n} consists of the values \li{xs} of type
%\li{List α} such that \li{xs} is of length \li{n}. This makes it possible to
%reuse Lean's extensive list library. Subtyping will be explained in
%Chapter~\ref{chap:logical-foundations-of-mathematics}.

\section{Summary of Newly Introduced Lean Constructs}

\begingroup
\summarysize

\subsection*{Declarations}

\noindent
\begin{xltabular}{\textwidth}{@{}p{9em}X@{}}
\lic{class} & declares a structure type as a type class \\
\lic{instance} & declares a structure value as a type class instance \\
\lic{structure} & introduces a structure type and its selectors \\
\end{xltabular}

\subsection*{Expressions}

\noindent
\begin{xltabular}{\textwidth}{@{}p{9em}X@{}}
\lic{if} $\dots$ \lic{then} $\dots$ \rlap{\lic{else}}
  & performs a case distinction on a decidable proposition \\
\lic{match} $\dots$ \lic{with} & performs pattern matching \\
\end{xltabular}

\subsection*{Tactic}

\noindent
\begin{xltabular}{\textwidth}{@{}p{9em}X@{}}
\lic|cases| & performs a case distinction \\
\end{xltabular}

\endgroup
