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

Tactical proofs work backwards. They start from the goal and reduce it to
existing theorems and hypotheses. Often it makes sense to work in a forward
fashion:\ to start with existing theorems and hypotheses and proceed step by
step towards our goal.
%
\emph{Structured proofs} are a style that supports this kind of reasoning.
Tactical proofs tend to be easier to write but harder to read. 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.

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
theorems 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 must use the \li{by} command.

The concepts covered here are described in more detail in Chapters 2~to~4
of \emph{Theorem Proving in Lean 4} \cite{theorem-proving-in-lean}. Nederpelt
and Geuvers's textbook \cite{nederpelt-geuvers-2014} is another useful reference.

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

As a first example, consider the following structured proof:

\lstinputlisting[linerange=fst_of_two_props-q]{../lean/LoVe/LoVe04_ForwardProofs_DemoMaster.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 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 always 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 … 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 qualifiers such as ``arbitrary but fixed'' in front of
``propositions,'' or they would write ``Let \li{a} and \li{b} be some
propositions.'' All these variants are equivalent. And instead of
``$\squareforqed$,'' we could 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 so-and-so, we have such-and-such.'' In Lean,
each intermediate step takes the form of a \li{have} command, as in the
following example:

\lstinputlisting[linerange=prop_comp-q]{../lean/LoVe/LoVe04_ForwardProofs_DemoMaster.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}. Modus ponens
(``from \li{a} and \li{a → b}, derive \li{b}'') is expressed by simple
juxtaposition (e.g., \li{hab ha}).

In general, the \li{fix}--\li{assume}--\li{show} skeleton repeats the
theorem'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 can 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 can overwhelm the reader.

The \li{have} command has a similar syntax to \li{theorem} but appears inside a
structured proof. We can also 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 then \li{hb} by \li{hab ha}, yielding

\lstinputlisting[linerange=prop_comp_inline-q]{../lean/LoVe/LoVe04_ForwardProofs_DemoMaster.lean}

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

\begin{lstlisting}
theorem hr :
  ∀(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*{Theorem or Hypothesis}

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

We can pass arguments to theorems to instantiate \li{∀}~quantifiers and to discharge
assumptions. Suppose the theorem \hbox{\li{add_comm}} \li{(m n : ℕ) : add m n = add} \li{n} \li{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 theorem and two arguments:

\lstinputlisting[linerange=add_comm_zero_left-q]{../lean/LoVe/LoVe04_ForwardProofs_DemoMaster.lean}
%
This is equivalent to 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 only to leave it immediately?

As with \li{exact} and \li{apply}, the theorem 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} \lic{:} \ttvar{type}
\end{quote}
%
The \li{fix} command moves \li{∀}-quantified variables from the goal's
target to the local context. It is a structured version of the \li{intro}
tactic.

Note that the standard Lean tactic for fixing variables is \hbox{\li{fun}.} We
prefer to use \li{fix}, which is provided by \li{LoVelib}, as a more readable
alternative. We will keep \li{fun} for specifying anonymous functions.

\subsection*{assume}

\smallskip

\begin{quote}
\lic{assume} \,\ttvar{name} \lic{:} \ttvar{proposition}
\end{quote}
%
The \li{assume} command moves the leading assumption from goal's target to
the local context. It can be seen as a structured version of the \li{intro}
tactic.

Note that the standard Lean tactic for stating assumptions is \hbox{\li{fun}.}
We prefer to use \li{assume}, which is provided by \li{LoVelib}, as a more
readable alternative. We will keep \li{fun} for specifying anonymous functions.

\subsection*{have}

\smallskip

\begin{quote}
\lic{have} \,\ttvar{name} \lic{:} \ttvar{proposition} \lic{:=} \\
\noindent\hbox{}\phantom{\li{xx}}\ttvar{proof}
\end{quote}
%
The \li{have} command lets us state and prove an intermediate theorem,
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 theorem 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}
\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}).

The construct \li{let} \,\ttvar{name} $\bigl[$\li{:} \ttvar{type}$\bigr]$
\li{:=} \ttvar{term} must be followed by a line break or a semicolon (\li{;}).

\subsection*{show}

\smallskip

\begin{quote}
\lic{show} \,\ttvar{proposition} \,\lic{from}\, \\
\noindent\hbox{}\phantom{\li{xx}}\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{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 give the flavor. Let us start with conjunction:

\lstinputlisting[linerange=and_swap-q]{../lean/LoVe/LoVe04_ForwardProofs_DemoMaster.lean}
%
Even readers who do not know what \li{And.left} etc.\ mean 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_tactical-q]{../lean/LoVe/LoVe04_ForwardProofs_DemoMaster.lean}

In general, backward proofs are easier to derive ``mindlessly,'' and most of the
automation provided by proof assistants works backwards. This makes sense:
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 eight 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 theorems 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 \hbox{\li{beast}} \hbox{\li{≥ 666}.} The following theorem
justifies this simplification:

\lstinputlisting[linerange=Forall.one_point-q]{../lean/LoVe/LoVe04_ForwardProofs_DemoMaster.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
equivalence, so we wrote
%
\begin{lstlisting}
  Iff.intro (_) (_)
\end{lstlisting}
where \li{Iff.intro} is the introduction rule for \li{↔}
(Section~\ref{sec:reasoning-about-connectives-and-quantifiers}).
%
The two placeholders are important to make this proof well formed. We use
parentheses because we strongly suspect that the subproofs will be nontrivial.
Because proofs are basically terms, which are basically programs, the
advice we gave in Section~\ref{sec:type-inhabitation} applies here as well,
mutatis mutandis:
%
\begin{quote}
\thekeyidea{proof}{proof}{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 placeholders can be replaced by a structured proof or a
tactical proof. To eliminate the first placeholder, we enter tactic mode and
apply the instance \li{t = t → P t} of the assumption \li{∀x, x = t → P x} to
the goal \li{⊢ P t}. This leaves the proof obligation \li{t = t}, which we
dischage using the \li{rfl} tactic:
%
\begin{lstlisting}
  Iff.intro
    (assume hall : ∀x, x = t → P x
     show P t from
       by
         apply hall t
         rfl))
    (_)
\end{lstlisting}

The second placeholder stands for \li{⊢ P t → ∀x, x = t → P x}.
To eliminate it, we write \li{assume} corresponding to the first implication's
assumption, \li{fix} for \li{∀}, \li{assume} for the second implication's
assumption, and \li{show} for the conclusion:
%
\begin{lstlisting}
    (assume hp : P t
     fix x : α
     assume heq : x = t
     show P x from
       _)
\end{lstlisting}
%
The \li{show}'s proof is tactical: We rewrite \li{x} to \li{t} in \li{⊢ P x},
obtaining \li{⊢ P t}, which matches the assumption \li{hp}:
%
\begin{lstlisting}
    (assume hp : P t
     fix x : α
     assume heq : x = t
     show P x from
       by
         rw [heq]
         exact hp)
\end{lstlisting}

Let us check that the one-point rule actually works on our motivating example:
%
\lstinputlisting[linerange=beast_666-q]{../lean/LoVe/LoVe04_ForwardProofs_DemoMaster.lean}
%
It works. Instead of \li{Forall.one_point _ _}, we could also have written
\li{Forall.}\allowbreak\li{one_point} \li{666} \li{(fun m} \li{↦ 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/LoVe/LoVe04_ForwardProofs_DemoMaster.lean}
%
Although the proof might look overwhelming, it was developed mostly without
thinking using the same procedure as for the proof of the one-point rule for
\li{∀}.

First, we use the introduction rule for \li{↔}:
%
\begin{lstlisting}
  Iff.intro (_) (_)
\end{lstlisting}
%
For the first placeholder, we must provide a proof of
\li{P t} under the assumption \li{∃x : α, x = t ∧ P x}. Thus, we expand the
proof skeleton to
%
\begin{lstlisting}
  Iff.intro
    (assume hex : ∃x : α, x = t ∧ P x
     show P t from
       _)
    (_)
\end{lstlisting}
%
At this point, we want to extract the witness for \li{x} in the assumption
\li{hex}. To achieve this, we use the elimination rule for \li{∃}:
%
\begin{lstlisting}
  Iff.intro
    (assume hex : ∃x : α, x = t ∧ P x
     show P t from
       Exists.elim hex (_))
    (_)
\end{lstlisting}
%
The first placeholder asks for a proof of the subgoal \li{⊢ ∀x, x = t ∧ P x → P t}.
We sketch one:
%
\begin{lstlisting}
  Iff.intro
    (assume hex : ∃x : α, x = t ∧ P x
     show P t from
       Exists.elim hex
         (fix x : α
          assume hand : x = t ∧ P x
          show P t from
            _))
    (_)
\end{lstlisting}
%
Notice how the subproof mirrors the subgoal, with \li{fix} corresponding to
\li{∀}, \hbox{\li{assume}} corresponding to \li{→}'s assumption, and \li{show}
corresponding to \li{→}'s conclusion.
We can now access the witness \li{x} and its characteristic property
\li{x = t ∧ P x}.

Next, we extract the two conjuncts of \li{x = t ∧ P x}, using the \li{have}
command and the elimination rules for \li{∧} (\li{And.left} and \li{And.right}):
%
\begin{lstlisting}
  Iff.intro
    (assume hex : ∃x : α, x = t ∧ P x
     show P t from
       Exists.elim hex
         (fix x : α
          assume hand : x = t ∧ P x
          have hxt : x = t :=
            And.left hand
          have hpx : P x :=
            And.right hand
          show P t from
            _))
    (_)
\end{lstlisting}
%
Now we can attempt a proof of \li{P t}. We rewrite \li{t} into \li{x} and apply
the hypothesis \li{P x}:
%
\begin{lstlisting}
  Iff.intro
    (assume hex : ∃x : α, x = t ∧ P x
     show P t from
       Exists.elim hex
         (fix x : α
          assume hand : x = t ∧ P x
          have hxt : x = t :=
            And.left hand
          have hpx : P x :=
            And.right hand
          show P t from
            by
              rw [←hxt]
              exact hpx))
    (_)
\end{lstlisting}

For the remaining placeholder, we first provide a proof skeleton based on the
subgoal \li{⊢ P t → ∃x : α, x = t ∧ P x}:
%
\begin{lstlisting}
    (assume hp : P t
     show ∃x : α, x = t ∧ P x from
       _)
\end{lstlisting}
%
Then we use the introduction rule for \li{∃} to provide the witness \li{t}:
%
\begin{lstlisting}
    (assume hp : P t
     show ∃x : α, x = t ∧ P x from
       Exists.intro t (_))
\end{lstlisting}
%
Then comes more boilerplate:
%
\begin{lstlisting}
    (assume hp : P t
     show ∃x : α, x = t ∧ P x from
       Exists.intro t
         (show t = t ∧ P t from
            _))
\end{lstlisting}
%
The last conjunction, \li{t = t ∧ P t}, is easy to prove: Its left-hand side
follows by reflexivity, and its right-hand side is simply the assumption
\li{hp}. Finally, we get
%
\begin{lstlisting}
    (assume hp : P t
     show ∃x : α, x = t ∧ P x from
       Exists.intro t
         (have tt : t = t :=
            by rfl
          show t = t ∧ P t from
            And.intro tt hp))
\end{lstlisting}

To develop the above structured proofs, we used largely the same procedure as
for exhibiting an inhabitant of a type (Section~\ref{sec:type-inhabitation}),
understanding the function arrow as implication. The similarity between the two
procedures is no coincidence, as we will see in
Section~\ref{sec:the-pat-principle}.

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

In informal mathematics, we often express proofs as transitive chains of
equalities, inequalities, or equivalences (e.g., \hbox{\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, which provides a lightweight syntax and takes care of
applying transitivity theorems for preregistered relations, such as equality and
the arithmetic comparison operators.

\newcommand\calcsyntax{%
\begin{quote}
\noindent\hbox{}\lic{calc} \\
\noindent\hbox{}\phantom{\li{xx}}\ttvar{term}$_\texttt{0}$ \,\ttvar{op}$_\texttt{1}$ \,\ttvar{term}$_\texttt{1}$ \lic{:=} \\
\noindent\hbox{}\phantom{\li{xxxx}}\ttvar{proof}$_\texttt{1}$ \\
\noindent\hbox{}\phantom{\li{xx}}\_ \,\ttvar{op}$_\texttt{2}$ \,\ttvar{term}$_\texttt{2}$ \lic{:=} \\
\noindent\hbox{}\phantom{\li{xxxx}}\ttvar{proof}$_\texttt{2}$ \\
\noindent\hbox{}\phantom{\li{xxxxxx}}$\vdots$ \\
\noindent\hbox{}\phantom{\li{xx}}\_ \,\ttvar{op}$_\ttvar{n}$ \,\ttvar{term}$_\ttvar{n}$ \lic{:=} \\
\noindent\hbox{}\phantom{\li{xxxx}}\ttvar{proof}$_\ttvar{n}$
\end{quote}%
}

The general syntax is as follows:
%
\calcsyntax
%
The underscores (\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 with each other. For example, $=$, $<$, and $\le$
are compatible, whereas $>$ and $<$ are not.

A simple example follows:

\lstinputlisting[linerange=two_mul_example-q]{../lean/LoVe/LoVe04_ForwardProofs_DemoMaster.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{}\li{2 * m + n} \,\li{=}\, \li{(m + m) + n}
  \hfill(since \li{2 * m = m + m}) \\
\noindent\hbox{}\phantom{\li{2 * m + n}} \,\li{=}\, \li{m + n + m}
  \hfill(by associativity and commutativity of \li{+}) \\
{\color{white}x} \qed
\end{quote}
%
In the Lean proof, the underscore stands 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_have-q]{../lean/LoVe/LoVe04_ForwardProofs_DemoMaster.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}

Many users prefer the tactic mode to structured proofs. 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
theorem we have seen several times already:

\lstinputlisting[linerange=prop_comp_tactical-q]{../lean/LoVe/LoVe04_ForwardProofs_DemoMaster.lean}

\subsection*{have}

\smallskip

\begin{quote}
\lic{have} \,\ttvar{name} \li{:} \ttvar{proposition} \li{:=} \\
\noindent\hbox{}\phantom{\li{xx}}\ttvar{proof}
\end{quote}
%
The \li{have} tactic lets us state and prove an intermediate theorem in tactic
mode. Afterwards, the theorem is available as a hypothesis in the goal state.

\subsection*{let}

\smallskip

\begin{quote}
\lic{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.

\subsection*{calc}

\smallskip

\calcsyntax
%
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{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 type 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.,
\hbox{\li|pick|} \li|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} itself is immaterial; we could also
write \li{m} or \li{x}.)

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. But:
%
\begin{itemize}
\item A type may also depend on another type---for example, the type
  constructor \li{List}, its \li{η}-expanded variant \li{fun α} \li{:}
  \li{Type ↦ List α}, or the polymorphic type \li{fun α : Type ↦ α → α} of functions
  with the same domain and codomain.

\item A term may depend on a type---for example,
  the polymorphic identity function \li{fun α : Type ↦ fun x : α ↦ x}.

\item And of course, a term may also depend on a term---for example,
  \li{fun n : ℕ} \li{↦ n + 2}.
\end{itemize}
%
In summary, there are four cases for \li{fun 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 & Polymorphic 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{Fun} rules presented in
Section~\ref{sec: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{Fun}$'$}
  {\strut\text{\lic{C, x : σ ⊢ t : τ[x]}}}
  {\strut\text{\lic{C ⊢ (fun x : σ ↦ t) : (x : σ) → τ[x]}}}
\end{gather*}
%
The notation \li{τ[x]} stands for a type that may contain \li{x}, and
\hbox{\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{Fun}$'$ coincide with \textsc{App} and \textsc{Fun}
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{Fun}$'$:
%
\[\prftree[r]{\textsc{Fun}$'$}
  {
    \prftree[r]{\textsc{Fun} or \textsc{Fun}$'$}
      {\strut\text{\lic|\α : Type, x : α ⊢ x : α|}}
      {\strut\text{\lic|\α : Type ⊢ (fun x : α ↦ x) : α → α|}}
  }
  {\strut\text{\lic|\⊢ (fun α : Type ↦ fun 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---should also be checked, using the
same type system. 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}.

Remarkably, universal quantification is simply an alias for a dependent type:
\li{∀x : σ, τ} abbreviates \li{(x : σ) → τ}. This will become clearer below.

\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{ℤ → ℕ}). 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}.''

It turns out that the two concepts not only \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, it also means 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
\begin{center}
``Is \li{H} a proof of \li{P}?''
\end{center}
becomes equivalent to
\begin{center}
``Does the term \li{H} have type \li{P}?''
\end{center}
As a result, inside of Lean, there is no proof checker, only a type checker.
Proofs are checked by the type checker.

Let us review the dramatis personae one by one. We use the mathematical
variables \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 functions from \li{σ} to \li{τ}.
\item \li{(x : σ) → τ[x]} is the dependent type of functions 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 of type \li{(x : σ) → Q[x]}, 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{fun 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 theorem or hypothesis is a proof.
\item \li{H t}, which instantiates the leading \li{∀} 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 modus
  ponens.
\item \li{fun h : P ↦ H[h]} is a proof of \li{P → Q},
  assuming \li{H[h]} is a proof of \li{Q} for all \li{h : P}.
\item \li{fun x : σ ↦ H[x]} is a proof of \li{∀x : σ, Q[x]},
  assuming \li{H[x]} is a proof of \li{Q[x]} for all \li{x : σ}.
\end{itemize}
%
The last two cases are justified by the \li{Fun}$'$ rule. In a structured
proof, as opposed to a raw proof term, we would write \li{assume} or \li{fix}
instead of \li{fun}, and we would probably want to repeat the conclusion using
\li{show} for readability, as follows:
%
\begin{lstlisting}[multicols=2]
theorem case_4 :
  P → Q :=
assume h : P
show Q from
  H[h]
theorem case_5 :
  ∀x : σ, Q[x] :=
fix x : τ
show Q[x] from
  H[x]
\end{lstlisting}

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}
%
In the broad sense, 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 ``\hbox{\li{t}} has type~\li{u}'' and the notion that
universes are types of types.

Some Lean commands have two names but are essentially the same by the PAT
principle. This is the case for \li{fix} and \li{assume};
indeed, both are \li{LoVelib} aliases for \li{fun}.
%
There are also pairs with slightly different behavior, such as
\li{def}/\li{theorem} and \li{let}/\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
theorem, the proof itself 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 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
\lic|intro x|       & \lic|fix x : τ|     & \lic|fun x ↦| \\
\lic|intro h|       & \lic|assume h : P|  & \lic|fun h ↦| \\
\lic|have k := H|   & \lic|have k := H|   & \lic|(fun k ↦ …) H| \\
\lic|let x := t|    & \lic|let x := t|    & \lic|(fun x ↦ …) t| \\
\lic|exact (H : P)| & \lic|show P from H| & \lic|H : P| \\
\lic|calc|          & \lic|calc|          & \lic|calc| \\
\bottomrule
\end{tabular}}

\vskip4\smallskipamount

\noindent
Notice that \li{let x := t} followed by \li{u} is essentially a
way of writing \li{(fun x ↦ u) t}, except that $\beta$-reduction is disabled.

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

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 the end of
Section~\ref{ssec:recursion-on-lists}:

\lstinputlisting[linerange=reverse_def-q]{../lean/LoVe/LoVe02_ProgramsAndTheorems_DemoMaster.lean}
%
In fact, \li{reverse} exists as \li{List.reverse} in Lean's standard library,
with a more efficient but less convenient definition for reasoning.
A useful property to prove is that \li{reverse} is its own inverse:
\hbox{\li{reverse (reverse xs) =}} \li{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}}\]
%
Notice the unpleasant presence of \,\hbox{\li{++ [x]}} inside the double
\hbox{\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 theorem:
%
\lstinputlisting[linerange=reverse_append-q]{../lean/LoVe/LoVe04_ForwardProofs_DemoMaster.lean}
%
The theorem's proof arguably 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 theorem we are proving
(\li{reverse_append}).

We explicitly pass \li{xs} as an 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 theorem will not be applied to
\li{x :: xs}, which could lead to a circular proof: ``To prove
\li{reverse_append} \li{(x :: xs)}, use \li{reverse_append} \li{(x :: xs)}.''
Lean's termination checker would notice that the proof 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 theorem we need is the one on \li{xs}.''

For reference, a tactical proof would be as follows:
%
\lstinputlisting[linerange=reverse_append_tactical-q]{../lean/LoVe/LoVe04_ForwardProofs_DemoMaster.lean}

The theorem would also be provable, and useful, if we put \li{[y]} instead of
\hbox{\li{ys}.} But it is a good habit to state theorems 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 theorems 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 commas.
The general format is
%
\begin{quote}
\begin{tabular}{@{}l@{}}
\lic|theorem| \,{\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{}\phantom{\li{xx}}\ttvar{statement} \\
\noindent\hbox{}\phantom{\li{xx}}\lic$|$\, \ttvar{patterns}$_\texttt{1}$ \,\lic$=>$\, \ttvar{proof}$_\texttt{1}$ \\
\noindent\hbox{}\phantom{\li{xx}}\phantom{\lic$|$\, \ttvar{pa}}$\vdots$ \\
\noindent\hbox{}\phantom{\li{xx}}\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, but \li{theorem} considers the defined term or
the proof opaque, whereas \li{def} keeps it transparent. Since the actual
proofs are irrelevant once a theorem 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 and recursion 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 theorem we prove. Lean's
termination checker is used to establish well-foundedness of the proof by
induction.

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

Induction by pattern matching and recursion is 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 and recursion is not
available for inductive predicates, which are the topic of
Chapter~\ref{chap:inductive-predicates}. For these reasons, we will often
prefer the \li{induction} tactic.

\section{Summary of Newly Introduced 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 theorem \\
\lic|let| & introduces a local definition \\
\lic|show| & 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 theorem \\
\lic|let| & introduces a local definition \\
\end{xltabular}

\endgroup
