\chapter{Forward Proofs}
\label{chap:forward-proofs}

Tactics are a backward proof mechanism. They start from the goal and break it
down. Often it makes sense to work in a forward fashion:\ to start with what we
already know and proceed step by step towards our goal. \emph{Structured
proofs} are a style that supports this kind of reasoning. It can be combined
with the tactical style. Tactical proofs tend to be easier to write but harder
to read; it is, after all, easier to destruct things than to construct them.
Most users combine the two styles, using whichever seems the most appropriate
for the situation. The higher readability of structured proofs make them
popular with some users, especially in mathematical circles.

Structured proofs are syntactic sugar sprinkled over Lean's \emph{proof terms}.
They are built using keywords such as \li{assume}, \hbox{\li{have},}
\hbox{\li{let},} and \li{show} that mimic pen-and-paper proofs. All Lean proofs,
whether tactical or structured, are reduced internally to proof terms. We have
seen some specimens already, in Chapter~\ref{chap:backward-proofs}: Given
hypotheses \li{ha : a} and \li{hab : a → b}, the term \li{hab ha} is a proof
term for the proposition \li{b}, and we write \li{hab ha : b}. The names of
lemmas and hypotheses, such as \li{ha} and \li{hab}, are also proof terms.
Pushing this idea further, given \li{hbc : b →} \li{c}, we can build the proof
term \li{hbc (hab ha)} for the proposition \li{c}. We can think of \li{hab} as a
function that converts a proof of \li{a} to a proof of \li{b}, and similarly for
\li{hbc}.

Structured proofs are the default in Lean. They can be used outside tactic
mode. To enter tactic mode, we need to use a \li{begin … end} block or a
\li{by} line.

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 Raamsdonk's lecture
notes \cite{van-raamsdonk-2011} are other useful references.

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

As a first example, consider the following structured proof:

\lstinputlisting[linerange=fst_of_two_props-q]{../lean/love03_forward_proofs_demo_master.lean}
%
Each variable bound by a \li{∀}-quantifier and each assumption of an
implication is introduced explicitly in the proof using the \li{fix} and
\li{assume} commands. Several variables or hypotheses can be introduced
simultaneously. We will \hbox{often} omit the types of variables, especially
when they can be guessed from their names; however, we will usually spell out
the propositions and put them one per line, to increase readability---which is,
after all, one of the main potential advantages of the structured style. The
\li{show …,} \hbox{\li{from}} command at the end repeats the proposition to
prove, for the sake of readability, and gives the proof after the keyword
\li{from}. The goal at this point is \li{a b : Prop, ha : a, hb : b ⊢ a}.

Informally, we could write the proof as follows:

\begin{quote}
Fix some propositions \li{a} and \li{b}.
\\[\jot]
Assume (\li{ha}) \li{a} and (\li{hb}) \li{b} are true.
\\[\jot]
We must show \li{a}. This follows trivially from \li{ha}. \qed
\end{quote}
%
Some authors would insert some qualifiers such as ``arbitrary but fixed'' in
front of ``propositions,'' especially in textbooks for first-year bachelor
students, or they would write ``Let \li{a} and \li{b} be some propositions.''
All these variants are equivalent. And instead of ``$\squareforqed$,'' some
authors would write ``QED'' to conclude the proof.

The Lean proof above is atypical in that the goal's target appears among the
hypotheses. Usually, we must perform some intermediate reasoning steps,
essentially of the form ``from such-and-such, we have so-and-so.'' In Lean,
each intermediate step takes the form of a \li{have} command, as in the
following example:

\lstinputlisting[linerange=prop_comp-q]{../lean/love03_forward_proofs_demo_master.lean}
%
Informally:

\begin{quote}
Assume (\li{ha}) \li{a} is true.
\\[\jot]
From \li{ha} and \li{hab}, we have (\li{hb}) \li{b}.
\\[\jot]
From \li{hb} and \li{hbc}, we have (\li{hc}) \li{c}.
\\[\jot]
We must show \li{c}. This follows trivially from \li{hc}. \qed
\end{quote}
%
Notice that this is a forward proof: It progresses one theorem at a time from
the hypothesis \li{a} to the desired theorem \li{c}.

In general, the \li{fix}--\li{assume}--\li{show} skeleton simply repeats the
lemma's statement. We often name the fixed variables after the bound variables
from the goal, as we did here, but this is not mandatory. Moreover, it is good
practice to avoid shadowing existing variables. Between the last \li{fix} or
\li{assume} and the \li{show}, we may have as many \li{have} commands as we
want, depending on how detailed we want the argument to be. Details can increase
readability, but providing too many details can overwhelm even the most
persistent reader.

The \li{have} command has a similar syntax to \li{lemma} but appears inside a
structured proof. We can think of a \li{have} as a definition. In
\li{have hb : b := hab ha}, the right-hand side \li{hab ha} is a proof term for
\li{b}, and the left-hand side \li{hb} is defined as a synonym for that proof
term. From then on, \li{hb} and \li{hab ha} can be used interchangeably.
Since \li{hb} and \li{hc} are used only once and their proofs are very short,
experts would tend to inline them, replacing \li{hc} by \li{hbc hb}
and \li{hb} by \li{hab ha}, yielding

\lstinputlisting[linerange=prop_comp₂-q]{../lean/love03_forward_proofs_demo_master.lean}

A typical structured proof has the following
\li{fix}--\li{assume}--\li{have}--\li{show} format:

\begin{lstlisting}
lemma l :
  ∀(c₁ : σ₁) … (cₗ : σₗ), P₁ → ⋯ → Pₘ → R :=
fix (c₁ : σ₁) … (cₗ : σₗ),
assume h₁ : P₁,
 ⋮
assume hₘ : Pₘ,
have k₁ : Q₁ :=
  …,
 ⋮
have kₙ : Qₙ :=
  …,
show R, from
  …
\end{lstlisting}

\section{Structured Constructs}
\label{sec:structured-constructs}

The previous section presented the main commands for writing structured proofs:\
\li{fix}, \li{assume}, \li{have}, and \li{show}. We now review the components
of structured proofs more systematically.

\subsection*{Lemma or Hypothesis}

The simplest structured proof, apart from \li{sorry}, is the name of a lemma or
hypothesis. If we have
%
\begin{lstlisting}
lemma two_add_two_eq_four :
  2 + 2 = 4 :=
begin
  …
end
\end{lstlisting}
%
then the lemma name \li{two_add_two_eq_four} can be used as a proof of
\li{2 + 2 = 4} later. For example:
%
\begin{lstlisting}
lemma this_time_with_feelings :
  2 + 2 = 4 :=
two_add_two_eq_four
\end{lstlisting}

We can pass arguments to lemmas to instantiate \li{∀}-quantifiers and discharge
assumptions. Suppose the lemma \li{add_comm (m n : ℕ) : add m n = add n m} is
available, 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_forward_proofs_demo_master.lean}
%
This has the same effect as the tactical proof \li{by exact add_comm 0 n}, but
is more concise. The \li{exact} tactic can be seen as the inverse of \li{by}.
Why enter tactic mode if only to leave it immediately?

Like with \li{exact} and \li{apply}, the lemma or hypothesis's statement is
matched with the current goal up to computation. This gives some flexibility.

\subsection*{fix}

\smallskip

\begin{quote}
\lic{fix} \,\ttvar{names} $\bigl[$\lic{:} \ttvar{type}$\bigr]$\lic{,} \\[\jot]
\lic{fix} \,\lic{(}\ttvar{names}$_\texttt{1}$ $\bigl[$\lic{:} \ttvar{type}$_\texttt{1}\bigr]$\lic{)} $\ldots$
  \lic{(}\ttvar{names}$_\ttvar{n}$ $\bigl[$\lic{:} \ttvar{type}$_\ttvar{n}\bigr]$\lic{),}
\end{quote}
%
The \li{fix} command moves \li{∀}-quantified variables from the goal's
target to the local context. It can be seen as a structured version of the
\li{intros} tactic.

Note that the standard Lean tactic for fixing variables is \hbox{\li{assume},} which
also works in this case. We prefer to use \li{fix}, which is provided by
\li{LoVelib}, as a more readable alternative and reserve \li{assume} for
assumptions.

\subsection*{assume}

\smallskip

\begin{quotecode}
\lic{assume} \,\ttvar{names} $\bigl[$\lic{:} \ttvar{proposition}$\bigr]$\lic{,} \\[\jot]
\lic{assume} \,\lic{(}\ttvar{names}$_\texttt{1}$ $\bigl[$\lic{:} \ttvar{proposition}$_\texttt{1}\bigr]$\lic{)} $\ldots$
  \lic{(}\ttvar{names}$_\ttvar{n}$ $\bigl[$\lic{:} \ttvar{proposition}$_\ttvar{n}\bigr]$\hbox{\lic{),}}
\end{quotecode}
%
The \li{assume} command moves the leading assumptions from goal's target to
the local context. It can be seen as a structured version of the \li{intros}
tactic.

\subsection*{have}

\smallskip

\begin{quote}
\lic{have} \,\ttvar{name} \lic{:} \ttvar{proposition} \lic{:=} \\
\noindent\hbox{}\quad \ttvar{proof}\lic{,}
\end{quote}
%
The \li{have} command lets us state and prove an intermediate lemma,
which may refer to names introduced by previous \li{fix}es, \li{assume}s, and
\li{have}s. The proof can be tactical or structured. Generally, we tend to use
structured proofs to sketch the main argument and resort to tactical proofs for
proving subgoals or uninteresting intermediate steps.
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 \li{exact hab ha}
will prove the goal~\li{⊢ b}. Here, \li{hab ha} is a proof
term nested inside a tactic.

\subsection*{let}

\smallskip

\begin{quote}
\lic{let} \,\ttvar{name} $\bigl[$\lic{:} \ttvar{type}$\bigr]$ \lic{:=}
\ttvar{term}\, \lic{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
is designed for computable data, not proofs. Expanding or introducing a \li{let}
corresponds to \li{ζ}-conversion (Section~\ref{sec:basic-tactics}).

\subsection*{show}

\smallskip

\begin{quote}
\lic{show} \,\ttvar{proposition}\lic{,} \,\lic{from}\, \\
\noindent\hbox{}\quad \ttvar{proof}
\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 a syntactically equal
form up to computation. Instead of the syntax \li{show}
\ttvar{proposition}\li{,} \li{from} \ttvar{proof}, we can simply write
\ttvar{proof} if we do not want to repeat the goal and do not need to rephrase
it. The proof can be tactical or structured.

\section{Forward Reasoning about Connectives and Quantifiers}
\label{sec:forward-reasoning-about-connectives-and-quantifiers}

Reasoning about the logical connectives and quantifiers in a forward fashion
uses the same introduction and elimination rules as in tactic mode
(Section~\ref{sec:reasoning-about-connectives-and-quantifiers}). A few examples
will show the flavor. Let us start with conjunction:

\lstinputlisting[linerange=and_swap-q]{../lean/love03_forward_proofs_demo_master.lean}
%
Even readers who do not know what \li{and.elim_left} etc.\ means can understand
that we extract \li{a} and \li{b} from \li{a ∧ b} and put them back together as
\li{b ∧ a}. Mathematicians would probably have an easier time making sense of
this proof than of its tactical counterpart:

\lstinputlisting[linerange=and_swap-q]{../lean/love02_backward_proofs_demo_master.lean}
%
On the other hand, the tactical proof is easier to derive mindlessly.

In general, backward proofs are easier to find, and most of the automation
provided by proof assistants works backwards. The reason is simple: Pretend
that you are Miss Marple or Hercule Poirot on a murder investigation. A
backward investigation would start from the crime scene and try to extract
clues that potentially connect a handful of suspects to the crime. In contrast,
a forward investigation might start by questioning as many as seven billion
people to determine whether they have an alibi. Which approach is more likely
to succeed?

Our next examples concern \emph{one-point rules}. These are lemmas that can be
used to eliminate a quantifier when the bound variable can effectively take
only one value. For example, the proposition \li{∀n, n = 666 → beast ≥ n} can
be simplified to \li{beast ≥ 666}. The following lemma justifies this
simplification:

\lstinputlisting[linerange=forall.one_point-q]{../lean/love03_forward_proofs_demo_master.lean}
%
The proof may look intimidating, but it was not hard to develop. The key was to
proceed one step at a time. At first, we observed that the goal is an
implication, so we wrote
%
\begin{lstlisting}
iff.intro (_) (_)
\end{lstlisting}
%
The two placeholders are important to make this proof well formed. We already
put parentheses because we strongly suspect that these will be nontrivial
proofs. Because proofs are basically terms, which are basically programs, the
advice we gave in Section~\ref{ssec:type-inhabitation} applies here as well:
%
\begin{quote}
%\thekeyidea{\soutthick{\,program\,} proof}
\thekeyidea{[proof]}
\end{quote}
%
Hovering over the first placeholder makes the corresponding subgoal appear. We
can see that Lean expects a proof of \hbox{\li{⊢ (∀x,}}
\hbox{\li{x = t → p x) → p t},} so we provide a suitable skeleton. A structured
proof of an implication consists of an \li{assume} followed by a
\li{show}:
%
\begin{lstlisting}
iff.intro
  (assume hall : ∀x, x = t → p x,
   show p t, from
     _)
  (_)
\end{lstlisting}
%
Each of the remaining placeholder can be replaced by a structured proof or by a
tactical proof. To fill these placeholders, we can use essentially the same
procedure as for exhibiting an inhabitant of a type
(Section~\ref{ssec:type-inhabitation}), interpreting implication as the function
arrow and writing \li{assume}--\li{show} instead of \li{λ}.

Let us check that the rule actually works on our motivating example:
%
\lstinputlisting[linerange=beast_666-q]{../lean/love03_forward_proofs_demo_master.lean}
%
It works. Matching \li{forall.one_point t p} against the statement of
\li{beast_666} yields the instantiation \li{t := 666} and
\li{p := (λm, beast ≥ m)}.

Finally, the one-point rule for \li{∃} demonstrates how to use the introduction
and elimination rules for \li{∃} in a structured proof:

\lstinputlisting[linerange=exists.one_point-q]{../lean/love03_forward_proofs_demo_master.lean}
%
Notice how we use \li{exists.elim hex} to obtain an \li{x} such that
\li{x = t ∧ p x}. This admittedly is a bit cumbersome.

\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, such as equality and
the arithmetic comparison operators.

\newcommand\calcsyntax[1]{%
\begin{quote}
\noindent\hbox{}\rlap{#1}\phantom{\lic{...} \ttvar{op}$_\texttt{2}$ }\,\ttvar{term}$_\texttt{0}$ \\
\noindent\hbox{}\phantom{\lic{...} }\ttvar{op}$_\texttt{1}$ \,\ttvar{term}$_\texttt{1}$ \lic{:} \\
\noindent\hbox{}\quad \ttvar{proof}$_\texttt{1}$ \\
\lic{...} \ttvar{op}$_\texttt{2}$ \,\ttvar{term}$_\texttt{2}$ \lic{:} \\
\noindent\hbox{}\quad \ttvar{proof}$_\texttt{2}$ \\
\noindent\phantom{\lic{...} \ttvar{o}}$\vdots$ \\
\lic{...} \ttvar{op}$_\ttvar{n}$ \,\ttvar{term}$_\ttvar{n}$ \lic{:} \\
\noindent\hbox{}\quad \ttvar{proof}$_\ttvar{n}$
\end{quote}%
}

The general syntax is as follows:
%
\calcsyntax{\lic{calc}}
%
The horizontal dots (\li{...}) are part of the syntax. Each
\ttvar{proof}$_\ttvar{i}$
justifies the statement
\ttvar{term}$_{\ttvar{i}\texttt{-1}}$ \ttvar{op}$_\ttvar{i}$ \ttvar{term}$_\ttvar{i}$.
The operators \ttvar{op}$_\ttvar{i}$ need not be identical,
but they must be compatible. For example, $=$, $<$, and $\le$ are compatible,
whereas $>$ and $<$ are incompatible.

A simple example follows:

\lstinputlisting[linerange=two_mul_example-q]{../lean/love03_forward_proofs_demo_master.lean}
%
Mathematicians (assuming they would condescend to offer a justification for such
a trivial result) could have written the above proof roughly as follows:
%
\begin{quote}
\noindent\hbox{}\phantom{\li{=}}\, \li{2 * m + n} \\
\li{=}\, \li{(m + m) + n}
  \hfill(since \li{2 * m = m + m}) \\
\li{=}\, \li{m + n + m}
  \hfill(by associativity and commutativity of \li{+}) \\
{\color{white}x} \qed
\end{quote}
%
In the Lean proof, the horizontal dots stand for the term \li{(m + m) + n},
which we would have had to repeat had we written the proof without \li{calc}:

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

\section{Forward Reasoning with Tactics}
\label{sec:forward-reasoning-with-tactics}

Most users prefer the tactic mode. But even in tactic mode, it can be useful to
reason in a forward fashion, mixing forward and backward reasoning steps. The
structured proof commands \li{have}, \li{let}, and \li{calc} are also available
as tactics, making this possible.

The following example demonstrates the \li{have} and \li{let} tactics on a lemma
we have seen several times already:

\lstinputlisting[linerange=prop_comp₃-q,keywords={lemma,begin,end}]{../lean/love03_forward_proofs_demo_master.lean}

\subsection*{have}

\smallskip

\begin{quote}
\li{have} \,$\bigl[\bigl[$\ttvar{name} \li{:}$\bigr]$ \ttvar{proposition}$\bigr]$ \li{:=} \\
\noindent\hbox{}\quad \ttvar{proof}
\end{quote}
%
The \li{have} tactic lets us state and prove an intermediate lemma in tactic
mode. Afterwards, the lemma is available as a hypothesis in the goal state.

\subsection*{let}

\smallskip

\begin{quote}
\li{let} \,\ttvar{name} $\bigl[$\li{:} \ttvar{type}$\bigr]$ \li{:=}
\ttvar{term}
\end{quote}
%
The \li{let} tactic lets us introduce a local definition in tactic mode.
Afterwards, the defined symbol and its definition are available
in the goal state.

Observe that the syntax for the \li{let} tactic is slightly different than for
the \li{let} structured proof command, with no \li{in} keyword (but a comma
instead if the tactic is followed by another tactic).

\subsection*{calc}

\smallskip

\calcsyntax{\li{calc}}
%
The \li{calc} tactic lets us enter a calculational proof
(Section~\ref{sec:calculational-proofs}) in tactic mode. The tactic has the same
syntax as the structured proof command of the same name. We can regard
\hbox{\li{apply} \li{calc …}\,,} where \li{calc} is a tactic, as an alias for
\li{apply} \hbox{\li{(exact}} \li{calc} \hbox{\li{…)},} where \li{calc} is the
structured proof command described above.

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

Dependent types are the defining feature of the \emph{dependent type theory}
family of logics. Although you may not be familiar with the terminology, you
are likely to be familiar with the concept in some form or other.

Consider a function \li{pick} that takes a natural number \li{n} (i.e., a value
from \li|ℕ| \li|=| \li|{0, 1, 2, …}|) and that returns a natural number between
\li{0} and \li{n}. Intuitively, \li{pick n} should have the type
\li|{0,| \hbox{\li|1, …, n}|} (i.e., the type consisting of all natural numbers
\li{i ≤ n}). In Lean, this is written \verb|{|\li{i : ℕ // i ≤ n}\verb|}|.
This would be the type of \li{pick n}. Mathematically inclined readers might want
to think of \li{pick} as an \li{ℕ}-indexed family of terms
\[\hbox{{\large\texttt{(}}\lic|pick n : {i : ℕ // i ≤ n}|{\large\texttt{)}}$_\texttt{n{:}ℕ}$}\]
in which the type of each term depends on the index---e.g.,
\li|pick 5 :| \li|{i : ℕ //| \hbox{\li|i ≤ 5}|.}
But what would be the type of \li{pick} itself? We would like to express that
\li{pick} is a function that takes an argument \li{n : ℕ} and that returns a
value of type \li|{i : ℕ // i ≤ n}|. To capture this, we will write
\[\hbox{\lic|pick : (n : ℕ) → {i : ℕ // i ≤ n}|}\]
This is a dependent type: The type of the result depends on the value of the
argument \li{n}. The variable name \li{n} is immaterial.

Unless otherwise specified, a \emph{dependent type} means a type depending on
a (non-type) term, as above, with \li{n : ℕ} as the term and
\verb|{|\li{i : ℕ // i ≤ n}\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{λn : ℕ, n + 2}. In summary,
there are four cases for \li{λx, t}:

\vskip4\smallskipamount

\centerline{\tabletfootnotesize\begin{tabular}{@{}l@{\quad}l@{\quad}l@{\kern1.5em}l@{}}
\toprule
Body (\li|t|)\kern-5em & & Argument (\li|x|) & Description \\
\midrule
A term & \relax{depending on} & a term & Simply typed $\lambda$-expression \\
A type & \relax{depending on} & a term & Dependent type (in the narrow sense) \\
A term & \relax{depending on} & a type & Polymorphic term \\
A type & \relax{depending on} & a type & Type constructor \\
\bottomrule
\end{tabular}}

\vskip4\smallskipamount

\noindent
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{ssec:type-checking-and-type-inference} must be generalized to work
with dependent types:
%
\begin{gather*}
\prftree[r]{\textsc{App}$'$}
  {\strut\text{\lic{C ⊢ t : (x : σ) → τ[x]}}}
  {\strut\text{\lic{C ⊢ u : σ}}}
  {\strut\text{\lic{C ⊢ t u : τ[u]}}}
\\[2\jot]
\prftree[r]{\textsc{Lam}$'$}
  {\strut\text{\lic{C, x : σ ⊢ t : τ[x]}}}
  {\strut\text{\lic{C ⊢ (λx : σ, t) : (x : σ) → τ[x]}}}
\end{gather*}
%
The notation \li{τ[x]} stands for a type that may contain \li{x}, and
\li{τ[u]} stands for the same type where all occurrences of \li{x} have been
replaced by \li{u}.

The simply typed case arises when \li{x} does not occur in \li{τ[x]}. Then, we
can simply write \li{σ →} instead of \li{(x : σ) →}. The familiar notation
\li{σ → τ} is equivalent to \li{(_ : σ)} \li{→ τ}. It is easy to check that
\textsc{App}$'$ and \textsc{Lam}$'$ coincide with \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\text{\lic|\⊢ pick : (n : ℕ) → {i : ℕ // i ≤ n}|}}
  {\strut\text{\lic|5 : ℕ|}}
  {\strut\text{\lic|\⊢ pick 5 : {i : ℕ // i ≤ 5}|}}\]
%
The next example demonstrates \textsc{Lam}$'$:
%
\[\prftree[r]{\textsc{Lam}$'$}
  {
    \prftree[r]{\textsc{Lam} or \textsc{Lam}$'$}
      {\strut\text{\lic|\α : Type, x : α ⊢ x : α|}}
      {\strut\text{\lic|\α : Type ⊢ (λx : α, x) : α → α|}}
  }
  {\strut\text{\lic|\⊢ (λα : Type, λx : α, x) : (α : Type) → α → α|}}\]

The picture is incomplete because we only check that the terms---the entities
on the left-hand side of a colon (\li{:})---are well typed. The types---the
entities on the right-hand side of a colon---must also be checked, using the
same type system, but this time as terms. For example, the type of
\li{nat.succ} is \li{ℕ → ℕ}, whose type is \li{Type}. Types of types, such as
\li{Type} and \li{Prop}, are called universes. We will study them more
closely in Chapter~\ref{chap:logical-foundations-of-mathematics}.

Regrettably, the intuitive syntax \li{(x : σ) → τ} used above
is not available in Lean. Instead, we must write \li{∀x : σ, τ}.
The familiar notation \li{σ → τ} is supported as syntactic
sugar for \li{∀_ : σ, τ}. The \li{∀} syntax emphasizes that \li{x} is a bound
variable. As an alias for \li{∀}, we can also write \li{Π}. The two symbols are
interchangeable.

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

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

\section{The PAT Principle}
\label{sec:the-pat-principle}

You will likely have noticed that the same symbol \li{→} is used both for implication
(e.g., \hbox{\li{false → true}}) and as the type constructor of functions (e.g.,
\li{ℤ → ℕ}). Similarly, \li{∀} is used both as a quantifier and to specify
dependent types. Without context, we cannot tell whether \hbox{\li{a → b}}
refers to the type of a function with domain \li{a} and codomain \li{b} or to
the proposition ``\li{a} implies \li{b},'' and similarly, \hbox{\li{∀x : a, b[x]}} can
denote a proposition or a dependent type.

It turns out that not only the two pairs of concepts \emph{look} the same, they
\emph{are} the same. This is 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*}
%
Furthermore, because types are also terms, we also have that propositions are
terms. However, PAT is not a quadruple mnemonic
({\soutthick{\,PAT \,\li{=}\, proofs as types\,}}). Also note that not all types
are propositions, and not all terms are proofs.

By using terms and types to represent proofs and propositions, dependent type
theory achieves a considerable economy of concepts. The question ``Is \li{H} a
proof of \li{P}?''\ becomes equivalent to ``Does the term \li{H} have type
\li{P}?'' As a result, inside of Lean, there is no proof checker, only a type
checker.

Let us review the dramatis personae one by one. We use the metavariables
\li{σ}, \li{τ} for types; \li{P}, \li{Q} for propositions; \li{t}, \li{u},
\li{x} for terms; and \li{h}, \li{G}, \li{H}, for proofs.

Starting with ``propositions as types,'' 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 function type from \li{x : σ} to
  \hbox{\li{τ[x]}.}
\end{itemize}
%
In contrast, for propositions, we have the following:
%
\begin{itemize}
\item \li{P → Q} can be read as ``\li{P} implies \li{Q},'' or as the type of
  functions mapping proofs of \li{P} to proofs of \li{Q}.
\item \li{∀x : σ, Q[x]} can be read as ``for all x, \li{Q[x]},'' or as the type
  of functions mapping values \li{x} of type \li{σ} to proofs of
  \li{Q[x]}.
\end{itemize}
%
Continuing with ``proofs as terms,'' for terms, we have the following:
%
\begin{itemize}
\item A constant is a term.
\item A variable is a term.
\item \li{t u} is the application of function \li{t} to argument \li{u}.
\item \li{λx, t[x]} is a function mapping \li{x} to \li{t[x]}.
\end{itemize}
%
In contrast, for proofs (i.e., proof terms), we have the following:
%
\begin{itemize}
\item The name of a lemma or hypothesis is a proof.
\item \li{H t}, which instantiates the leading parameter or quantifier of
  proof \li{H}'s statement with term~\li{t}, is a proof.
\item \li{H G}, which discharges the leading assumption of \li{H}'s
  statement with proof~\li{G}, is a proof. This operation is called \emph{modus
  ponens}.
\item \li{λh : P, H[h]} is a proof of \li{P → Q},
  assuming \li{H[h]} is a proof of \li{Q} for \li{h : P}.
\item \li{λx : σ, H[x]} is a proof of \li{∀x : σ, Q[x]},
  assuming \li{H[x]} is a proof of \li{Q[x]} for \li{x : σ}.
\end{itemize}
%
The last two cases are justified by the \li{Lam}$'$ rule. In a structured
proof, as opposed to a raw proof term, we would write \li{assume} or \li{fix}
instead of \li{λ}, and we would probably want to repeat the conclusion using
\li{show} for readability, as follows:
%
\begin{lstlisting}[multicols=2]
lemma case_4 :
  P → Q :=
assume h : P,
show Q, from
  H[h]
lemma case_5 :
  ∀x : σ, Q[x] :=
fix x,
show Q[x], from
  H[x]
\end{lstlisting}

Some commands are provided in Lean under two different names but are really the
same by the PAT principle. This is the case for
\li{constant} and \li{axiom} as well as for \li{fix} and \li{assume};
indeed, \li{fix} is defined by \li{LoVelib} as an alias for \li{assume}.

There are also pairs with slightly different behavior, such as \li{def} and
\li{lemma} or \li{let} and \li{have}. The fundamental difference is this: When
we define some function or data, we care not only about the type but also about
the body---the behavior. On the other hand, once we have proved a lemma, the
proof becomes \emph{irrelevant}. All that matters is that there \emph{is} a
proof. We will return to the topic of proof irrelevance in
Chapter~\ref{chap:logical-foundations-of-mathematics}.

The following correspondence table summarizes the differences between tactical
proofs, structured proofs, and raw proof terms:

\vskip4\smallskipamount

\centerline{\tabletsmall\begin{tabular}{@{}p{11em}@{\enskip}p{11em}@{\enskip}p{11em}@{}}
\toprule
Tactical proof & Structured proof & Raw proof term \\
\midrule
\li|intro x,|       & \lic|fix x,|          & \lic|\λx,| \\
\li|intro h,|       & \lic|assume h,|       & \lic|\λh,| \\
\li|have k := H,|   & \lic|have k := H,|    & \lic|(\λk, …) H| \\
\li|let x := t,|    & \lic|let x := t in|   & \lic|(\λx, …) t| \\
\li|exact (H : P)|  & \lic|show P, from H|  & \lic|H : P| \\
\li|calc …|         & \lic|calc …|          & \lic|calc …| \\
\bottomrule
\end{tabular}}

\vskip4\smallskipamount

\noindent
Notice that \li{let x := a in t} is essentially a sophisticated way to write
\li{(λx, t) a}. Its main benefit, aside from readability, is that it is not
subject to $\beta$-reduction.

The terminology of dependent type theory can be quite confusing, because some
words have a narrow and a broad sense. The following diagram captures the
various meanings of important words:\strut
%
\begin{center}
\Large
\begin{tabular}{@{}c@{\enskip}c@{\enskip}c@{\enskip}c@{\enskip}c@{\enskip}c@{\enskip}l@{}}
$\overbrace{\strut\text{\lic|2 + 2|}}^{\vphantom{Pq}\text{term}}$
  & \lic|:| & $\overbrace{\strut\text{\lic|\ℕ|}}^{\vphantom{Pq}\text{type}}$
  & \lic|:| & \lic|Type|
  & \lic|:| & \enskip$\cdots$ \\[1\jot]
$\underbrace{\strut\text{\lic|true.intro|}}_{\vphantom{Pq}\text{proof}}$
  & \lic|:| & $\underbrace{\strut\text{\lic|true|}}_{\vphantom{Pq}\text{proposition}}$
  & \lic|:| & \lic|Prop|
  & \lic|:| & \enskip$\cdots$ \\[-3ex]
&&&& \multicolumn{3}{@{}l@{}}{\rlap{$\underbracket{\kern5.5em}_{\vphantom{(q}\text{universes}}$}} \\[-1.5ex]
&& \multicolumn{5}{@{}l@{}}{\rlap{$\underbracket{\kern10.75em}_{\vphantom{(q}\text{types}}$}} \\[-1.5ex]
\multicolumn{7}{@{}l@{}}{\rlap{$\underbracket{\kern17.65em}_{\vphantom{(q}\text{terms}}$}} \\
\end{tabular}
\end{center}
%
According to the broad senses, any expression is a term, any expression that
may occur on the right-hand side of a typing judgment is a type, and any
expression that may occur on the right-hand side of a typing judgment with a
type on its left-hand side is a universe. This is consistent with the
reading of \li{t : u} as ``\li{t}~has type~\li{u}'' and the notion that
universes are types of types.

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

In Section~\ref{sec:proofs-by-mathematical-induction}, we reviewed the use of
the \li{induction'} tactic to perform proofs by induction. An alternative, more
flexible style relies on pattern matching and the PAT principle.

Recall the definition of the reverse of a list from Section~\ref{sec:function-definitions}:

\lstinputlisting[linerange=reverse_def-q]{../lean/love01_definitions_and_statements_demo_master.lean}
%
In fact, \li{reverse} exists as \li{list.reverse} in Lean's standard library,
but our definition is optimized for reasoning.
A useful 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. The induction step is
%
\[\hbox{\tabletfootnotesize\ctxt{ih}~\lic{: ∀xs, reverse (reverse xs) = xs ⊢ reverse (reverse xs ++ [x]) = x :: xs}}\]
%
What is unpleasant about this subgoal is the presence of \,\hbox{\li{++ [x]}} inside the
double \li{reverse} sandwich. We need a way to ``distribute'' the outer
\li{reverse} over \li{++} to 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/love03_forward_proofs_demo_master.lean}
%
The lemma's proof uses a more flexible style than usual. Arguably, it looks more
like a recursive function definition than a proof. The patterns on the left,
\li{[]} and \li{x} \li{::} \hbox{\li{xs},} correspond to the two constructors of
the \li{∀}-quantified variable \li{xs}. On the right-hand side of each \li{:=}
symbol is a proof for the corresponding case. The variables on which we can
pattern-match are those that appear in the \li{∀} quantifiers, in order of
occurrence (here, \li{xs} and \li{ys}).

Inside the induction step's proof, the induction hypothesis is available under
the same name as the lemma we are proving (\li{reverse_append}). We explicitly
pass \li{xs} as argument to the induction hypothesis. This restricts the
hypothesis so that it only applies to \li{xs} but not to other lists. In
particular, this ensures that the lemma will not be applied to \li{x :: xs},
which could lead to a circular argument: ``To prove \li{reverse_append}
\li{(x :: xs)}, use \li{reverse_append} \li{(x :: xs)}.'' Lean's termination
checker would notice that the argument is ill-founded and raise an error, but we
want to avoid that. In addition, the explicit argument \li{xs} is useful as
documentation, effectively saying, ``The only recursive instance of the lemma we
need is the one on \li{xs}.''

For reference, the corresponding tactical proof is as follows:
%
\lstinputlisting[linerange=reverse_append₂-q]{../lean/love03_forward_proofs_demo_master.lean}

The lemma would also be provable, and useful, if we put \li{[y]} instead of
\hbox{\li{ys}.} But it is a good habit to state lemmas as generally as possible. This
results in more reusable libraries. Moreover, this is often necessary to obtain
a strong enough induction hypothesis in a proof by induction. In general,
finding the right inductions and lemmas can require thought and creativity.

Simultaneous pattern matching on multiple variables is supported (e.g., \li{xs}
and \li{ys} above). The patterns are then separated by spaces. This explains
why Lean requires us to put parentheses around complex patterns, even when we
match on a single variable. The general format is
%
\begin{quote}
\begin{tabular}{@{}l@{}}
\lic|lemma| \,{\color{procnamecolor}\ttvar{name}}
  \,\lic|(|\ttvar{params}$_\texttt{1}$ \lic|:| \ttvar{type}$_\texttt{1}$\lic|)| $\ldots$
  \lic|(|\ttvar{params}$_\ttvar{m}$ \lic|:| \ttvar{type}$_\ttvar{m}$\lic|) :| \\
\noindent\hbox{}\quad \ttvar{statement} \\
\lic$|$\, \ttvar{patterns}$_\texttt{1}$ \,\lic$:=$\, \ttvar{proof}$_\texttt{1}$ \\
\noindent\hbox{}\phantom{\lic$|$\, \ttvar{pa}}$\vdots$ \\
\lic$|$\, \ttvar{patterns}$_\ttvar{n}$ \,\lic|:=|\, \ttvar{proof}$_\ttvar{n}$
\end{tabular}
\end{quote}
%
Notice the strong similarity with the syntax of \li{def}
(Section~\ref{sec:function-definitions}). The two commands are, in fact, almost
the same, the main exception being that \li{lemma} considers the defined term or
the proof opaque, whereas \li{def} keeps it transparent. Since the actual
proofs are irrelevant once a lemma is proved
(Section~\ref{chap:logical-foundations-of-mathematics}), there is no need to
expand them later. A similar distinction exists between \li{let} and \li{have}.

By the PAT principle, a proof by induction by pattern matching is the same as a
recursive proof term. When we invoke the induction hypothesis, we are really
just invoking a recursive function recursively. This explains why the induction
hypothesis has the same name as the lemma we prove. Lean's termination checker
is used to establish well-foundedness of the proof by induction.

With the \li{reverse_append} lemma in place, we can return to our initial goal:
%
\lstinputlisting[linerange=reverse_reverse-q]{../lean/love03_forward_proofs_demo_master.lean}

Induction by pattern matching is highly popular among Lean users. Its main
advantages are its convenient syntax and its support for well-founded
induction, which is more powerful than structural induction as provided by the
\li{induction'} tactic (Section~\ref{sec:induction-tactic}). However, in this
guide, we will not need the full power of well-founded induction. Furthermore,
for subtle logical reasons, induction by pattern matching is not available for
inductive predicates, which are the topic of
Chapter~\ref{chap:inductive-predicates}. For these reasons, we will generally
prefer \li{induction'}.

\section{Summary of New Lean Constructs}

\begingroup
\summarysize

\subsection*{Proof Commands}

\noindent
\begin{xltabular}{\textwidth}{@{}p{9em}X@{}}
\lic|assume| & states assumptions \\
\lic|calc| & combines proofs by transitivity \\
\lic|fix| & fixes variables \\
\lic|have| & states an intermediate lemma \\
\lic|let … in| & introduces a local definition \\
\lic|show …, from| & states the target \\
\end{xltabular}

\subsection*{Tactics}

\noindent
\begin{xltabular}{\textwidth}{@{}p{9em}X@{}}
\lic|calc| & combines proofs by transitivity \\
\lic|have| & states an intermediate lemma \\
\lic|let| & introduces a local definition \\
\end{xltabular}

\endgroup
