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

In this chapter, we see how to prove Lean lemmas 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 lemma, the lemma statement is the
initial goal. A proof is complete once all (sub)goals have been eliminated
using suitable tactics. The tactics described here are documented in more
detail in Chapter~5 of \emph{Theorem Proving in Lean}
\cite{theorem-proving-in-lean} and Chapter~6 of \emph{The Lean Reference
Manual} \cite{lean-reference-manual}.

Tactics are a \emph{backward} proof mechanism. They start from the goal and
work backwards towards the already proved lemmas. Consider the lemmas
\li{a}, \li{a → b}, and \li{b → c} and the goal \li{⊢ c}. An informal backward
proof is as follow:
%
\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 lemma \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}.

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

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

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{c : τ} 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/love02_backward_proofs_demo_master.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, it
has the meaning ``\li{a} implies that \li{b} implies \li{a},'' or equivalently
``\li{a} and \li{b} imply \li{a}.'' In the example, three tactics are invoked,
each on its own line. Let us trace their behavior:
%
\begin{itemize}
\item[1.] Initially, the goal is simply the lemma statement:
  \[\hbox{\lic{⊢ ∀a b : Prop, a → b → a}}\]

\item[2.] The \li{intros a b} tactic tells Lean to fix two free variables,
  \hbox{\li{a}}~and~\li{b}, corresponding to the two bound variables of the same names.
  Often, we name the free variables after the bound variables. 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}}\]

\item[3.] The \li{intros 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}.

\item[4.] 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.
\end{itemize}

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{intros} invocations by
declaring the variables and hypotheses as parameters of the lemma, as follows:

\lstinputlisting[linerange=fst_of_two_props₂-q]{../lean/love02_backward_proofs_demo_master.lean}

If the proof consists of a single tactic invocation, we can use \li{by}
instead. The syntax \texttt{by} \ttvar{tactic} abbreviates
\texttt{begin} \ttvar{tactic} \texttt{end}:

\lstinputlisting[linerange=fst_of_two_props₃-q]{../lean/love02_backward_proofs_demo_master.lean}
%
Here is an example with multiple \li{apply}s in sequence:

\lstinputlisting[linerange=prop_comp-q]{../lean/love02_backward_proofs_demo_master.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{intros} and \li{apply} tactics. These are the staples
of tactical proofs. Other basic tactics include \li{refl}, \li{exact},
\li{assumption}, and \li{cc}. 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(s)}

\smallskip

\begin{quote}
\lic{intro} \,$\bigl[$\ttvar{name}$\bigr]$ \\[\jot]
\lic{intros} \,$\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. The plural variant
\li{intros} can be used to move several variables or assumptions at once.

\subsection*{refl}

The \li{refl} 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 expansion of definitions, reduction of an application of a
\li{λ}-expression 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| \li|(n : ℕ)| \li|: ℕ := n + n|:

\begin{center}
\begin{tabular}{@{}rl@{}}
$\alpha$-conversion & \lic|(λx, f x) = (λy, f y)| \\
$\beta$-conversion  & \lic|(λx, f x) a = f a| \\
$\delta$-conversion & \lic|double 5 = 5 + 5| \\
$\zeta$-conversion  & \lic|(let n : ℕ := 2 in n + n) = 4| \\
$\eta$-conversion   & \lic|(λ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}. Since much of Lean's machinery treats terms that are
syntactically equal up to computation uniformly, it usually makes sense to tell
Lean's pretty-printer to aggressively \li{β}-reduce its output. This is what
the the command
%
\begin{lstlisting}
set_option pp.beta true
\end{lstlisting}
%
near the top of the files accompanying this guide achieves.

\subsection*{apply}

\smallskip

\begin{quote}
\lic{apply} \,\ttvar{lemma-or-hypothesis}
\end{quote}
%
The \li{apply} tactic matches the goal's target with the conclusion of the
specified lemma or hypothesis and adds the lemma 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{⊢ 2 + 2 = 4} and
we \li{apply} the lemma \li{false → ?a}, the variable \li{?a} is matched against
\li{2 + 2 = 4}, 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{lemma-or-hypothesis}
\end{quote}
%
The \li{exact} tactic matches the goal's target with the specified lemma or
hypothesis, closing the goal. We can often use \li{apply} in such situations,
but \li{exact} communicates our intentions better. In the example from
Section~\ref{sec:tactic-mode}, we could have used \li{exact ha} instead of
\li{apply ha}.

\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. In the example
from Section~\ref{sec:tactic-mode}, we could have used \li{assumption}
instead of \li{apply ha}.

\subsection*{cc}

The \li{cc} tactic implements an algorithm known as \emph{congruence closure}
\cite{selsam-de-moura-2016} to derive new equalities from those that are
present in the goal. For example, if the goal contains \li{b = a} and
\li{f b ≠ f a} as hypotheses, the algorithm will derive \li{f b = f a} from
\li{b = a} and discover a contradiction with \li{f b ≠ f a}. The \li{cc} tactic
is also suitable for more pedestrian work, such as proving
\li{hb : b ⊢ a ∨ b ∨ c} or discovering a contradiction among the goal's
hypotheses.

In addition, \li{cc} can be used to reason up to associativity
(e.g., \hbox{\li{(a + b) + c =}} \hbox{\li{a + (b + 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}.

At this point, you might wonder, ``So what does \li{cc} do exactly?'' Of
course, you could look up the reference \cite{selsam-de-moura-2016} given
above to the scientific paper that describes its underlying algorithm, or even
read the source code. 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{cc} and other tactics, you will develop some intuition
about what kinds of goal they work well on. This is one of the many reasons why
interactive theorem proving can only be learned 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}.

\subsection*{sorry}

The \li{sorry} proof command we encountered in
Chapter~\ref{chap:definitions-and-statements} is also available 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/love02_backward_proofs_demo_master.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
immediately after each comma, you can see the effect of the command on that
line. If you want to see the proof state after the last command, you need to
move the cursor right before the \li{e} of the keyword \li{end}. 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
lemmas
%
\begin{center}
\begin{tabular}{@{}r@{}l@{}}
\lic|and.intro| & \lic| : ?a → ?b → ?a ∧ ?b| \\
\lic|and.elim_left| & \lic| : ?a ∧ ?b → ?a| \\
\lic|and.elim_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 lemma.

The three lemmas above are the introduction rule and the two elimination rules
associated with conjunction. An \emph{introduction rule} for a symbol (e.g.,
\li{∧}) is a lemma whose conclusion contains that symbol. Dually, an
\emph{elimination rule} has the symbol in an assumption. In the above proof, we
apply the introduction rule associated with \li{∧} to prove the goal
\li{⊢ b ∧ a}, and we apply the two elimination rules to extract
\li{b}~and~\li{a} from the hypothesis \li{a ∧ b}.

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.elim_right}, we have the goal
%
\[\hbox{\ctxt{a} \ctxt{b} \lic{: Prop,} \ctxt{hab} \lic{: a ∧ b ⊢ ?m_1 ∧ b}}\]
%
The tactic \li{exact hab} matches \li{?m_1} (in the target) with \li{a} (in
\hbox{\li{hab}).} Because variables can occur both in the hypothesis or lemma that is
\li{apply}d and in the target, in general the procedure used to instantiate
variables to make two terms syntactically equal is called \emph{unification}.
Matching is a special case of unification where one of the two terms contains
no variables. In practice, goals with variables are rare, so
Lean's unification usually amounts to matching.

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

The following is an alternative proof of the lemma \li{and_swap}:

\lstinputlisting[linerange=and_swap₂-q]{../lean/love02_backward_proofs_demo_master.lean}
%
The lemma is stated differently, with \li{a} and \li{b} as \li{∀}-quantified
variables instead of parameters of the lemma. 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{elim_right}
and \li{and.elim_left} directly to the hypothesis \li{a ∧ b} to obtain \li{b}
and \li{a}, respectively, instead of waiting for the lemmas' 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{?m_1} variable.

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

The \li{∀}-quantifiers in \li{or.intro_left} and \li{or.intro_right} can be
instantiated directly by applying the lemma name to the value we want to
instantiate with, via simple juxtaposition. Thus,
\li{or.}\allowbreak\li{intro_left} \li{false} corresponds to the lemma \hbox{\li{?a →}}
\hbox{\li{?a ∨ false}.} This is the forward style.

Alternatively, we can invoke \li{apply or.intro_left}
on a goal of the form \li{… ⊢ c ∨ d}. This instantiates the lemma with
\li{?a :=} \li{c} and \li{b := d}. The new subgoal is \li{… ⊢ c}. This is
the backward style.

Both \li{or.intro_left} and \li{or.intro_right} 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.intro_right} yields the
unprovable subgoal \li{⊢ false}.

The \li{or.elim} rule may seem counterintuitive at a 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 \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 concept 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.elim_left| & \lic| : (?a ↔ ?b) → ?a → ?b| \\
\lic|iff.elim_right| & \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/love02_backward_proofs_demo_master.lean}
%
Again, we instantiate a \li{∀}-quantifier in a forward fashion:
\li{exists.}\allowbreak\li{intro 0} is the lemma \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 $\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 will succeed at
extracting 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.

Negation (\li{not}) is defined in terms of implication and falsehood: \li{¬ a}
abbreviates \li{a →} \li{false}. 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.by_contradiction| & \lic| : (¬ ?a → false) → ?a| \\
\end{tabular}
\end{center}

Finally, implication (\li{→}) and universal quantification (\li{∀}) are the
proverbial dogs that did not bark. For both of them, the \li{intro} tactic is
the introduction principle, and application is the elimination principle. For
example, given the lemmas \li{hab :} \li{a → b} and \li{ha : a}, the
juxtaposition \li{hab ha} is a lemma 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}(\li{s}) 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 lemma 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 lemma 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_def} (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 next step, you would typically
  \li{apply} a lemma or hypothesis of the form \li{P →} \li{false} or \li{¬ P}.

\item When you face several choices (e.g., between \li{or.intro_left} and
  \li{or.intro_}\allowbreak\li{right}), remember which choices you have made,
  and backtrack when you reach a dead end or have the impression 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 lemma statement, the current goal might
  be unprovable (e.g., if you used unsafe rules such as \hbox{\li{or.intro_left}).}
\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 lemmas are introduction rules specifying that \li{=} is an
equivalence relation. The fourth lemma is an elimination rule that allows us to
replace equals for equals in an arbitrary context, represented by the
higher-order variable~\li{?p}.

An example will show how this works. Below, we apply \li{eq.subst}
to rewrite \li{f a b} to \li{f a' b}, using the equation \li{a = a'}:
%
\lstinputlisting[linerange=cong_fst_arg-q]{../lean/love02_backward_proofs_demo_master.lean}
%
The \li{eq.subst} instance we use has \li{?a := a},
\li{?b := a'}, and \hbox{\li{?p :=}} \hbox{\li{(λx, f a b = f x b)}:}
%
\[\hbox{\lic{a = a' → (λx, f a b = f x b) a → (λx, f a b = f x b) a'}}\]
%
In $\beta$-reduced form:
%
\[\hbox{\lic{a = a' → f a b = f a b → f a b = f a' b}}\]
%
The lemma's first assumption matches the hypothesis \hbox{\li{ha}} \li{:} \hbox{\li{a = a'},}
which is passed as argument in the first \li{apply} invocation. The lemma's
second assumption is a trivial equality that can be proved by
\li{apply eq.refl} or \li{refl}. The lemma's conclusion matches the goal's
target. Notice how a higher-order variable (e.g., \hbox{\li{?p}}) can
represent an arbitrary context (e.g., \li{f … b}) around a term (e.g., \li{a} or
\hbox{\li{a'}).} This works because \li{apply} unifies up to computation,
including $\beta$-conversion.

The \li{eq.subst} lemma can be used several times in sequence, as follows:
%
\lstinputlisting[linerange=cong_two_args-q]{../lean/love02_backward_proofs_demo_master.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{refl} is applicable:
%
\lstinputlisting[linerange=cong_two_args₂-q]{../lean/love02_backward_proofs_demo_master.lean}

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

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

The rewriting tactic \li{rw} and its relative \li{simp} replace equals for
equals. Unlike \li{cc}, they use equations as left-to-right rewrite rules. 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 ⊢| & rewrites the target (the default) \\
\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} \,\ttvar{lemma-or-constant}\, $\bigl[$\lic{at} \,\ttvar{position}$\bigr]$
\end{quote}
%
The \li{rw} tactic rewrites the goal using a single equation as a left-to-right
rewrite rule. It searches for the first subterm that matches the equation's
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 lemma as a right-to-left rewrite rule, put
a short left arrow (\li{←}) in front of the lemma's name.

Given the lemma \li{l : ∀x, g x = f x} and the goal \hbox{\li{⊢ h (f a) (g b)}} \li{(g c)},
the tactic \li{rw l} produces the subgoal \li{⊢ h (f a) (f b) (g c)},
whereas \li{rw ←l} produces the subgoal \li{⊢ h (g a) (g b) (g c)}.

Instead of a lemma, we can also specify the name of a constant. This will
attempt to use one of the constant's defining equations as rewrite rules.
For technical reasons, this does not work with \li{not} (\li{¬}), and we must
use \li{rw not_def} instead.

%\begin{quote}
%\lic{rw} \,\lic{[}\ttvar{lemma-or-constant}$_\texttt{1}$\lic{,} $\dots$\lic{,}
%\ttvar{lemma-or-constant}$_\ttvar{n}$\lic{]}\,
%$\bigl[$\lic{at} \,\ttvar{position}$\bigr]$\kern-\leftmargin
%\end{quote}
%%
%The above syntax abbreviates \li{rw}
%\ttvar{lemma-or-constant}$_\texttt{1}$, $\dots$, \li{rw}
%\ttvar{lemma-\allowbreak or-constant}$_\ttvar{n}$. (The thick, small
%brackets \li{[}\,\li{]} are part of the syntax.)

\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. The simp set can be extended by
putting the \li{@[simp]} attribute on lemmas. Unlike \li{rw}, \li{simp} can
rewrite terms containing bound variables (e.g., occurrences of \li{x} in the
body of \li{λx, …}, \li{∀x, …}, or \li{∃x, …}).

\begin{quote}
\lic{simp} \,\lic{[}\ttvar{lemma-or-constant}$_\texttt{1}$\lic{,} $\dots$\lic{,}
\ttvar{lemma-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 lemmas are temporarily added to
the simp set. In the lemma list, an asterisk (\li{*}) can be use to represent
all hypotheses.%
\pagebreak[2]
The minus sign (\li{-}) in front of a lemma name temporarily
removes the lemma 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 lemma \li{l : ∀x, g x = f x} and the goal \hbox{\li{⊢ h (f a) (g b)}} \li{(g c)},
the tactic \li{simp [l]} 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 lemma, we can also specify the name of a constant. This
temporarily adds the constant's defining equations to the simp set.

To find out what \li{simp} does, you can enable tracing via the command
%
\begin{lstlisting}
set_option trace.simplify.rewrite true
\end{lstlisting}

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

The \li{induction'} tactic performs structural induction on an inductive
type. \emph{Structural induction} simply means that the induction follows the
structure of the inductive type. For natural numbers constructed from
\li{nat.zero} and \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 \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
lemmas, \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/love02_backward_proofs_demo_master.lean}
%
The first \li|{ }| encloses the base case
\hbox{\li|⊢ add 0 0 = 0|.} The second block 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 local variable \li|n| in the induction step should not be confused with the
\li|n| in the lemma statement. Like mathematicians, \hbox{\li{induction'}} tries to
reuse variable names that are no longer needed. The name \li{ih} for the
induction hypothesis, in the induction step, is also generated by the
\li{induction'} tactic.

We can keep on proving lemmas by structural induction:

\lstinputlisting[linerange=add_succ-q]{../lean/love02_backward_proofs_demo_master.lean}
\betweenlistings
\lstinputlisting[linerange=add_comm-q]{../lean/love02_backward_proofs_demo_master.lean}
\betweenlistings
\lstinputlisting[linerange=add_assoc-q]{../lean/love02_backward_proofs_demo_master.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{cc}, know about this. The
following commands achieve this for \li{add}:

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

\lstinputlisting[linerange=mul_add-q]{../lean/love02_backward_proofs_demo_master.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
  usually makes 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 lemmas should be proved first.
\end{itemize}

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

\subsection*{induction$\pmb{'}$}

\smallskip

\begin{quote}
\lic{induction'} \,\ttvar{term} $\bigl[$\li{with}
  \ttvar{name}$_\texttt{1}$ $\ldots$
  \ttvar{name}$_\ttvar{n}\bigr]$
\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{name}$_\texttt{1}$, \ldots,
\ttvar{name}$_\ttvar{n}$ are used for any emerging variables or hypotheses.

Note that the standard Lean tactic for structural induction is called
\li{induction}. The primed variant is provided by \li{mathlib}. It is more
user-friendly and is the only one we will use.

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

The following tactics help us clean up the goal by allowing us to give more
meaningful names to variables or hypotheses or to remove useless hypotheses. We
did not need them so far, but they can be helpful during proof exploration.

\subsection*{rename}

\smallskip

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

\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.

\section{Summary of New Lean Constructs}

\begingroup
\summarysize

\subsection*{Commands}

\noindent
\begin{xltabular}{\textwidth}{@{}p{9em}X@{}}
\lic|set_option| & changes or activates tracing, syntax output, etc. \\
\end{xltabular}

\subsection*{Attribute}

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

\subsection*{Proof Commands}

\noindent
\begin{xltabular}{\textwidth}{@{}p{9em}X@{}}
\lic|begin … end| & invokes a list of tactics in sequence \\
\lic|by| & invokes a single tactic \\
\end{xltabular}

\subsection*{Tactics}

\noindent
\begin{xltabular}{\textwidth}{@{}p{9em}X@{}}
\lic|apply| & matches the goal's target with the lemma's conclusion \\
\lic|assumption| & proves the goal using a hypothesis \\
\lic|cc| & propagates equalities up to to associativity and commutativity \\
\lic|clear| & removes a variable or hypothesis from the goal \\
\lic|exact| & proves the goal using the specified lemma \\
\lic|induction'| & performs structural induction on a variable of an inductive type \\
\lic|intro|(\lic|s|) & moves $\forall$-quantified variables into the goal's hypotheses \\
\lic|refl| & proves \lic|l = r| where \lic|l| and \lic|r| are equal up to computation \\
\lic|rename| & renames a variable or hypothesis \\
\lic|rewrite| & rewrites once using the given lemma 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 or definition \\
\end{xltabular}

\subsection*{Tactic Combinator}

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

\endgroup
