\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~9 of \emph{Theorem Proving in Lean}
\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. Already in
Chapter~\ref{chap:definitions-and-statements}, we saw some basic inductive
types:\ the natural numbers, the finite lists, and a type of arithmetic
expressions. 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/love01_definitions_and_statements_demo_master.lean}
%
This definition introduces three constants, which could have been
declared as follows:
%
\begin{lstlisting}
constant nat : Type
constant nat.zero : nat
constant nat.succ : nat → nat
\end{lstlisting}
%
In addition, the inductive definitions asserts some properties about
\li{nat.zero} and \li{nat.succ}, which is why we use the \hbox{\li{inductive}}
command. It also 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 exist 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},%
\footnote{We could try to cheat and axiomatize special constants using
\li{constant} and \li{axiom}, but the result would be either tautological (i.e.,
useless) or contradictory (i.e., positively harmful). A safer but equally
pointless alternative would be to locally assume the existence of such a
value; this would be pointless because the assumption could never be
discharged.}
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. These 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}.

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.

Regardless of the 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, because these require us to understand what we
are doing:

\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
\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 lemmas 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/love04_functional_programming_demo_master.lean}
%
The routine reasoning about constructors is all carried out by \li{simp}
automatically, which is usually what we want.

We can supply our own names, and reorder the cases, by using the \li{case}
tactic in front of each case, together with the case's name and the desired
names for the variables and hypotheses introduced by \li{induction'}. For
example:
%
\lstinputlisting[linerange=nat.succ_neq_self₂-q]{../lean/love04_functional_programming_demo_master.lean}
%
Instead of \li{n} and \li{ih}, we chose the names \li{m} and \li{IH}.

\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.
This is a prerequisite for establishing that the function terminates, an
important property to ensure both logical consistency and termination of
evaluation.

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 fact₂ : ℕ → ℕ
| 0       := 0
| 1       := 1
| (n + 1) := (n + 1) * fact₂ 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/love04_functional_programming_demo_master.lean}
%
If Lean were to accept this definition, we could exploit it to prove that
\li{0 = 1}, by subtracting \li{illegal n} on each side of the equation
\li{illegal n = illegal n + 1}. From \li{0 = 1}, we could derive \li{false},
and from \li{false}, we could derive anything, including the three-color
theorem. Clearly, we do not want that.

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

Another reason for preferring \li{def} is that the defining equations are
used to compute. Tactics such as \li{refl} that unify up to computation become
stronger each time we introduce a definition, and the diagnosis 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} shockingly returns \li{0} regardless of the
argument, and \li{fact₂ 0} should give \li{1}, not \li{0}. We quite literally
\li{fact}ed up. These embarrassing mistakes remind us to \emph{test} our
definitions and \emph{prove} some properties about them. 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| \\
\lic$|$\, \ttvar{pattern}$_\texttt{11}$\li|,| $\ldots$\li|,|
  \ttvar{pattern}$_{\texttt{1}\ttvar{m}}$
  \,\lic|:=|\, \ttvar{result}$_\texttt{1}$ \\
\noindent\hbox{}\phantom{\texttt{|}\, \ttvar{pa}}$\vdots$ \\
\lic$|$\, \ttvar{pattern}$_{\ttvar{n}\texttt{1}}$\li|,| $\ldots$\li|,|
  \ttvar{pattern}$_\ttvar{nm}$
  \,\lic|:=|\, \ttvar{result}$_\ttvar{n}$ \\
\lic|end|
\end{tabular}
\end{center}
%
The construct is vaguely reminiscent of \li{switch} in many 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}

Notice the differences with the pattern matching syntax in \li{def}: The
patterns are separated by commas and not by spaces. This reduces the number of
required parentheses. 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/love04_functional_programming_demo_master.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{ff} and \li{tt}.%
\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
to avoid relying on such implicit coercions. There is unfortunately no way to
disable them.}
The connectives are called \li{bor} (infix:\ \li{||}), \li{band} (infix:\
\li{&&}), \li{bnot}, and \li{bxor}.

The following diagram shows the interpretations of \li{bool} and
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. We see that \li{bool} are interpreted as a set with two values,
whereas \li{Prop} consists in 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:logical-foundations-of-mathematics}.

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/love04_functional_programming_demo_master.lean}
%
This requires a decidable (i.e., executable) proposition. This is
the case for \li{≤}: Given concrete values for the arguments, such as \li{35}
and \li{49}, Lean can reduce \li{35 ≤ 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 records, or \emph{structures} as
they are also called. These are essentially nonrecursive single-constructor
inductive types but 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/love04_functional_programming_demo_master.lean}
%
This definition has roughly the same effect as the following commands:
%
\lstinputlisting[linerange=rgb_as_inductive-q]{../lean/love04_functional_programming_demo_master.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/love04_functional_programming_demo_master.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{:=} \\
\lic{(}\ttvar{f{}ield-names}$_\texttt{1}$ \,\lic{:}\, \ttvar{f{}ield-type}$_\texttt{1}$\lic{)} \\
\noindent\hbox{}\phantom{\lic{(}\,\ttvar{co}}$\vdots$ \\
\lic{(}\ttvar{f{}ield-names}$_\ttvar{n}$ \,\lic{:}\, \ttvar{f{}ield-type}$_\ttvar{n}$\lic{)}
\end{quote}
%
The parameters \ttvar{params}$_\texttt{1}$, \ldots, \ttvar{params}$_\ttvar{k}$
are effectively additional fields, but unlike the fields
\ttvar{f{}ield-names}$_\texttt{1}$, \ldots, \ttvar{f{}ield-names}$_\ttvar{n}$,
they are also stored in the type, as arguments to the type constructor
(\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/love04_functional_programming_demo_master.lean}
%
The definition of \li{semitransparent_red} copies all the values from
\li{pure_red} (indicated by the \li{..pure_red} syntax) except for the
\li{alpha} field, which it overrides.

Next, we define an operation called \li{shuffle}:
%
\lstinputlisting[linerange=shuffle_def-q]{../lean/love04_functional_programming_demo_master.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 these
forms in Lean's output, even if we do not use them 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/love04_functional_programming_demo_master.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. For \li{rgb}, the invocation
\li{cases' c} transforms a goal \li{⊢ P[c]} into a single subgoal, \li{r g b : ℕ}
\hbox{\li{⊢ P[rgb.mk r g b]}.} We could also have used \li{induction' c}. If you
find yourself hesitating between \li{induction'} and \li{cases'}, you can always
choose \li{induction'} and see afterwards if you needed the induction
hypotheses. If you did not, it is good style to document that fact by
substituting \li{cases'} for \li{induction'}.

In a structured proof, we can use \li{match} expressions to perform a case distinction.
For example:
%
\lstinputlisting[linerange=shuffle_shuffle_shuffle₂-q]{../lean/love04_functional_programming_demo_master.lean}
%
Recall from Section~\ref{sec:reasoning-about-equality} that \li{eq.refl} is the
property \li{∀a, a = a}.

\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. 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.%
\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 simple example is the type class \li{inhabited}, which requires only a
constant \li{inhabited.default} and no properties:
%
\begin{lstlisting}
@[class] structure inhabited (α : Type) : Type :=
(default : α)
\end{lstlisting}
%
The syntax is the same as for structures, except with the attribute
\li{@[class]} in front. The parameter \li{α} represents an arbitrary type that
could be a member of this class.

Any type that has at least one element can be registered as an instance of this
class. For example, we can register \li{ℕ} by choosing an
arbitrary number to be the default value:
%
\lstinputlisting[linerange=inhabited_nat-q]{../lean/love04_functional_programming_demo_master.lean}
%
This specifies a value called \li{nat.inhabited} of type
\hbox{\li{inhabited ℕ}.} Thanks to the \li{@[instance]} attribute, 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/love04_functional_programming_demo_master.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, recall 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{α → β} is inhabited if either (1)~\li{β} is inhabited or
(2)~\li{α} is \emph{not} inhabited. Case~(1) is easy:
%
\lstinputlisting[linerange=fun.inhabited_1-q]{../lean/love04_functional_programming_demo_master.lean}
%
The instance relies itself on an instance of the same type class but on a
different type. This frequently occurs and is part of the reason why we speak
of type class \emph{search} and not lookup.

For case~(2), there is no type class for \emph{non}inhabitation, but we know
that the type \li{empty} is not inhabited, so it will do:
%
\lstinputlisting[linerange=fun.inhabited_2-q]{../lean/love04_functional_programming_demo_master.lean}
%
Notice the trivial \li{match} that implements the body of a function that can
never be called, because no value of type \li{empty} can be passed as argument.
The definition of \li{empty} has zero introduction rules, so the corresponding
\li{match} has zero cases.

Finally, the type \li{α × β} of pairs, also called product type, contains values
of the form \li{(a, b)}, where \li{a : α} and \li{b : β}. Given a pair~\li{ab},
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/love04_functional_programming_demo_master.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/love04_functional_programming_demo_master.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 to the \li{head}
constant. But unlike for other implicit arguments, Lean performs not only type
inference but also 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/love04_functional_programming_demo_master.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. This is the main reason
why we give names to the type class instances.

Let us take a closer look at \li{inhabited.default}:
%
\[\hbox{\lic{inhabited.default (α : Type) [i : 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 exceptions of \li{empty} and
\li{false}), so the \li{inhabited} restriction is hardly an issue. Regardless,
lists over empty types are uninteresting---the only possible value is \li{[]}.

We can prove abstract lemmas about the \li{inhabited} type class, such as
%
\lstinputlisting[linerange=head_head-q]{../lean/love04_functional_programming_demo_master.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 has_zero (α : Type) :=
(zero : α)

class has_neg (α : Type) :=
(neg : α → α)

class has_add (α : Type) :=
(add : α → α → α)
class has_one (α : Type) :=
(one : α)

class has_inv (α : Type) :=
(inv : α → α)

class has_mul (α : Type) :=
(mul : α → α → α)
\end{lstlisting}
%
These \emph{syntactic} type classes introduce constants that are used in many
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~1. The main purpose of these type classes is to form the
foundation for a rich hierarchy of algebraic type classes (groups, monoids,
ring, 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 serious restrictions on the types that
can be declared instances, except that a type of type class \li{has_zero} or
\li{has_one} must be inhabited. 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 type classes:
%
\begin{lstlisting}
class is_commutative (α : Type) (f : α → α → α) :=
(comm : ∀a b, f a b = f b a)

class is_associative (α : Type) (f : α → α → α) :=
(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 sorts of constraints.

Conceptually, \li{is_commutative} is a dependent type of triples
\li{(α, f, comm)}, and similarly for \li{is_associative}. 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 \emph{input} to the type class
search, whereas the fields are \emph{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/love02_backward_proofs_demo_master.lean}
%
Whenever we try to access \li{@is_commutative.comm ℕ add}, we obtain
\li{add_comm}, and similarly for \li{@is_associative.assoc ℕ add}. The \li{cc}
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] structure} {\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{:=} \\
\lic{(}\ttvar{constant-names}$_\texttt{1}$ \,\lic{:}\, \ttvar{constant-type}$_\texttt{1}$\lic{)} \\
\noindent\hbox{}\phantom{\lic{(}\,\ttvar{co}}$\vdots$ \\
\lic{(}\ttvar{constant-names}$_\ttvar{n}$ \,\lic{:}\, \ttvar{constant-type}$_\ttvar{n}$\lic{)} \\
\lic{(}\ttvar{property-names}$_\texttt{1}$ \,\lic{:}\, \ttvar{proposition}$_\texttt{1}$\lic{)} \\
\noindent\hbox{}\phantom{\lic{(}\,\ttvar{co}}$\vdots$ \\
\lic{(}\ttvar{property-names}$_\ttvar{p}$ \,\lic{:}\, \ttvar{proposition}$_\ttvar{p}$\lic{)}
\end{quote}
%
The general syntax to instantiate a type class is as follows:
%
\begin{quote}
\lic{@[instance] def}\, {\color{procnamecolor}\,\ttvar{instance-name}} \,\tabletbreak{\qquad}\lic{:}\,
  \ttvar{type-class} \,\ttvar{arguments} \,\lic{:=} \\
\noindent\hbox{}\,\lic${$ \ttvar{constant}$_\texttt{1}$ \,\lic{:=}\, \ttvar{definition}$_\texttt{1}$\lic{,} \\
\noindent\hbox{}\,\phantom{\texttt{X} \phantom{co}}$\vdots$ \\
\noindent\hbox{}\,\phantom{\texttt{X}} \ttvar{constant}$_\ttvar{n}$ \,\lic{:=}\, \ttvar{definition}$_\ttvar{n}$\lic{,} \\
\noindent\hbox{}\,\phantom{\texttt{X}} \ttvar{property}$_\texttt{1}$ \,\lic{:=}\, \ttvar{proof}$_\texttt{1}$\lic{,} \\
\noindent\hbox{}\,\phantom{\texttt{X} \phantom{co}}$\vdots$ \\
\noindent\hbox{}\,\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 show how to exploit injectivity of constructors. The
\li{cases'} tactic can be used to exploit injectivity to simplify equations in which both
sides have the same constructor applied. In the proof below, the equation
before simplification is \li{x :: xs = y :: ys}:
%
\lstinputlisting[linerange=injection_example-q]{../lean/love04_functional_programming_demo_master.lean}
%
As a result of the case distinction, \li{y} is replaced by \li{x} and \li{ys}
is replaced by \li{xs} throughout the goal, yielding the subgoal
%
\[\hbox{\ctxt{h} \lic{: x :: xs = x :: xs ⊢ x = x ∧ xs = xs}}\]
%
The \li{clear h} tactic removes the useless hypothesis
\li{h : x :: xs = x :: xs}.

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

The first operation we define is a \emph{map function}:\ a function that applies
its argument \li{f}---which is itself a function---to all elements stored in a
container.

\lstinputlisting[linerange=map-q]{../lean/love04_functional_programming_demo_master.lean}
%
Notice that because \li{f} does not change in the recursive call, we put it as
a parameter of the entire definition. This means we must write \li{map xs} and
not \li{map f xs} in the recursive call. However, when using the function
later, we need to pass an argument for \li{f}. The alternative, which is the
only option for arguments that change in recursive calls, would be as follows:

\lstinputlisting[linerange=map₂-q]{../lean/love04_functional_programming_demo_master.lean}

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

\lstinputlisting[linerange=map_ident-q]{../lean/love04_functional_programming_demo_master.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/love04_functional_programming_demo_master.lean}

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

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

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

The next list operation removes the first element of a list, returning the tail:
%
\lstinputlisting[linerange=tail-q]{../lean/love04_functional_programming_demo_master.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}.
Another possible definition uses an \li{option} wrapper:

\lstinputlisting[linerange=head_opt-q]{../lean/love04_functional_programming_demo_master.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 head_opt xs with$ \\
\licw$| option.none   := handle_the_error$ \\
\licw$| option.some x := do_something_with_value x$ \\
\licw$end$
\end{tabular}
\end{center}
%
We cannot simply write \li{do_something_with_value (head_opt xs)}, because this
would be type-incorrect. The type system forces us to think about error
handling.

Using the power of dependent types, another way to implement a partial function
is to specify a precondition. The callee must then pass a proof that the
precondition is satisfied as argument:
%
\lstinputlisting[linerange=head_pre-q]{../lean/love04_functional_programming_demo_master.lean}
%
The \li{head_pre} function takes two explicit arguments. The first argument,
\li{xs}, is a list. The second argument, \li{hxs}, is a proof of \li{xs ≠ []}.
Since the type (\li{xs ≠ []}) of the second argument depends on the first
argument, we must use the dependent type syntax \li{∀xs : list α,} rather than
\li{list α →} to 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 precondition \li{hxs} is used to rule out the case where \hbox{\li{xs}} is
\li{[]}. In that case, \li{hxs} is a proof of \li{[] ≠ []}, which is
impossible. The \li{cc} tactic derives the 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=head_pre_eval-q]{../lean/love04_functional_programming_demo_master.lean}
%
This prints \li{3}.

Let us move on. 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/love04_functional_programming_demo_master.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 slightly from the structural recursion schema.

The length of a list is defined by recursion:
%
\lstinputlisting[linerange=length-q]{../lean/love04_functional_programming_demo_master.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/love04_functional_programming_demo_master.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)|}\]

The syntax \li|∀{β}| is new but suggestive: It indicates that the type \li|β|
is an implicit argument of \li{ih}. In contrast, \li{ys} is explicit---and from
it, \li|β| can be inferred.

Why are there \li|∀|-quantifiers? The \li{induction'}
tactic automatically generalized the lemma statement so that the induction
hypothesis is not restricted to same fixed \li{β} and \li{ys} as the proof goal
but can be used for arbitrary values of \li{β} and \li{ys}. Such flexibility is
rarely needed for types (e.g., \li{β}), but here we need it for \li{ys},
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 lemma about the \li{min} function that we need to prove
ourselves:
%
\lstinputlisting[linerange=min_add_add-q]{../lean/love04_functional_programming_demo_master.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}.

Here are two different ways to perform a case distinction on a proposition in a
structured proof:
%
\lstinputlisting[linerange=min_add_add₂-q]{../lean/love04_functional_programming_demo_master.lean}
\betweenlistings
\lstinputlisting[linerange=min_add_add₃-q]{../lean/love04_functional_programming_demo_master.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
\li|cases' t,| & \lic|match t with _ end| & \lic|match t with _ end| \\
\li|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/love04_functional_programming_demo_master.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, especially in proofs.

\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. A
possible definition of binary trees follows:

\lstinputlisting[linerange=btree-q]{../lean/love04_functional_programming_demo_master.lean}
%
(The \verb|{}| annotation is often used with nullary constructors of
polymorphic types. It indicates that all parameters---here, \li{α}---should be
implicitly derived from the context. This enables us to write \li{tree.empty}
instead of \li{tree.empty _}, or \li{tree.}\allowbreak\li{empty ℕ}, etc.)

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.empty]|} \\
\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/love04_functional_programming_demo_master.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/love04_functional_programming_demo_master.lean}

A more detailed informal proof would be as follows:

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

\textsc{Case} \li{tree.empty}: We must show that
\li{mirror (mirror} \li{tree.empty) =} \hbox{\li{tree.empty}}. 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.node a l 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₂-q]{../lean/love04_functional_programming_demo_master.lean}

The following lemma will be useful in Chapter~\ref{chap:inductive-predicates}:

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

\section{Case Distinction and Induction Tactics}
\label{sec:case-distinction-and-induction-tactics}

The following tactics are useful when performing case distinctions, with or
without induction hypotheses.

\subsection*{cases$\pmb{'}$}

\smallskip

\begin{quote}
\lic{cases'} \,\ttvar{term} $\bigl[$\li{with}
  \ttvar{name}$_\texttt{1}$ $\ldots$
  \ttvar{name}$_\ttvar{n}\bigr]$
\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 behaves roughly the same as \li{induction'} except
that it does not produce induction hypotheses and it eliminates impossible
cases.

The optional names \ttvar{name}$_\texttt{1}$, \ldots, \ttvar{name}$_\ttvar{n}$
are used for any emerging variables or hypotheses, to override the default
names.

Note that the standard Lean tactic for case distinction is called \li{cases}.
The primed variant is provided by \li{mathlib}. It is more user-friendly and is
the only one we will use.

\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.
If \li{r} fails to match \li{l}, no subgoals emerge; the proof is complete.

\begin{quote}
\lic{cases'} \lic{classical.em} \lic{(}\ttvar{proposition}\lic{)} $\bigl[$\li{with}
  \ttvar{name}$_\texttt{1}$
  \ttvar{name}$_\texttt{2}\bigr]$
\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}$_\texttt{1}$ and
\ttvar{name}$_\texttt{2}$ are used for hypotheses in the true and false cases,
respectively.

\subsection*{case}

\smallskip

\begin{quote}
\lic{case} \,\ttvar{name}
  $\bigl[$\li{:} \ttvar{name}$_\texttt{1}$ $\ldots$ \ttvar{name}$_\ttvar{n}\bigr]$
  \lic|{| \\
\noindent\hbox{}\phantom{\li{xx}}\li|… }|
\end{quote}
%
The \li{case} tactic (with no \li{s}) can be used in tandem with \li{cases'} or
\li{induction'} to select a subgoal corresponding to the constructor called
\ttvar{name} and focus on it.

The optional names \ttvar{name}$_\texttt{1}$, \ldots, \ttvar{name}$_\ttvar{n}$
are used for any emerging variables or hypotheses, to override the default
names.

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

The inductive types \li{list α} and \li{btree α} 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/love04_functional_programming_demo_master.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 also useful in 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=list_of_vec-q]{../lean/love04_functional_programming_demo_master.lean}
\betweenlistings
\lstinputlisting[linerange=vec_of_list-q]{../lean/love04_functional_programming_demo_master.lean}

The \li{list_of_vec} 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
\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. The first
two arguments are implicit, which is reasonable since they can be inferred from
the type of the third argument.

The \li{vec_of_list} 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_list_of_vec-q]{../lean/love04_functional_programming_demo_master.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{⊢ 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 := …$ \\
\licw$end$
\end{tabular}
\end{center}
%
but this is just as naive as our first induction proof attempt above. Because
the term \li{n} in the type \li{vec α n} may change depending on the
constructor, we must pattern-match on it 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$…$ \\
\licw$end$
\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$…$ \\
\licw$end$
\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 := …$ \\
\licw$end$
\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 to
\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 New Lean Constructs}

\begingroup
\summarysize

\subsection*{Declaration}

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

\subsection*{Attributes}

\noindent
\begin{xltabular}{\textwidth}{@{}p{9em}X@{}}
\li|@[class]| & declares a structure type as a type class \\
\li|@[instance]| & registers a structure value as a type class instance \\
\end{xltabular}

\subsection*{Term Language}

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

\subsection*{Tactics}

\noindent
\begin{xltabular}{\textwidth}{@{}p{9em}X@{}}
\lic|case| & focuses on a subgoal and names its variables and \hbox{hypotheses} \\
\lic|cases'| & performs a case distinction \\
\end{xltabular}

\endgroup
