\chapter{Backward Proofs}
\label{chap:backward-proofs}

In this chapter, we see how to prove Lean theorems using tactics, and we review
the most important Lean tactics. A \emph{tactic} is a procedure that operates
on the goal---the proposition to prove---and either fully proves it or produces
new subgoals (or fails). When we state a theorem, the theorem statement is the
initial goal. A proof is complete once all (sub)goals have been eliminated
using suitable tactics. Most of the tactics described here are documented in
more detail in Chapter~5 of \emph{Theorem Proving in Lean 4}
\cite{theorem-proving-in-lean}.

Tactics are a \emph{backward} proof mechanism. They start from the goal and
work backwards towards the already proved theorems. Consider the theorems
\li{a}, \li{a → b}, and \li{b → c} as well as the goal \li{⊢ c}. (Goals, like
typing judgments, are identified by the symbol \li{⊢}.) An informal backward
proof is as follows:
%
\begin{quote}
To prove \li{c}, by \li{b → c} it suffices to prove \li{b}.
\\[\jot]
To prove \li{b}, by \li{a → b} it suffices to prove \li{a}.
\\[\jot]
To prove \li{a}, we use \li{a}. \qed
\end{quote}
%
The telltale sign of a backward proof is the phrase ``it suffices to.'' Notice
how we progress from one \emph{goal} to another (\li{⊢ c}, \li{⊢ b}, \li{⊢ a})
until no goal is left to prove. By contrast, a \emph{forward} proof would start
from the theorem \li{a} and progress, one \emph{theorem} at a time, towards the
desired theorem~\li{c}:
%
\begin{quote}
From \li{a} and \li{a → b}, we have \li{b}.
\\[\jot]
From \li{b} and \li{b → c}, we have \li{c}, as desired. \qed
\end{quote}
%
A forward proof only manipulates theorems, not goals. We will study forward
proofs more deeply in Chapter~\ref{chap:forward-proofs}.

Informal proofs are sometimes written in a mixture of both styles. This is
manageable as long as the backward steps are clearly identified, by such wording
as ``to prove \dots, it suffices to prove \dots.'' It may help to put the \li{⊢}
sign in front of goals as a reminder that these claims have not been proved yet.

Another format for expressing proofs you may be familiar with is natural
deduction. A natural deduction derivation corresponding to the above proof is
given below:
%
\begin{gather*}
\prftree[r]{$\to$E}
  {\strut\text{\lic{\⊢ b → c}}}
  {\prftree[r]{$\to$E}
    {\strut\text{\lic{\⊢ a → b}}}
    {\strut\text{\lic{\⊢ a}}}
    {\strut\text{\lic{\⊢ b}}}}
  {\strut\text{\lic{\⊢ c}}}
\end{gather*}
%
When read from top to bottom, the derivation corresponds to a forward proof;
when read from bottom to top, it corresponds to a backward proof.

\section{Tactic Mode}
\label{sec:tactic-mode}

In Chapter~\ref{chap:programs-and-theorems}, whenever a proof was required,
we simply put a \li{sorry} placeholder. For a tactical proof, we will now write
\li{by} to enter \emph{tactic mode}. In this mode, we can invoke a sequence of
tactics.

Tactics operate on the goal, which consists of the proposition~\li{Q} that we
want to prove and of a local context \li{C}. The local context consists of
variable declarations of the form \li{x : σ} and hypotheses of the
form~\li{h : P}. We write \li{C ⊢ Q} to denote a goal, where \li{C} is a list
of variables and hypotheses and \li{Q} is the goal's target.

To make things more concrete, consider the following Lean example:

\lstinputlisting[linerange=fst_of_two_props-q]{../lean/LoVe/LoVe03_BackwardProofs_DemoMaster.lean}
%
Note that the implication arrow \li{→} is right-associative; this means that
\li{a → b →} \li{a} is the same as \li{a → (b → a)}. Intuitively speaking,
the statement has the meaning ``\li{a} implies that \li{b} implies \li{a},'' or
equivalently ``\li{a} and \li{b} imply \li{a}.''

Initially, the goal is simply the theorem statement:
\[\hbox{\lic{⊢ ∀a b : Prop, a → b → a}}\]

The \li{by} keyword indicates that we enter tactic mode, in which
we can specify a proof by means of tactics. The tactics then follow, one per
line and with the same indentation for all.

The \li{intro a b} tactic tells Lean to fix two free variables,
\hbox{\li{a}}~and~\hbox{\li{b},} corresponding to the two bound variables of
the same names. The tactic mimics how mathematicians work on paper: To prove a
\li{∀}-quantified proposition, it suffices to prove it for some arbitrary but
fixed value of the bound variable. The goal becomes
\[\hbox{\ctxt{a} \ctxt{b} \lic{: Prop ⊢ a → b → a}}\]
where the propositions \li{a} and \li{b} are declared in the goal's local
context, on the left of the \li{⊢} symbol. We often use the same names for the
free variables as for bound variables, as we did here, but this is not
mandatory. In general, it is good practice to use unique names and avoid
shadowing existing variables.

The \li{intro ha hb} tactic tells Lean to move the assumptions
\li{a} and \li{b} to the local context and to call these hypotheses \li{ha}
and \li{hb}. Indeed, to prove an implication, it suffices to take its
left-hand side as hypothesis and prove its right-hand side. The goal becomes
\[\hbox{\ctxt{a} \ctxt{b} \lic{: Prop,} \ctxt{ha} \lic{: a,} \ctxt{hb} \lic{: b ⊢ a}}\]
It is customary to prefix hypothesis names with \li{h}.

The \li{apply ha} tactic tells Lean to match the hypothesis \li{a},
called \li{ha}, against the goal \li{⊢ a}. Since \li{a} is syntactically equal
to \li{a}, we have a match, and this completes the proof.

Informally, in a style reminiscent of pen-and-paper mathematics, we could write
the proof as follows:
%
\begin{quote}
Let \li{a} and \li{b} be propositions.
\\[\jot]
Assume (\li{ha}) \li{a} and (\li{hb}) \li{b} are true.
\\[\jot]
To prove \li{a}, we use hypothesis \li{ha}. \qed
\end{quote}
%
(Mathematicians would probably use numeric tags such as (1) and (2) for the
hypotheses instead of informative names.)

Going back to the Lean proof, we can avoid the \li{intro} invocations by
declaring the variables and hypotheses as parameters of the theorem, as follows:

\lstinputlisting[linerange=fst_of_two_props_params-q]{../lean/LoVe/LoVe03_BackwardProofs_DemoMaster.lean}

Here is an example with multiple \li{apply}s in sequence:

\lstinputlisting[linerange=prop_comp-q]{../lean/LoVe/LoVe03_BackwardProofs_DemoMaster.lean}
%
Putting on our mathematician's hat, we can verbalize the last proof as follows:
%
\begin{quote}
Assume (\li{ha}) \li{a} is true.
\\[\jot]
To prove \li{c}, by hypothesis \li{hbc} it suffices to prove \li{b}.
\\[\jot]
To prove \li{b}, by hypothesis \li{hab} it suffices to prove \li{a}.
\\[\jot]
To prove \li{a}, we use hypothesis \li{ha}. \qed
\end{quote}

\section{Basic Tactics}
\label{sec:basic-tactics}

We already saw the \li{intro} and \li{apply} tactics. These are the staples of
tactical proofs. Other basic tactics include \li{exact}, \hbox{\li{assumption},}
\li{rfl}, and \li{ac_rfl}. These tactics can go a long way, if we are patient
enough to carry out the reasoning using them, without appealing to stronger
proof automation. They can also be used to solve various logic puzzles.

Below, the thin, large square brackets $\bigl[\,\bigr]$ enclose optional syntax.

\subsection*{intro}

\smallskip

\begin{quote}
\lic{intro} \,$\bigl[$\ttvar{name}$_\texttt{1}$ $\ldots$ \ttvar{name}$_\ttvar{n}\bigr]$
\end{quote}
%
The \li{intro} tactic moves the leading \li{∀}-quantified variable or the
leading assumption \li{a →} from the goal's target to the local context. The
tactic takes as an optional argument the name to give to the variable or to the
assumption in the context, overriding the default name. If multiple names
are supplied (i.e., \li{n > 1}), multiple variables or assumptions are moved.

\subsection*{rfl}

The \li{rfl} tactic proves goals of the form \li{⊢ l = r}, where the two sides
\li{l} and \li{r} are syntactically equal \emph{up to computation}. Computation
means first and foremost the expansion of definitions but also the reduction of
an application of an anonymous function to an argument, and more. These
\emph{conversions} have traditional names. The main conversions are listed below
together with examples, in a global context containing \li|def double|
\hbox{\li|(n : ℕ)|} \li|: ℕ := n + n|:

\begin{center}
\begin{tabular}{@{}rl@{}}
$\alpha$-conversion & \lic|(fun x ↦ f x) = (fun y ↦ f y)| \\
$\beta$-conversion  & \lic|(fun x ↦ f x) a = f a| \\
$\delta$-conversion & \lic|double 5 = 5 + 5| \\
$\zeta$-conversion  & \lic|(let n : ℕ := 2; n + n) = 4| \\
$\eta$-conversion   & \lic|(fun x ↦ f x) = f| \\
$\iota$-conversion  & \lic|Prod.fst (a, b) = a| \\
\end{tabular}
\end{center}

Applying conversions repeatedly as left-to-right rewrite rules is called
\emph{reduction}; applying a conversion once in reverse is called
\emph{expansion}.

Briefly, to prove \li{⊢ l = r}, the \li{rfl} tactic expands definitions in
\li{l} and \li{r} and performs $\beta$-reduction and other reductions. It
succeeds if \li{l} and \li{r} become syntactically identical at some point
during this reduction process. Often, \li{rfl} succeeds where a mathematician
would say ``by definition.''

\subsection*{apply}

\smallskip

\begin{quote}
\lic{apply} \,\ttvar{theorem-or-hypothesis}
\end{quote}
%
The \li{apply} tactic matches the goal's target with the conclusion of the
specified theorem or hypothesis and adds the theorem or hypothesis's assumptions
as new goals. The matching is performed up to computation.

We must invoke \li{apply} with care, because it can transform a provable goal
into an unprovable subgoal. For example, if the goal is \li{⊢ True} and we
\li{apply} the theorem \li{False → True}, the conclusion \li{True} is matched
against the goal's target \li{True}, and we end up with the unprovable subgoal
\li{⊢ False}. We say that \li{apply} is \emph{unsafe}. In contrast, \li{intro}
always preserves provability and is therefore \emph{safe}.

\subsection*{exact}

\smallskip

\begin{quote}
\lic{exact} \,\ttvar{theorem-or-hypothesis}
\end{quote}
%
The \li{exact} tactic matches the goal's target with the specified theorem or
hypothesis, closing the goal. We can often use \li{apply} in such situations,
but \li{exact} communicates our intentions better.

\subsection*{assumption}

The \li{assumption} tactic finds a hypothesis from the local context that
matches the goal's target and \li{apply}s it to prove the goal.

\subsection*{ac\_rfl}

The \li{ac_rfl} is similar to \li{rfl}, but it can be used to reason up to
associativity (e.g., \hbox{\li{(a + b) + c =}} \hbox{\li{a + (b}}
\hbox{\li{+ c)}}) and commutativity (e.g, \li{a + b = b + a}).
This works for binary operations that are registered as associative and
commutative, such as \li{+} and \li{*} on arithmetic types, and
\li{∪} and \li{∩} on sets. We will see an example in
Section~\ref{sec:proofs-by-mathematical-induction}.

\subsection*{sorry}

The \li{sorry} proof command we encountered in
Chapter~\ref{chap:programs-and-theorems} can be used at any point in a
tactical proof, as a tactic. It ``proves'' the current goal without actually
proving it. Use with care.

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

Before we learn to reason about natural numbers, lists, or other data types, we
must first learn to reason about the logical connectives and quantifiers of
Lean's logic. Let us start with a simple example:\ commutativity of conjunction
(\li{∧}).

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

At this point, we recommend that you move the cursor over the example in Visual
Studio Code, to see the sequence of proof states. By putting the cursor
on or immediately after each command, you can see the effect of the command on
that line. For the last line, Lean simply reports ``Goals accomplished,''
meaning that no subgoals remain to be proved.

The proof is a typical \li{intro}--\li{apply}--\li{exact} mixture. It uses the
theorems
%
\begin{center}
\begin{tabular}{@{}r@{}l@{}}
\lic|And.intro| & \lic| : ?a → ?b → ?a ∧ ?b| \\
\lic|And.left| & \lic| : ?a ∧ ?b → ?a| \\
\lic|And.right| & \lic| : ?a ∧ ?b → ?b| \\
\end{tabular}
\end{center}
%
\noindent
where the question marks (\li{?}) indicate variables that can be
instan\-tiated---for example, by matching the goal's target against the
conclusion of a theorem. These are called \emph{metavariables}.

The three theorems above are the introduction rule and the two elimination rules
associated with conjunction. An \emph{introduction rule} for a logical symbol
(e.g., \hbox{\li{∧})} is a theorem whose conclusion has that symbol as the
outermost symbol. Dually, an \emph{elimination rule} has the symbol in an
assumption. For each logical symbol, the introduction rules tell us \emph{how to
prove} a proposition with that symbol as the outermost position. By contrast,
the elimination rules tell us \emph{how we must have proved} such a proposition.

In the above proof, we apply the introduction rule for \li{∧} to prove the goal
\li{⊢ b} \li{∧ a}, and we apply the two elimination rules to extract
\li{b}~and~\li{a} from the hypothesis \li{a ∧ b}. It may sound strange that we
``eliminate'' \li{∧} in \li{⊢ b ∧ a} by using a so-called introduction
rule. The terminology is backward because our proofs are backward.

Question marks can also arise in goals. They indicate variables that can be
instantiated arbitrarily. In the middle of the proof above, right after
the tactic \li{apply And.right}, we have the goal
%
\[\hbox{\ctxt{a} \ctxt{b} \lic{: Prop,} \ctxt{hab} \lic{: a ∧ b ⊢ ?left.a ∧ b}}\]
%
where \li{?left.a} is a metavariable.
The tactic \li{exact hab} matches \li{?left.a} (in the target) with \li{a} (in
\hbox{\li{hab}).} The procedure used to
instantiate variables to make two terms syntactically equal is called
\emph{unification}. \emph{Matching} is a special case of unification where one
of the two terms contains no variables, like here.

Incidentally, whenever metavariables appear in goals, additional subgoals will
also appear, with the type of each metavariable as a subgoal (e.g.,
\li{⊢ Prop}). These confusing subgoals are merely a reminder that we will have
to instantiate the metavariables with terms of the right type. We can usually
ignore these subgoals. As soon as the metavariable is instantiated (typically
when we solve another subgoal), its associated subgoal will also go away.

In Lean, unification is performed up to computation. For example, the terms
\li{(fun x ↦ ?m) a} and \li{b} can be unified by taking \li{?m} \li{:=} \li{b},
because \li{(fun x ↦ b) a} and \li{b} are syntactically equal up to
$\beta$-conversion.

The following is an alternative proof of the theorem \li{And_swap}:

\lstinputlisting[linerange=and_swap_braces-q]{../lean/LoVe/LoVe03_BackwardProofs_DemoMaster.lean}
%
The theorem is stated differently, with \li{a} and \li{b} as \li{∀}-quantified
variables instead of parameters of the theorem. Logically, this is equivalent,
but in the proof we must then \li{intro}duce \li{a} and \li{b} in addition to
\li{hab}.

Another difference is the use of curly braces \verb|{|\,\verb|}|. When we face
two or more goals to prove, it is generally good style to put each proof in its
own block enclosed in curly braces. The \verb|{|\,\verb|}| tactic combinator
focuses on the first subgoal; the tactic inside must prove it. In our example,
the \li{apply And.intro} tactic creates two subgoals, \li{⊢ b} and \li{⊢ a}.

A third difference is that we now apply, by juxtaposition, \li{And.}\allowbreak\li{right}
and \li{And.}\allowbreak\li{left} directly to the hypothesis \li{a ∧ b} to obtain \li{b}
and \li{a}, respectively, instead of waiting for the theorems' assumptions to
emerge as new subgoals. This is a small forward step in an otherwise backward
proof. The same syntax is used both to discharge (i.e., prove) a hypothesis and
to instantiate a \li{∀}~quantifier. One benefit of this approach is that we avoid
the potentially confusing \li{?left.a} metavariable.

In the next example, we use juxtaposition to instantiate a \hbox{\li{∀}} quantifier:
%
\lstinputlisting[linerange=f5_if-q]{../lean/LoVe/LoVe03_BackwardProofs_DemoMaster.lean}
%
If \li{h} is the theorem \li{∀n, f n = n}, then \li{h 5} is
the theorem \li{f 5 = 5}.

The introduction and elimination rules for disjunction (\li{∨}) are as
follows:
%
\begin{center}
\begin{tabular}{@{}r@{}l@{}}
\lic|Or.inl| & \lic| : ∀b : Prop, ?a → ?a ∨ b| \\
\lic|Or.inr| & \lic| : ∀b : Prop, ?a → b ∨ ?a| \\
\lic|Or.elim| & \lic| : ?a ∨ ?b → (?a → ?c) → (?b → ?c) → ?c| \\
\end{tabular}
\end{center}

\begin{sloppypar}
The \li{∀}~quantifiers in \li{Or.inl} (``introduction left'') and \hbox{\li{Or.inr}}
(``introduction right'') can be
instantiated directly by applying the theorem name to the value we want to
instantiate with, via simple juxtaposition. Thus,
\li{Or.}\allowbreak\li{inl} \li{False} corresponds to the theorem \hbox{\li{?a →}}
\hbox{\li{?a ∨ False}.} This is the forward style.
\end{sloppypar}

Alternatively, we can invoke \li{apply Or.inl} on a goal of the form
\hbox{\li{… ⊢}} \hbox{\li{c ∨ d}.} This sets \li{?a :=} \li{c} and \li{?b := d}
in the theorem. The new subgoal is \hbox{\li{… ⊢ c}.} This is the backward
style.

Both \li{Or.inl} and \li{Or.inr} are unsafe: If you apply the
wrong one of the two, or either of them too early in a proof, you might end up
with an unprovable subgoal. This is easy to see if you consider the provable
goal \li{⊢ True ∨ False}: \li{apply}ing \li{Or.inr} yields the
unprovable subgoal \li{⊢ False}.

The \li{Or.elim} rule may seem counterintuitive at first glance. In essence,
it states that if we have \li{a ∨ b}, then to prove an arbitrary \li{c}, it
suffices to prove \li{c} when \hbox{\li{a}} holds and when \li{b} holds. You can
think of \li{(?a → ?c) → (?b → ?c) → ?c} as a clever trick to express the
meaning of disjunction using only implication.

The introduction and elimination rules for equivalence (\li{↔}) are as
follows:
%
\begin{center}
\begin{tabular}{@{}r@{}l@{}}
\lic|Iff.intro| & \lic| : (?a → ?b) → (?b → ?a) → (?a ↔ ?b)| \\
\lic|Iff.mp| & \lic| : (?a ↔ ?b) → ?a → ?b| \\
\lic|Iff.mpr| & \lic| : (?a ↔ ?b) → ?b → ?a| \\
\end{tabular}
\end{center}

The introduction and elimination rules for existential quantification (\li{∃})
are
%
\begin{center}
\begin{tabular}{@{}r@{}l@{}}
\lic|Exists.intro| & \lic| : ∀w, (?P w → (∃x, ?P x))| \\
\lic|Exists.elim| & \lic| : (∃x, ?P x) → (∀a, ?P a → ?c) → ?c| \\
\end{tabular}
\end{center}

The introduction rule for \li{∃} can be used to instantiate an existential
quantifier with a witness. For example:

\lstinputlisting[linerange=nat_exists_double_iden-q]{../lean/LoVe/LoVe03_BackwardProofs_DemoMaster.lean}
%
Again, we instantiate a \li{∀}~quantifier in a forward fashion:
\li{Exists.}\allowbreak\li{intro 0} is the theorem \li{?P 0 → (∃x, ?P x)}.
The rule is unsafe: Choosing the wrong witness for \li{x} will result in an
unprovable goal. For example, if the goal is \hbox{\li{⊢ ∃n,}} \li{n > 5} and
we take \li{3} as the witness, we end up with the unprovable subgoal
\li{⊢ 3 > 5}.

The elimination rule for \li{∃} is reminiscent of that for $\lor$. Indeed, a
fruitful way to think of a quantification \li{∃n, ?P n} is as a possibly
infinitary disjunction \hbox{\li{?P 0}} \hbox{\li{∨ ?P 1 ∨ ⋯}.} Similarly,
\li{∀n, ?P n} can be thought of as \li{?P 0 ∧ ?P 1 ∧ ⋯}.

For truth (\li{True}), there is only an introduction rule:
%
\begin{center}
\begin{tabular}{@{}r@{}l@{}}
\lic|True.intro| & \lic| : True| \\
\end{tabular}
\end{center}
%
Truth holds no information whatsoever. If it appears as a hypothesis, it is
completely useless, and there is no elimination rule that can extract any
information from it. The \li{clear} tactic, described in
Section~\ref{sec:cleanup-tactics} below, can be used to remove such useless
hypotheses.

Dually, for falsehood (\li{False}), there is only an elimination rule:
%
\begin{center}
\begin{tabular}{@{}r@{}l@{}}
\lic|False.elim| & \lic| : False → ?a| \\
\end{tabular}
\end{center}
%
There is no way to prove falsehood, but if we somehow have it from somewhere
(e.g., from a hypothesis), then we can derive \hbox{\li{?a}ny}\-thing.

In fact, negation (\li{Not}) is defined in terms of implication and falsehood:
\li{¬ a} abbreviates \li{a →} \li{False}. Intuitively, these mean the same. We
can think of ``not \li{a}'' as saying that ``\li{a} would imply something absurd
(hence not \li{a}).''

Lean's logic is classical, with support for the
law of excluded middle and proof by contradiction:
%
\begin{center}
\begin{tabular}{@{}r@{}l@{}}
\lic|Classical.em| & \lic| : ∀a : Prop, a ∨ ¬ a| \\
\lic|Classical.byContradiction| & \lic| : (¬ ?a → False) → ?a| \\
\end{tabular}
\end{center}

Implication (\li{→}) and universal quantification (\li{∀}) are the
proverbial dogs that did not bark. They do not have introduction or elimination
rules. Instead, for both of them, the \hbox{\li{intro}} tactic is the
introduction principle, and application (as in the \li{λ}-calculus) is the
elimination principle. For example, given the theorems \li{hab} \li{: a → b} and
\li{ha : a}, the application \li{hab ha} is a theorem stating~\li{b}.

For proving logic puzzles involving connectives and quantifiers, we advocate a
``mindless,'' ``video game'' style of reasoning that relies mostly on basic
tactics such as \li{intro} and \li{apply}. Here are some strategies
that often work:

\begin{itemize}
\item If the goal's target is an implication \li{P → Q}, invoke
  \li{intro hP} to move \li{P} into your hypotheses: \,\li{…, hP : P ⊢ Q}.

\item If the goal's target is a universal quantification \li{∀x : σ, Q},
  invoke \li{intro} \li{x} to move \li{x} into the local context:
  \,\li{…, x : σ ⊢ Q}.

\item Look for a theorem or hypothesis whose conclusion has the
  same shape as the goal's target (possibly containing variables that can
  be matched), and \li{apply} it. For example, if the goal's
  target is \li{Q} and you have a theorem or hypothesis of the form
  \li{hPQ : P → Q}, try \li{apply hPQ}.

\item A negated goal \li{⊢ ¬ P} is syntactically equal to \li{⊢ P → False} up to
  computation, so you can invoke \li{intro hP} to produce the subgoal
  \li{hP : P ⊢ False}. Expanding negation's definition by invoking
  \li{rw [Not]} (described in Section~\ref{sec:rewriting-tactics}) is often a
  good strategy.

\item Sometimes you can make progress by replacing the goal by \li{False}, by
  entering \li{apply} \li{False.elim}. As the next step, you would typically
  \li{apply} a theorem or hypothesis of the form \li{P →} \li{False} or \li{¬ P}.

\item When you face several choices (e.g., between \li{Or.inl} and \li{Or.inr}),
  remember which choices you have made, and backtrack when you reach a dead end
  or feel that you are not making any progress.

\item If you suspect that you might have reached a dead end,
  check whether the goal actually is provable under the given assumptions.
  Even if you started with a provable theorem statement, the current goal might
  be unprovable (e.g., if you applied unsafe rules).
\end{itemize}

\section{Reasoning about Equality}
\label{sec:reasoning-about-equality}

Equality (\li{=}) is also a basic logical constant. It is characterized by the
following introduction and elimination rules:
%
\begin{center}
\begin{tabular}{@{}r@{}l@{}}
\lic|Eq.refl| & \lic| : ∀a, a = a| \\
\lic|Eq.symm| & \lic| : ?a = ?b → ?b = ?a| \\
\lic|Eq.trans| & \lic| : ?a = ?b → ?b = ?c → ?a = ?c| \\
\lic|Eq.subst| & \lic| : ?a = ?b → ?P ?a → ?P ?b| \\
\end{tabular}
\end{center}
%
The first three theorems are introduction rules specifying that \hbox{\li{=}} is an
equivalence relation. The fourth theorem is an elimination rule that allows us to
replace equals for equals in an arbitrary context, represented by the
metavariable~\li{?P}.

An example will show some of these rules in action. Below, we apply \hbox{\li{Eq.trans}}
and \hbox{\li{Eq.symm}} to prove \li{a = c} using the equations \li{a = b}
and \li{c = b}:
%
\lstinputlisting[linerange=eq_trans_symm-q]{../lean/LoVe/LoVe03_BackwardProofs_DemoMaster.lean}

Since rewriting in this way is such a common operation, Lean provides a
\li{rw} tactic to achieve the same result. The tactic will also notice if
\li{rfl} is applicable:
%
\lstinputlisting[linerange=eq_trans_symm_rw-q]{../lean/LoVe/LoVe03_BackwardProofs_DemoMaster.lean}

A note on parsing: Equality binds more tightly than the logical
connectives. Thus, \li{a = b ∧ c = d} is read as \li{(a = b) ∧}
\hbox{\li{(c = d)}.}

\section{Rewriting Tactics}
\label{sec:rewriting-tactics}

The rewriting tactic \li{rw} and its relative \li{simp} replace equals for
equals. They use equations as left-to-right rewrite rules, replacing occurrences
of the left-hand side by the right-hand side.

By default, they operate on the goal's target, but they can also be used to
rewrite hypotheses specified using the \li{at} keyword:
%
\begin{center}
\begin{tabular}{@{}ll@{}}
\li|at h|$_\texttt{1}$ $\dots$ \li|h|$_\ttvar{n}$ & rewrites the specified hypotheses \\
\li|at *| & rewrites all hypotheses and the target \\
\end{tabular}
\end{center}

\subsection*{rw}

\smallskip

\begin{quote}
\lic{rw} \,\lic{[}\ttvar{theorem-or-constant}$_\texttt{1}$\lic{,} $\dots$\lic{,}
\ttvar{theorem-or-constant}$_\ttvar{n}$\lic{]}\,
\tabletbreak{\qquad}$\bigl[$\lic{at}~\ttvar{position}$\bigr]$\kern-\leftmargin
\end{quote}
%
The \li{rw} tactic rewrites the goal using one or more equations as left-to-right
rewrite rules. It searches for the first subterm that matches any of the
equations' left-hand side; once found, all occurrences of that subterm are replaced by the
right-hand side of the equation. If the equation contains variables, these are
instantiated as necessary. To use a theorem in reverse, as a right-to-left
rewrite rule, put a short left arrow (\li{←}) in front of the theorem's name.

Thus, given the theorem \li{hg : ∀x, g x = f x} and the goal
\hbox{\li{⊢ h (f a)}} \hbox{\li{(g b)}} \hbox{\li{(g c)},}
the tactic \li{rw [hg]} produces the subgoal \li{⊢ h (f a)} \hbox{\li{(f b)}} \li{(g c)},
whereas \li{rw [←hg]} produces the subgoal \hbox{\li{⊢ h (g a)}}
\hbox{\li{(g b)}} \hbox{\li{(g c)}.}

Instead of a theorem, we can also specify the name of a constant. This will
attempt to use one of the constant's defining equations as rewrite rules.

\subsection*{simp}

\smallskip

\begin{quote}
\lic{simp} \,$\bigl[$\lic{at} \ttvar{position}$\bigr]$
\end{quote}
%
The \li{simp} tactic rewrites the goal using a standard set of rewrite rules,
called the \emph{simp set}, exhaustively. Each equation in the simp set is used
as a left-to-right rewrite rule. The simp set contains various rules about
predefined symbols (e.g., arithmetic and list operators) and can be extended by
putting the \li{@[simp]} attribute on suitable theorems.
%Unlike \li{rw},
%\li{simp} can rewrite terms containing bound variables (e.g., occurrences of
%\li{x} in the body of \li{fun x ↦ …}, \li{∀x, …}, or \li{∃x, …}).

\begin{quote}
\lic{simp} \,\lic{[}\ttvar{theorem-or-constant}$_\texttt{1}$\lic{,} $\dots$\lic{,}
\ttvar{theorem-or-constant}$_\ttvar{n}$\lic{]}\,
\tabletbreak{\qquad}$\bigl[$\lic{at} \ttvar{position}$\bigr]$\kern-\leftmargin
\end{quote}
%
For the above \li{simp} variant, the specified theorems are temporarily added to
the simp set. In the theorem list, an asterisk (\li{*}) can be use to represent
all hypotheses. The minus sign (\li{-}) in front of a theorem name temporarily
removes the theorem from the simp set. A powerful incantation that both simplifies
the hypotheses and uses the result to simplify the goal's target is
\li{simp [*] at *}.

Given the theorem \li{hg : ∀x, g x = f x} and the goal \hbox{\li{⊢ h (f a) (g b)}} \li{(g c)},
the tactic \li{simp [hg]} produces the subgoal
\hbox{\li{⊢ h (f a) (f b)}} \hbox{\li{(f c)},} where both \li{g b} and \li{g c} have been
rewritten. Instead of a theorem, we can also specify the name of a constant. This
temporarily adds the constant's defining equations to the simp~set.

At this point, you might wonder, ``So what does \li{simp} do exactly?'' Of
course, you could study the source code or look up the scientific literature.
But this might not be the most efficient use of your time. In truth, even expert
users of proof assistants do not fully understand the behavior of the tactics
they use daily. The most successful users adopt a relaxed, sporty attitude,
trying tactics in sequence and studying the emerging subgoals, if any, to see if
they are on the right path.

As you keep on using \li{simp} and other tactics, you will develop some intuition
about what kinds of goals they work well on. This is one of the many reasons why
interactive theorem proving can be learned only by doing. Often, you will not
understand exactly what Lean does---why a tactic succeeds, or fails. Theorem
proving can be very frustrating at times. The advice printed in large, friendly
letters on the cover of \emph{The Hitchhiker's Guide to the Galaxy} applies
here: \textsc{don't panic}.

\section{Proofs by Mathematical Induction}
\label{sec:proofs-by-mathematical-induction}

The \li{induction} tactic performs structural induction on a value of an
inductive type. \emph{Structural induction} means that the induction follows the
structure of the inductive type. For natural numbers constructed from
\li{Nat.zero} and \hbox{\li{Nat.succ},} structural induction corresponds to
standard mathematical induction: To prove \hbox{\li{p n},} it suffices to prove
\li{p 0} and \li{∀k, p k → p (k + 1)}. Equipped with \hbox{\li{induction},} we
can reason about the addition and multiplication operations we defined by
recursion in Section~\ref{sec:function-definitions}.

Addition is defined by recursion on its second argument. We will prove two
theorems, \li{add_zero} and \li{add_succ}, that give us alternative equations
that recurse on the \emph{first} argument. We start with \li{add_zero}:

\lstinputlisting[linerange=add_zero-q]{../lean/LoVe/LoVe03_BackwardProofs_DemoMaster.lean}
%
The induction tactic is followed by two subproofs identified by the constructor
they correspond to. In addition, any variables or hypotheses specific to the
subproof can be named explicitly after the name of the constructor.

The first case, labeled \li{zero}, corresponds to the base case
\hbox{\li|⊢ add 0 0 = 0|.} The second case, labeled \li{succ}, corresponds to
the induction step
%
\[\text{\ctxt{n'} \lic|: ℕ,| \ctxt{ih} \lic|: add 0 n' = n' ⊢ add 0 (Nat.succ n') = Nat.succ n'|}\]
%
The names \li{n'} and \li{ih} specified after \li{succ} are the names we give to
the argument of \li{Nat.succ} and the induction hypothesis, respectively. Other
names are possible, but it is generally good practice to call the induction
hypothesis \li|ih|.

We can keep on proving theorems by structural induction:

\lstinputlisting[linerange=add_succ-q]{../lean/LoVe/LoVe03_BackwardProofs_DemoMaster.lean}
\betweenlistings
\lstinputlisting[linerange=add_comm-q]{../lean/LoVe/LoVe03_BackwardProofs_DemoMaster.lean}
\betweenlistings
\lstinputlisting[linerange=add_assoc-q]{../lean/LoVe/LoVe03_BackwardProofs_DemoMaster.lean}

Once we have proved that a binary operator is commutative and associative, it
is a good idea to let Lean's automation, notably \li{ac_rfl}, know about this. The
following commands achieve this for \li{add}:

\lstinputlisting[linerange=is_commutative_associative-q]{../lean/LoVe/LoVe03_BackwardProofs_DemoMaster.lean}
%
(The \li{instance} mechanism will be explained in
Chapter~\ref{chap:functional-programming}.) The following example uses the
\li{ac_rfl} tactic to reason up to associativity and commutativity of \li{add}:

\lstinputlisting[linerange=mul_add-q]{../lean/LoVe/LoVe03_BackwardProofs_DemoMaster.lean}

Here are a few hints on how to carry out proofs by induction:

\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. In particular,
  if a function is defined by recursion on its \textit{n}th argument, it
  can make sense to perform the induction on that argument.

\item If the base case of an induction is difficult, this is often a sign that
  the wrong variable was chosen or that some theorems should be proved first.
\end{itemize}

\section{Induction Tactic}
\label{sec:induction-tactic}

\subsection*{induction}

\smallskip

\begin{quote}
\begin{tabular}{@{}l@{}}
\lic|induction| \,\ttvar{term} \,$\bigl[$\lic|with| \\
\lic$|$\, \ttvar{constructor}$_\texttt{1}$ \ttvar{names}$_\texttt{1}$
  \,\lic|=>|\, \ttvar{tactics}$_\texttt{1}$ \\
\noindent\hbox{}\phantom{\texttt{|}\, \ttvar{pa}}$\vdots$ \\
\lic$|$\, \ttvar{constructor}$_{\ttvar{n}}$ \ttvar{names}$_{\ttvar{n}}$
  \,\lic|=>|\, \ttvar{tactics}$_\ttvar{n}\bigr]$
\end{tabular}
\end{quote}
%
The \li{induction} tactic performs structural induction on the specified term.
This gives rise to as many subgoals as there are constructors in the definition
of the term's type. Induction hypotheses are available as hypotheses in the
subgoals corresponding to recursive constructors (e.g., \li{Nat.succ} or
\li{List.cons}). The optional names \ttvar{names}$_\texttt{1}$, \ldots,
\ttvar{names}$_\ttvar{n}$ are used for any emerging variables or hypotheses.

\section{Cleanup Tactics}
\label{sec:cleanup-tactics}

The following tactics help us clean up the goal. We did not need them so far,
but they can be helpful during proof exploration.

\subsection*{clear}

\smallskip

\begin{quote}
\lic{clear} \,\ttvar{variable-or-hypothesis}$_\texttt{1}$ $\dots$
\tabletbreak{\qquad}\ttvar{variable-or-hypothesis}$_\ttvar{n}$
\end{quote}
%
The \li{clear} tactic removes the specified variables and hypotheses, as long
as they are not used anywhere else in the goal.

\subsection*{rename}

\smallskip

\begin{quote}
\lic{rename} \,\ttvar{type-of-variable-or-proposition-of-hypothesis} \,\li{=>}\, \ttvar{new-name}\kern-\leftmargin
\end{quote}
%
The \li{rename} tactic changes the name of a variable or hypothesis.

\section{Summary of New Lean Constructs}

\begingroup
\summarysize

\subsection*{Attribute}

\noindent
\begin{xltabular}{\textwidth}{@{}p{9em}X@{}}
\lic|@[simp]| & adds a theorem to the simp set \\
\end{xltabular}

\subsection*{Proof Command}

\noindent
\begin{xltabular}{\textwidth}{@{}p{9em}X@{}}
\lic|by| & initiates a tactical proof \\
\end{xltabular}

\subsection*{Tactics}

\noindent
\begin{xltabular}{\textwidth}{@{}p{9em}X@{}}
\lic|ac_rfl| & proves \lic|l = r| up to associativity and commutativity \\
\lic|apply| & matches the goal's target against the theorem's conclusion \\
\lic|assumption| & proves the goal using a hypothesis \\
\lic|clear| & removes a variable or hypothesis from the goal \\
\lic|exact| & proves the goal using the specified theorem \\
\lic|induction| & performs structural induction on a variable of an inductive type \\
\lic|intro| & moves $\forall$-quantified variables into the goal's hypotheses \\
\lic|rename| & renames a variable or hypothesis \\
\lic|rfl| & proves \lic|l = r| up to computation \\
\lic|rw| & rewrites once using the given theorem as a left-to-right rewrite rule \\
\lic|simp| & rewrites using a set of preregistered rewrite rules exhaustively \\
\lic|sorry| & stands for a missing proof \\
\end{xltabular}

\subsection*{Tactic Combinator}

\noindent
\begin{xltabular}{\textwidth}{@{}p{9em}X@{}}
\texttt{\{} \ldots{} \texttt{\}} & focuses on the first subgoal; needs to prove that subgoal \\
\end{xltabular}

\endgroup
