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

We take a closer look at the basics of typed functional programming:
inductive types, pattern matching, recursive functions, and proofs by
induction. 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 datatypes of typed functional
programming languages (e.g., Haskell, ML, OCaml). As we saw in
Chapter~\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$ or \li{ε} that cannot be expressed using a finite combination of
\li{zero} and \li{succ}, and ``no confusion'' ensures that \li{zero} ≠
\li{succ n} for all \li{n}. In addition, inductive types are always finite.
The infinite term \li{succ (succ (succ …))} is not a value, nor does there
exist a number \li{n} such that \li{n = succ n}.

Already in Chapter~\ref{chap:definitions-and-lemma-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 some
new types.

\section{Example: Lists}
\label{sec:example-lists}

We first define the reverse of a list, exploiting the predefined concatenation
operator \li{++}:

\lstinputlisting[linerange=reverse_def-q]{../lean/love04_functional_programming_demo_master.lean}
%
(In fact, \li{reverse} exists in Lean's standard library, as
\li{list.reverse}, but our definition is more suitable for reasoning.)
A nice property to prove is that \li{reverse} is its own inverse:
\li{reverse (reverse xs) = xs} for all lists \li{xs}. However, if we try to
prove it by induction, we quickly run into an obstacle. For the induction
step, the goal to prove is
%
\[\hbox{\li{reverse (reverse xs ++ [x]) = x :: xs}}\]
%
and the induction hypothesis is
%
\[\hbox{\li{∀xs : list α, reverse (reverse xs) = xs}}\]
%
We need a way to ``distribute'' \li{reverse} over \li{++}, to eliminate the
occurrence of \li{++ [x]} and obtain a term that matches the induction
hypothesis's left-hand side. The trick is to prove and use the following
lemma:

\lstinputlisting[linerange=reverse_append-q]{../lean/love04_functional_programming_demo_master.lean}
%
It is important to state the lemma generally, for all \li{xs} and \li{ys}. If
we put \li{[y]} instead of \li{ys}, we would run into difficulties when
proving the lemma's induction step. In general, finding the right inductions
and lemmas can be a difficult task, which requires thought and creativity.

With the \li{reverse_append} lemma in place, we can prove our initial goal
by a straightforward induction:

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

The next 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 would 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}
%
Notice the use of \li{_} as a nameless placeholder in the first case. We could
also have given the variable a name (e.g., \li{f}).

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 are two examples:

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

The length of a list is defined by recursion:

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

The next 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 \li{bool}, not
\li{Prop}. As a general rule, we will use type \li{bool}, of Booleans, when
specifying programs and use the type \li{Prop}, of propositions, when stating
properties of programs. The two values of type \li{bool} are called \li{tt} and
\li{ff}. The connectives are called \li{bor} (infix: \li{||}), \li{band}
(infix: \li{&&}), \li{bnot}, and \li{bxor}.

The \li{match} construct has the following general syntax:
%
\begin{quote}
\li{match} \,\texttt{\itshape term}$_\texttt{1}$\li{,} $\ldots$\li{,}
  \texttt{\itshape term}$_\texttt{\itshape m}$ \,\li{with} \\
\li{|}\, \texttt{\itshape patterns}$_\texttt{11}$\li{,} $\ldots$\li{,}
  \texttt{\itshape pattern}$_\texttt{1\itshape m}$
  \,\li{:=}\, \texttt{\itshape result}$_\texttt{1}$ \\
\noindent\hbox{}\phantom{\li{|}\, \texttt{\itshape pa}}$\vdots$ \\
\li{|}\, \texttt{\itshape patterns}$_\texttt{{\itshape n}1}$\li{,} $\ldots$\li{,}
  \texttt{\itshape pattern}$_\texttt{\itshape nm}$
  \,\li{:=}\, \texttt{\itshape result}$_\texttt{\itshape n}$ \\
\li{end}
\end{quote}
%
Notice the differences with the pattern matching syntax in \li{def} and
\li{lemma}: The patterns are separated by commas and not by spaces. This reduces
the number of required parentheses. The patterns may contain variables,
constructors, and \li{_} placeholders. The
\texttt{\itshape result}$_\texttt{\itshape i}$ expressions may refer to the
variables introduced in the corresponding patterns.

The next list operation extracts the first element of a list:

\lstinputlisting[linerange=head-q]{../lean/love04_functional_programming_demo_master.lean}
%
Because an empty list contains no elements, there is no meaningful value we can
return in that case. For this reason, we use an \li{option}. The type
\li{option α} has two constructors: \li{none : option α} and
\li{some : α → option α}. We use \li{none} when we have no meaningful value to
return and \li{some} otherwise.

Given two lists of the same length
\li{[x}$_\texttt{1}$\li{,} $\ldots$, \li{x}$_\texttt{\itshape n}$\li{]} and
\li{[y}$_\texttt{1}$\li{,} $\ldots$, \li{y}$_\texttt{\itshape n}$\li{]},
the zip operation constructs a list of
pairs
\li{[(x}$_\texttt{1}$\li{, y}$_\texttt{1}$\li{),} $\ldots$,
\li{(x}$_\texttt{\itshape n}$\li{, y}$_\texttt{\itshape 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 [a, b, c] [x, y] = [(a, x), (b, y)]}.

Pairs are written using traditional notations. The type constructor \li{×},
which occurs in the result type \li{list (α × β)}, has an infix syntax. The
pair constructor is written using the syntax \li{(t, u)}, where \li{t} and
\li{u} are the arguments. Given a pair~\li{p}, the first and second components
can be extracted by writing \li{p.fst} and \li{p.snd} or \li{p.1} and
\li{p.2}.

The \li{p.1} and \li{p.2} syntaxes are used below to state a distributivity law
about \li{map} and \li{zip}:

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

We can also say something interesting about the length of the result of
\li{zip}---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 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}

The \li{min} function is defined such that
\li{min a b = (if a ≤ b then a else b)}. To reason about it, we often need to
perform a case analysis on the condition \li{a ≤ b}. This is achieved using
\li{by_cases}. Given a condition \li{c}, it creates two subgoals:\ one in
which \li{c} appears as a hypothesis and one where \li{¬ c} appears.

In the next example, we show how to exploit injectivity of constructors. The
\li{cases} tactic can be used to apply injectivity on equations whose both
sides have the same constructor applied. In the proof below, the equation on
which injectivity is applied is \li{x :: xs = y :: ys}. 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:

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

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}

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

Lists are not the only interesting data type. 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. Here, it indicates that the type \li{α} should be
implicitly derived from the context surrounding occurrences of \li{empty}.)

By default, the constructor names are prefixed by the name of the type---i.e.,
\li{tree.empty} and \li{tree.node}. To lighten notations, we can enter the
following command, which exports \li{empty} and \li{node} from the \li{tree}
namespace, allowing us to write \li{empty} and \li{node} with no
qualification:

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

A peculiarity of binary trees is that structural induction has two induction
hypotheses:\ one for the left subtree of an inner node and one for the right
subtree. To prove a goal \li{p t} about a tree \li{t} by structural induction on
\li{t}, we must prove (1)~\li{p empty} and (2)~\li{p (node a l r)} assuming
\li{p l} and \li{p r}.

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 the example below demonstrates:

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

\section{Example: Colors}
\label{sec:example-colors}

Lean provides a convenient syntax for defining records, or \emph{structures}.
These are essentially nonrecursive, single-constructor inductive types, but
with some syntactic sugar. The definition below introduces an \li{rgb}
structure 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}

We can define a new structure as the extension of an existing structure. The
definition below introduces a fourth component, called \li{alpha}, to \li{rgb}
and calls the result \li{rgba}:

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

Values can be specified in a variety of syntaxes:

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

The definition of \li{semitransparent_red} copies all the values from \li{red}
(indicated by the \li{..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 uses the automatically generated projection functions
\li{rgb.red}, \li{rgb.green}, and \li{rgb.blue}. Instead of \li{rgb.red c}, Lean
lets us simply write \li{c.red}, and similarly for the other fields.

Applying \li{shuffle} three times in a row is the same as not applying it at
all:

\betweenlistings
\lstinputlisting[linerange=shuffle_shuffle_shuffle-q]{../lean/love04_functional_programming_demo_master.lean}
%
The proof teaches us a new trick. The \li{cases} tactic is a relative of
\li{induction}. It performs a case distinction on its arguments, but it does
not generate inductive hypotheses.

\section{Overlapping Patterns}

It is possible to write equations with overlapping patterns. For example:

\begin{lstlisting}
def f {α : Type} : list α → ⋯
| [] := …
| xs := … xs …
\end{lstlisting}
%
The first matching equation is taken. Internally, this is the same as

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

\section{New Tactics}
\label{sec:new-tactics-functional-programming}

\subsection{by\_cases}

\begin{quote}
\li{by_cases} \,\texttt{\itshape proposition}
\end{quote}
%
The \li{by_cases} tactic performs a case analysis on a proposition. It is useful
to reason about the condition in an \li{if} condition.

\subsection{cases}

\begin{quote}
\li{cases} \,\texttt{\itshape variable} $\bigl[$\li{with}
  \texttt{\itshape name}$_\texttt{1}$ $\ldots$
  \texttt{\itshape name}$_\texttt{\itshape n}\bigr]$
\end{quote}
%
The \li{cases} tactic performs a case distinction on the specified variable.
This gives rise to as many subgoals as there are constructors in the
definition of the variable's type. Its behavior is similar to \li{induction}'s
except that it does not produce induction hypotheses.

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

\section{Summary of New Syntax}

\small

\subsection{Declaration}

\noindent
\begin{tabularx}{\textwidth}{@{}p{9em}X@{}}
\li{structure} & introduces a record type and its projection functions \\
\end{tabularx}

\subsection{Command}

\noindent
\begin{tabularx}{\textwidth}{@{}p{9em}X@{}}
\li{export} & makes names available outside their namespaces \\
\end{tabularx}

\subsection{Term Language}

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

\subsection{Tactics}

\noindent
\begin{tabularx}{\textwidth}{@{}p{9em}X@{}}
\li|by_cases| & performs a case analysis on an \li{if} condition \\
\li|cases| & performs a case analysis on a variable of an inductive type \\
\end{tabularx}
