\chapter{Structured Proofs and Proof Terms}
\label{chap:structured-proofs-and-proof-terms}

Tactics are a \emph{backward} (or \emph{bottom-up}) proof mechanism. They start
from the goal and break it down. Often it makes sense to work \emph{forward}:\
to start with what we already know and proceed step by step towards our goal.
\emph{Structured proofs} are a style that supports this reasoning. They can be
combined with the tactical style. Backward proofs tend to be easier to write
but harder to read. It is, after all, easier to destruct things than to
construct them.

Structured proofs are syntactic sugar sprinkled over Lean's \emph{proof
terms}. All proofs, whether tactical or structured, are reduced internally to
proof terms. As the name suggests, these proofs are represented as terms. We
have seen some proof terms already, in Chapter~\ref{chap:tactical-proofs}: If
we have \li{hab : a → b} and \li{ha : a}, then \li{hab ha} is a proof term
for~\li{b}, and we write \li{hab ha : b}.

The concepts covered here are described in more detail in Chapters 2~to~4 of
\emph{Theorem Proving in Lean} \cite{theorem-proving-in-lean}. Nederpelt and
Geuvers's textbook \cite{nederpelt-geuvers-2014} and Van Raamdonk's lecture
notes \cite{van-raamsdonk-2011} are other useful references.

\section{Structured Proofs}
\label{sec:structured-proofs}

Structured proofs are built using a number of constructs. We review the main
ones below.

\subsection{Lemma Name}

The simplest kind of structured proof is the name of a lemma. If we have
%
\begin{lstlisting}
lemma some_name :
  some_proposition :=
…
\end{lstlisting}
%
then \li{some_name} can be used as a proof of \li{some_proposition}
later---for example:
%
\begin{lstlisting}
lemma some_other_name :
  some_proposition :=
some_name
\end{lstlisting}
%
We can do the same with local hypotheses, and we can pass arguments to lemmas or
hypotheses to instantiate \li{∀} quantifiers and discharge assumptions of a
lemma.

As an more realistic example, suppose we have a lemma
\li{add_comm (m n : ℕ)} \li{:} \li{add m n = add n m}, and suppose we want to
prove its instance \li{add 0 n = add n 0}. This can be achieved neatly using
the name of the lemma and two arguments:

\lstinputlisting[linerange=add_comm_zero_left-q]{../lean/love03_structured_proofs_and_proof_terms_demo_master.lean}
%
This has the same effect as the tactical proof \li{by exact add_comm 0 n},
but is more concise.

\subsection{assume}

\begin{quote}
\li{assume} \,\texttt{\itshape name}$_\texttt{1}$ $\ldots$ \texttt{\itshape name}$_\texttt{\itshape n}$\li{,}
\end{quote}
%
The \li{assume} command moves variables or assumptions from the goal into the
local context, as local constants or hypotheses. It can be seen as a structured
version of the \li{intros} tactic. At the proof term level, it amounts to
\texttt{\itshape n} \li{λ}~binders.

\subsection{have}

\begin{quote}
\li{have} \,\texttt{\itshape name} \li{:} \texttt{\itshape proposition} \li{:=} \texttt{\itshape proof}\li{,}
\end{quote}
%
The \li{have} command lets us state and prove an intermediate lemma statement,
which can refer to the local context. Often we put a \li{_} placeholder for
\texttt{\itshape proposition} if it can be inferred from the proof.

\subsection{let}

\begin{quote}
\li{let} \,\texttt{\itshape name} $\bigl[$\li{:} \texttt{\itshape type}$\bigr]$ \li{:=} \texttt{\itshape term} \,\li{in}
\end{quote}
%
The \li{let} command introduces a new local definition. It can be used to name a complex
object that occurs several times in the proof afterwards. It is similar to \li{have} but for
computable data, not a proof. Often we omit the type if it can be inferred from the term.
Folding or unfolding a \li{let} corresponds to \li{ζ}-conversion
(Section~\ref{sec:basic-tactics}).

\subsection{show}

\begin{quote}
\li{show} \,\texttt{\itshape proposition}\li{,} \,\li{from} \,\texttt{\itshape structured-proof} \\
\li{show} \,\texttt{\itshape proposition}\li{,} \,\li{begin} \texttt{\itshape tactics} \li{end} \\
\li{show} \,\texttt{\itshape proposition}\li{,} \,\li{by} \texttt{\itshape tactic}
\end{quote}
%
The \li{show} command lets us repeat the goal to prove, which can be useful as
documentation. It also allows us to rephrase the goal in an equal form up
to computation. Instead of the syntax \li{show} \texttt{\itshape proposition}\li{,}
\li{from} \texttt{\itshape structured-proof}, we can simply write
\texttt{\itshape structured-proof} if we do not need to rephrase the goal.

The second and third syntaxes listed above remind us that it is possible to mix
proof styles. Similarly, the \texttt{\itshape proof} part of a \li{have}
command can be either a structured proof or a tactical proof introduced by
\li{begin} or \li{by}. Generally, we tend to use structured proofs to sketch the
main argument and resort to tactical proofs for proving subgoals or
straightforward lemmas.

Another kind of mixture arises when we pass arguments to lemma names. For
example, given, \li{hab : a → b} and \li{ha : a}, the tactic invocation
\li{exact hab ha} will prove the goal~\li{b}: \li{hab ha} is a (admittedly
small) proof term nested in a tactic. Yet another kind of mixture arises when
we open a \li{begin} $\ldots$ \li{end} block after invoking some structured
proof commands such as \li{assume} and \li{have}, as in the following example:

\lstinputlisting[linerange=and_swap₂-q]{../lean/love03_structured_proofs_and_proof_terms_demo_master.lean}
%
Here is a purer proof:

\lstinputlisting[linerange=and_swap-q]{../lean/love03_structured_proofs_and_proof_terms_demo_master.lean}

\subsection{Forward Tactics}

Two of the proof commands presented above---\li{have} and \li{let}---are also
available as tactics. Many users, especially beginners, prefer the tactical
mode. Even with tactics, it can be useful to reason in a forward fashion.
Observe that the syntax for the tactic \li{let} is slightly different than for
the structured proof command of the same name, with a comma (\li{,}) instead of
the keyword \li{in}.

\begin{quote}
\li{have} \,$\bigl[\bigl[$\texttt{\itshape name} \li{:}$\bigr]$ \texttt{\itshape proposition}$\bigr]$ \li{:=} \texttt{\itshape proof}\li{,}
\\[2\jot]
\li{let} \,\texttt{\itshape name} $\bigl[$\li{:} \texttt{\itshape type}$\bigr]$ \li{:=} \texttt{\itshape term}\li{,}
\end{quote}

\section{Calculational Proofs}
\label{sec:calculational-proofs}

In informal mathematics, we often express proofs as transitive chains of
equalities, inequalities, or equivalences (e.g., \li{a = b = c}, \li{a ≥ b ≥ c},
or \li{a ↔ b ↔ c}). In Lean, such \emph{calculational proofs} are supported by
the \li{calc} command. It provides a lightweight syntax and takes care of
applying transitivity lemmas for preregistered relations (including equality
and the arithmetic comparison operators).

The general syntax is as follows:
%
\begin{quote}
\noindent\rlap{\li{calc}}\phantom{\li{...} \texttt{\itshape op}$_\texttt{2}$ }\texttt{\itshape expr}$_\texttt{0}$ \\
\phantom{\li{...} }\texttt{\itshape op}$_\texttt{1}$ \texttt{\itshape expr}$_\texttt{1}$ \li{:} \\
\noindent\hbox{}\quad \texttt{\itshape proof}$_\texttt{1}$ \\
\li{...} \texttt{\itshape op}$_\texttt{2}$ \texttt{\itshape expr}$_\texttt{2}$ \li{:} \\
\noindent\hbox{}\quad \texttt{\itshape proof}$_\texttt{2}$ \\
\noindent\phantom{\li{...} \texttt{\itshape op}$_\texttt{2}$ \texttt{\itshape ex}}$\vdots$ \\
\li{...} \texttt{\itshape op}$_\texttt{\itshape n}$ \texttt{\itshape expr}$_\texttt{\itshape n}$ \li{:} \\
\noindent\hbox{}\quad \texttt{\itshape proof}$_\texttt{\itshape n}$
\end{quote}
%
The horizontal dots (\li{...}) are part of the syntax. Each
\texttt{\itshape proof}$_\texttt{\itshape i}$
establishes the statement
\texttt{\itshape expr}$_\texttt{{\itshape i}-1}$ \texttt{\itshape op}$_\texttt{\itshape i}$ \texttt{\itshape expr}$_\texttt{\itshape i}$.
The operators \texttt{\itshape op}$_\texttt{\itshape i}$ need not be identical,
but they need to be compatible. For example, $=$, $<$, and $\le$ are compatible
with each other, whereas $>$ and $<$ are not.

A simple example follows:

\lstinputlisting[linerange=two_mul_example-q]{../lean/love03_structured_proofs_and_proof_terms_demo_master.lean}
%
The horizontal dots stand for the term \li{(m + m) + n}, which we would have had
to repeat had we performed the proof with two \li{have}s:

\lstinputlisting[linerange=two_mul_example₂-q]{../lean/love03_structured_proofs_and_proof_terms_demo_master.lean}
%
Notice that with \li{have}s, we also need to explicitly invoke \li{eq.trans}
and to give names to the two intermediate steps.

\section{Induction by Pattern Matching}
\label{sec:induction-by-pattern-matching}

In Section~\ref{sec:induction-tactic}, we saw how to use the \li{induction}
tactic to carry out proofs by induction. An alternative, more structured style
relies on pattern matching, as in the example below:

\lstinputlisting[linerange=add_zero-q]{../lean/love03_structured_proofs_and_proof_terms_demo_master.lean}
%
The patterns on the left, \li{0} and \li{(nat.succ m)}, correspond to the two
constructors of the type of the \li{∀}-quantified variable \li{n : ℕ}. On the
right-hand side of each \li{:=} symbol is a proof for the corresponding case:\
the base case or the induction step.

Inside the induction step's proof, the induction hypothesis is available under
the same name as the lemma we are proving. We explicitly pass \li{m} as
argument to the hypothesis: This is useful as documentation, and it also
prevents Lean from accidentally invoking the induction hypothesis in a
circular or otherwise ill-founded fashion---for example, on \li{nat.succ m}.
Lean's termination checker would detect this and raise an error.

Simultaneous pattern matching is also possible, as in the examples below:

\lstinputlisting[linerange=add_succ_etc-q]{../lean/love03_structured_proofs_and_proof_terms_demo_master.lean}
%
Notice the structured proof command \li{have} in the proof of \li{add_comm₂}.

The general format of lemmas with pattern matching is as follows:
%
\begin{quote}
\li{lemma} \,\texttt{\itshape name} \,\texttt{(\itshape vars}$_\texttt{1}$ : \texttt{\itshape type}$_\texttt{1}$\texttt{)} $\ldots$ \texttt{(\itshape vars}$_\texttt{\itshape m}$ : \texttt{{\itshape type}$_\texttt{\itshape m}$)}
  \,\li{:}\, \texttt{\itshape statement} \\
\li{|}\, \texttt{\itshape patterns}$_\texttt{1}$ \,\li{:=}\, \texttt{\itshape proof}$_\texttt{1}$ \\
\noindent\hbox{}\phantom{\li{|}\, \texttt{\itshape pa}}$\vdots$ \\
\li{|}\, \texttt{\itshape patterns}$_\texttt{\itshape n}$ \,\li{:=}\, \texttt{\itshape proof}$_\texttt{\itshape n}$
\end{quote}

A few hints on how to carry out proofs by induction follow:

\begin{itemize}
\item It is usually beneficial to perform induction following the structure of
  the definition of one of the functions appearing in the goal.

\item If the base case of an induction is difficult, this is often a sign that
  the wrong variable was chosen or that some lemmas are missing.
\end{itemize}

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

Dependent types are the defining feature of the \emph{dependent type theory}
family of logics. Consider a function \li{pick} that takes a natural number
\li{x} (a value from \li|ℕ = {0, 1, 2, …}|) and that returns a natural number
between \li{0} and \li{x}. Conceptually, \li{pick} has a dependent type, namely,
\li{(x : ℕ) →} \verb|{|\li{y : ℕ // y ≤ x}\verb|}|. Informally, we read
\verb|{|\li{y : ℕ // y ≤ x}\verb|}| as ``the type consisting of all \li{y} from
\li{ℕ} such that \li{y ≤ x}.'' We can think of this type as a \li{ℕ}-indexed
family, where each member's type may depend on the index:
\li|pick x : {y : ℕ // y ≤ x}|. The name \li{x} is immaterial; we~could have
used any other name except \li{y}.

Unless otherwise specified, a \emph{dependent type} means a type depending on
a term, as in the above example, with \li{x : ℕ} as the term and
\verb|{|\li{y : ℕ // y ≤ x}\verb|}| as the type that depends on it. This is
what we mean when we claim that simple type theory does not support dependent
types. But a type may also depend on another type---for example, the type
constructor \li{list}, its \li{η}-expanded variant \li{λα} \li{:}
\li{Type, list α}, or the polymorphic type \li{λα : Type, α → α} of functions
with the same domain and codomain. A term may depend on a type---for example,
the polymorphic identity function \li{λα : Type, λx : α, x}. And of course, a
term may also depend on a term---for example, \li{λx : ℕ, x}.

In summary, there are four cases for \li{λx, t} in dependent type theory:

\begin{center}
\begin{tabular}{@{}l@{\quad}l@{\quad}l@{\kern1.5em}l@{}}
\toprule
Body (\verb|t|)\kern-5em & & Argument (\verb|x|) & Description \\
\midrule
A term & \relax{depending on} & a term & Simply typed $\lambda$-abstraction \\
A type & \relax{depending on} & a term & Dependent type (stricto senso) \\
A term & \relax{depending on} & a type & Polymorphic term \\
A type & \relax{depending on} & a type & Type constructor \\
\bottomrule
\end{tabular}
\end{center}

The last three rows correspond to the three axes of Henk Barendregt's
$\lambda$-cube.%
\footnote{\url{https://en.wikipedia.org/wiki/Lambda_cube}}

The \textsc{App} and \textsc{Lam} rules presented in
Section~\ref{sec:types-and-terms} must be generalized to work with
dependent types:
%
\begin{gather*}
\prftree[r]{\textsc{App}$'$}
  {\strut\Gamma~\vdash~\text{\li{t : (x : σ) → τ[x]}}}
  {\strut\Gamma~\vdash~\text{\li{u : σ}}}
  {\strut\Gamma~\vdash~\text{\li{t u : τ[u]}}}
\\[2\jot]
\prftree[r]{\textsc{Lam}$'$}
  {\strut\Gamma\text{\li{, x : σ}}~\vdash~\text{\li{t : τ[x]}}}
  {\strut\Gamma~\vdash~\text{\li{(λx : σ, t) : (x : σ) → τ[x]}}}
\end{gather*}
%
The simply typed case arises when \li{x} does not occur in \li{τ[x]}.
Then, we can simply write \li{σ →} and not \li{(x : σ) →}.
The notation \li{σ → τ} is equivalent to \li{(_ : σ)} \li{→ τ}.
It is easy to see that \textsc{App}$'$ and \textsc{Lam}$'$ are identical to
\textsc{App} and \textsc{Lam} when \li{x} does not occur in \li{τ[x]}.

The example below demonstrates \textsc{App}$'$:
%
\[\prftree[r]{\textsc{App}$'$}
  {\strut\vdash~\text{\li{pick : (x : ℕ) →}
   \texttt{\char`\{}\li{y : ℕ // y ≤ x}\texttt{\char`\}}}}
  {\strut\vdash~\text{\li{5 : ℕ}}}
  {\strut\vdash~\text{\li{pick 5 :}
   \texttt{\char`\{}\li{y : ℕ // y ≤ 5}\texttt{\char`\}}}}\]

The next example demonstrates \textsc{Lam}$'$:
%
\[\prftree[r]{\textsc{Lam}$'$}
  {
    \prftree[r]{\textsc{Lam} or \textsc{Lam}$'$}
      {\strut\hbox{\texttt{$\alpha$~:~Type,~x~:~$\alpha~{\vdash}$~x~:~$\alpha$}}}
      {\strut\hbox{\texttt{$\alpha$~:~Type~${\vdash}$~($\lambda$x~:~$\alpha$,~x)~:~$\alpha \to \alpha$}}}
  }
  {\strut\hbox{${\vdash}$~\texttt{($\lambda\alpha$~:~Type,~$\lambda$x~:~$\alpha$,~x)~:~($\alpha$~:~Type)${}
    \to \alpha \to \alpha$}}}\]

We conclude with an important remark on notations. Regrettably, the intuitive
syntax \li{(x : σ) → τ} is not available in Lean. Instead, we must write
\li{Πx : σ, τ} to specify a dependent type. The arrow notation \li{σ → τ}
(without the \li{x}) is syntactic sugar for \li{Π_ : σ, τ}. The \li{Π} binder
emphasizes that \li{x} is a bound variable within \li{Π}'s scope.

As an alias for \li{Π}, we can also write \li{∀}. The two symbols are fully
interchangeable.

In Section~\ref{sec:type-definitions}, we saw the commands

\lstinputlisting[linerange=check_list-q]{../lean/love01_definitions_and_lemma_statements_demo_master.lean}
%
and their output
%
\begin{lstlisting}
list.nil : Π(α : Type), list α
list.cons : ?M_1 → list ?M_1 → list ?M_1
\end{lstlisting}
%
We can now make sense of the $\Pi$-type. Namely, \li{list.nil} is a function
that takes a type \li{α} as argument and that returns a value of type
\li{list α}.

\section{The Curry--Howard Correspondence}
\label{sec:the-curry-howard-correspondence}

You likely have noticed that we use the same symbol \li{→} both as the
implication symbol and as the type constructor of functions. Similarly, \li{∀}
is used both as a quantifier and to specify dependent types. When we see
\li{a → b}, without further context, we cannot tell whether we have the type of a
function with domain \li{a} and codomain \li{b} or the proposition ``\li{a}
implies \li{b}.'' Similarly, \li{∀x, t[x]} can denote a proposition or a
dependent type.

It turns out that not only the two pairs of concepts look the same, they
\emph{are} the same. This is called the \emph{Curry--Howard correspondence}.
It is also called the \emph{PAT principle}, where PAT is a double mnemonic:
%
\begin{align*}
   \hbox{PAT \,\li{=}\, propositions as types}
&& \hbox{PAT \,\li{=}\, proofs as terms}
\end{align*}

Nicolaas Govert de Bruijn, Haskell Curry, William Alvin Howard, and possibly
others independently noticed that for some logics, propositions are isomorphic
to types, and proofs are isomorphic to terms. Hence, in dependent type theory,
we \emph{identify} proofs with terms as well as propositions with types,
a considerable economy of concepts.

Let us go through the dramatis personae one by one:\ types, propositions,
terms, and proofs. We use the metavariables \li{σ}, \li{τ} for types;
\li{φ}, \li{ψ} for propositions; \li{t}, \li{u}, \li{x} for terms; and \li{h}
for proofs.

For types, we have the following:
%
\begin{itemize}
\item \li{σ → τ} is the type of (total) functions from \li{σ} to \li{τ}.
\item \li{Πx : σ, τ[x]} is the dependent type from \li{x : σ} to \li{τ[x]}.
\end{itemize}

For propositions, we have the following:
%
\begin{itemize}
\item \li{φ → ψ} can be read as ``\li{φ} implies \li{ψ}'', or as the type of
  functions mapping proofs of \li{φ} to proofs of \li{ψ}.
\item \li{∀x : σ, ψ[x]} can be read as ``for all x, \li{ψ[x]}'', or as the type
  of function mapping values \li{x} of type \li{σ} to proofs of
  \li{ψ[x]}.
\item \li{∀h : φ, ψ[h]} is the type of function mapping proofs \li{h} of
  \li{φ} to proofs of \li{ψ[h]}.
\end{itemize}

Notice the similarities between types and propositions. And recall that \li{∀}
is an alias for \li{Π}.

For terms, we have the following:
%
\begin{itemize}
\item Declared constants are terms.
\item \li{t u} is the application of function \li{t} to value \li{u}.
\item \li{λx, t[x]} is a function mapping \li{x} to \li{t[x]}.
\end{itemize}

For proofs (i.e., proof terms), we have the following:
%
\begin{itemize}
\item A lemma name is a proof.
\item \li{l} \li{a}, which instantiates the leading parameter or quantifier of
  lemma~\li{l} with value~\li{a}, is a proof.
\item \li{l} \li{l'}, which discharges the leading assumption of \li{l} with
  lemma~\li{l'}, is a proof. This operation is called \emph{modus ponens}.
\item Given \li{h[n] : φ[n]}, we have that \li{λn : σ, h[n]} is a proof of
  \li{∀n : σ, φ[n]}.
\item Given \li{h[h'] : φ[h']}, we have that \li{λh' : ψ, h[h']} is a proof of
  \li{∀h' : ψ, φ[h']}.
\end{itemize}
%
For the last two cases, in a structured proof we would write \li{assume}, and
in a tactical proof we would invoke \li{intros}.

By the Curry--Howard correspondence, a proof by \emph{induction} is the same as
a \emph{recursively} specified proof term. When we invoke the induction
hypothesis, we are really just calling a recursive function (the lemma)
recursively. This explains why, in a proof by pattern matching
(Section~\ref{sec:induction-by-pattern-matching}), the induction hypothesis has
the same name as the lemma we prove.

In the same way, \emph{well-founded induction} (also called ``complete
induction'', ``course-of-values induction'', or ``strong induction'') is the
same as well-founded recursion. \emph{Structural induction} corresponds to
\emph{structural recursion}. Lean's termination checker is used to prove
well-foundedness of the proof by induction.

Finally, you may have noticed that the commands \li{def} and \li{lemma} have
almost the same syntax. They are, in fact, almost the same, with the exception
that \li{lemma} considers the proof term (or whatever defined term) opaque,
whereas \li{def} keeps it transparent. Since proofs are irrelevant to Lean's
logic, there is no need to store them or unfold them later. A similar
difference is visible between \li{let} and \li{have}.

\section{Summary of New Syntax}

\small

\subsection{Proof Commands}

\noindent
\begin{tabularx}{\textwidth}{@{}p{9em}X@{}}
\li|assume| & states variables or assumptions \\
\li|calc| & combines proofs by transitivity \\
\li|have| & states an intermediate lemma \\
\li|let| $\dots$ \li{in} & introduces a local definition \\
\li|show| & states the goal's conclusion \\
\end{tabularx}

\subsection{Tactics}

\noindent
\begin{tabularx}{\textwidth}{@{}p{9em}X@{}}
\li|have| & states an intermediate lemma \\
\li|let| & introduces a local definition \\
\end{tabularx}
