\chapter{Tactical Proofs}
\label{chap:tactical-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 formula to prove---and either fully solves it or
produces new subgoals. 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}.

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

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

Tactics operate on the proof goal, which consists of the conjecture~\li{χ} that
we want to prove and of a context $\Gamma$ that provides constant declarations
of the form \li{c : τ} and hypotheses of the form~\li{h : φ}. We write
\li{C, H ⊢ χ} to denote a goal, where \li{C} is a set of (local) constants,
\li{H} is a set of (local) hypotheses, and \li{χ} is the goal's conclusion. The
constants and hypotheses form a set; the comma is read as set union. We call
\li{C, H} the \emph{local context} of the goal.

This will become clearer with an example:

\lstinputlisting[linerange=fst_of_two_props-q]{../lean/love02_tactical_proofs_demo_master.lean}
%
Note that the implication arrow \li{→} is right-associative; this means
that \li{a → b → a} is the same as \li{a → (b → a)}. In the example, three
tactics are invoked, each on its own line. Let us trace their behavior:
%
\begin{enumerate}
\item Initially, the goal is simply the lemma statement:
  \[\hbox{\li{⊢ ∀a b : Prop, a → b → a}}\]

\item The \li{intros a b} tactic tells Lean to fix two arbitrary constants,
  \li{a}~and~\li{b}, corresponding to the two bound variables of the same names.
  It is customary, although not mandatory, to name the constants after the bound
  variables. The tactic mimics how mathematicians work on paper: To prove a
  \li{∀}-quantified formula, it suffices to prove it for some arbitrary value of
  the bound variable. The goal becomes
  \[\hbox{\li{a b : Prop ⊢ a → b → a}}\]

\item Next, the \li{intros ha hb} tactic tells Lean to move the assumptions \li{a}
  and \li{b} to the context and to call these hypotheses \li{ha} and \li{hb}.
  Indeed, to prove an implication, we can take its left-hand side as
  hypothesis and try to prove its right-hand side. The goal becomes
  \[\hbox{\li{(a b : Prop) (ha : a) (hb : b) ⊢ a}}\]

\item
  The \li{apply ha} tactic tells Lean to match \li{ha : a} against the goal
  \li{a}. Since \li{a} is syntactically equal to \li{a}, this finishes the
  proof.
\end{enumerate}

We can save ourselves the \li{intros} invocations by declaring the constants and
hypotheses as parameters of the lemma, as follows:

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

\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{exact}, \li{assumption},
\li{refl}, \li{ac_refl}, and \li{use}.

These basic 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.

\subsection{intro(s)}

\begin{quote}
\li{intro} \,$\bigl[$\texttt{\itshape name}$\bigr]$ \\
\li{intros} \,$\bigl[$\texttt{\itshape name}$_\texttt{1}$ $\ldots$ \texttt{\itshape name}$_\texttt{\itshape n}\bigr]$
\end{quote}
%
(The symbols $\bigl[\,\bigr]$ encompass optional syntax, here and elsewhere.)
The \li{intro} tactic moves the leading \li{∀}-quantified variable or the
leading assumption \li{a →} from the conclusion 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 \li{intros} variant
can be used to move several variables or assumptions at once.

\subsection{apply}

\begin{quote}
\li{apply} \,\texttt{\itshape lemma}
\end{quote}
%
The \li{apply} tactic matches the goal's conclusion with the conclusion of the
specified lemma and adds the lemma's hypotheses as new goals.

\subsection{exact}

\begin{quote}
\li{exact} \,\texttt{\itshape lemma}
\end{quote}
%
The \li{exact} tactic matches the goal's conclusion with the specified lemma,
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 conclusion and applies it to solve the goal. In the example
from Section~\ref{sec:tactic-mode}, we could have used \li{assumption}
instead of \li{apply ha}.

\subsection{refl}

The \li{refl} tactic solves goals of the \li{l = r}, where the two sides are
equal \emph{up to computation}. We also say, equivalently, that the two terms
are \emph{definitionally equal}. Computation means unfolding of
definitions, reduction of an application of a \li{λ}-expression to an
argument, and more. These conversions have traditional names. The main
conversions are listed below together with examples, in a context with
\li|def double (n : ℕ) : ℕ := n + n|:

\kern\abovedisplayskip

\noindent
\begin{tabularx}{\textwidth}{@{}p{9em}X@{}}
$\alpha$-conversion & \li|(λx, f x) = (λy, f y)| \\
$\beta$-conversion & \li|(λx, f x) a = f a| \\
$\delta$-conversion & \li|double m = m + m| \\
$\zeta$-conversion & \li|(let n : ℕ := 2 in n + n) = 4| \\
$\eta$-conversion & \li|(λx, f x) = f| \\
$\iota$-conversion & \li|prod.fst (a, b) = a| \\
\end{tabularx}

\subsection{ac\_refl}

Proves \li{l = r}, where the two sides are equal up to associativity and
commutativity. This works for binary operations that are registered as
associative and commutative (e.g., \li{+} and \li{*} on arithmetic types).
We will see an example in Section~\ref{sec:proofs-about-natural-numbers}.

\subsection{use}

\begin{quote}
\li{use} \,\texttt{\itshape term}
\end{quote}
%
The \li{use} tactic allows us to supply a witness for an existential quantifier.
In the example below, where \li|def double (n : ℕ) : ℕ := n + n|, the witness is
\li{0}, and the proof goes through by computation once the witness has been
supplied:

\lstinputlisting[linerange=nat_exists_double_iden-q]{../lean/love02_tactical_proofs_demo_master.lean}

\section{Proofs about Logical Connectives and Quantifiers}
\label{sec:proofs-about-logical-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_tactical_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.

The proof is a typical combination \li{intro}, \li{apply}, and \li{exact}
tactics. The lemmas used are

\kern\abovedisplayskip

\noindent
\begin{tabularx}{\textwidth}{@{}p{9em}X@{}}
\li{and.intro} & \noindent\llap{\li|:|~}\li|?a → ?b → ?a ∧ ?b| \\
\li{and.elim_left} & \noindent\llap{\li|:|~}\li|?a ∧ ?b → ?a| \\
\li{and.elim_right} & \noindent\llap{\li|:|~}\li|?a ∧ ?b → ?b| \\
\end{tabularx}

\kern\belowdisplayskip

\noindent
where the question marks indicate variables that can be instantiated---for
example, by matching the goal's conclusion against one 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}.

The following is an alternative proof of the same lemma:

\lstinputlisting[linerange=and_swap₂-q]{../lean/love02_tactical_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 introduce (using \li{intro}) \li{a} and \li{b}
in addition to \li{a ∧ b}.

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 solve it. In our example,
the \li{apply and.intro} invocation creates two subgoals, \li{b} and \li{a}.

The third difference between the proofs is that we now apply \li{and.elim_right}
and \li{and.elim_left} directly to the hypothesis \li{a ∧ b} to obtain \li{b}
and \li{a}, respectively, instead of the combination of \li{apply} and
\li{exact} used in the first proof. Quantifier instantiation has the same
syntax---juxtaposition---as passing an argument to a function. This is not a
coincidence, as we will see in
Chapter~\ref{chap:structured-proofs-and-proof-terms}.

The introduction and elimination rules for disjunction (\li{∨}) are as
follows:

\kern\abovedisplayskip

\noindent
\begin{tabularx}{\textwidth}{@{}p{9em}X@{}}
\li{or.intro_left} & \noindent\llap{\li|:|~}$\forall$\li|b : Prop, ?a → ?a ∨ b| \\
\li{or.intro_right} & \noindent\llap{\li|:|~}$\forall$\li|b : Prop, ?a → b ∨ ?a| \\
\li{or.elim} & \noindent\llap{\li|:|~}\li|?a ∨ ?b → (?a → ?c) → (?b → ?c) → ?c| \\
\end{tabularx}

\kern\belowdisplayskip

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

The introduction and elimination rules for equivalence (\li{↔}) are as
follows:

\kern\abovedisplayskip

\noindent
\begin{tabularx}{\textwidth}{@{}p{9em}X@{}}
\li{iff.intro} & \noindent\llap{\li|:|~}\li|(?a → ?b) → (?b → ?a) → (?a ↔ ?b)| \\
\li{iff.elim_left} & \noindent\llap{\li|:|~}\li|(?a ↔ ?b) → ?a → ?b| \\
\li{iff.elim_right} & \noindent\llap{\li|:|~}\li|(?a ↔ ?b) → ?b → ?a| \\
\end{tabularx}

\kern\belowdisplayskip

The introduction and elimination rules for existential quantification (\li{∃})
are as follows:

\kern\abovedisplayskip

\noindent
\begin{tabularx}{\textwidth}{@{}p{9em}X@{}}
\li{exists.intro} & \noindent\llap{\li|:|~}$\forall$\li|w, (?p w → (∃x, ?p x))| \\
\li{exists.elim} & \noindent\llap{\li|:|~}\li|(∃x, ?p x) → (∀a, ?p a → ?c) → ?c| \\
\end{tabularx}

\kern\belowdisplayskip

\noindent
The introduction rule for \li{∃} is what the \li{use} tactic uses
internally. For example:

\lstinputlisting[linerange=nat_exists_double_iden₂-q]{../lean/love02_tactical_proofs_demo_master.lean}
%
The elimination rule for \li{∃} has a similar ``counterintuitive'' flavor to the
elimination rule for $\lor$.

For truth (\li{true}), there is only an introduction rule:

\kern\abovedisplayskip

\noindent
\begin{tabularx}{\textwidth}{@{}p{9em}X@{}}
\li{true.intro} & \noindent\llap{\li|:|~}\li|true| \\
\end{tabularx}

\kern\belowdisplayskip

For falsehood (\li{false}), there is only an elimination rule:

\kern\abovedisplayskip

\noindent
\begin{tabularx}{\textwidth}{@{}p{9em}X@{}}
\li{false.elim} & \noindent\llap{\li|:|~}\li|false → ?a| \\
\end{tabularx}

\kern\belowdisplayskip

Negation (\li{not}) is defined in terms of implication and falsehood: \li{¬ φ}
abbreviates \li{φ →} \li{false}. Lean's logic is classical, with support for the
law of excluded middle and proofs by contradiction:

\kern\abovedisplayskip

\noindent
\begin{tabularx}{\textwidth}{@{}p{9em}X@{}}
\li{classical.em} & \noindent\llap{\li|:|~}$\forall$\li|a : Prop, a ∨ ¬ a| \\
\multicolumn{2}{@{}l@{}}{\li{classical.by_contradiction}} \\
& \noindent\llap{\li|:|~}\li|(¬ ?a → false) → ?a| \\
\end{tabularx}

\kern\belowdisplayskip

Finally, implication (\li{→}) and universal quantification (\li{∀}) are the dogs
that did not bark. For both of them, \li{intro} is the introduction rule, and
application (juxtaposition) is the elimination rule. For example, if we have
\li{hab : a → b} and \li{ha : a}, then \li{hab ha : b} is a proof of~\li{b}.

For proving logic puzzles involving connectives and quantifiers, we advocate a
``mindless,'' ``video game'' style of reasoning that relies mostly 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 conclusion is an implication \li{φ → ψ}, invoke
  \li{intro hφ} to move \li{φ} into your hypotheses: \,\li{… (hφ : φ) ⊢ ψ}.

\item If the goal's conclusion is a universal quantification \li{∀x : σ, φ},
  invoke \li{intro} \li{x} to move it into the local context: \,\li{… (x : σ) ⊢ ψ}.

\item Otherwise, look for a hypothesis or a lemma whose conclusion has the
  same shape as the goal's conclusion (possibly containing variables that can
  be matched against the goal), and \li{apply} it. For example, if the goal's
  conclusion is \,\li{⊢ ψ} and you have a hypothesis \li{hφψ : φ → ψ}, try
  \li{apply hφψ}.

\item A negated goal \,\li{⊢ ¬ φ} is definitionally equal to \,\li{⊢ φ → false}, so
  you can invoke \li{intro hφ} to produce the subgoal \li{hφ : φ ⊢ false}.
  Expanding negation's definition by invoking \li{dunfold 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 false.elim}. As next step, you would typically \li{apply}
  a hypothesis of the form \li{φ → false} or \li{¬ φ}.

\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 have difficulties carrying out a proof, it can be a good idea to
  check whether the goal actually is provable under the given assumptions. Be
  also aware that even if you started with a provable lemma statement, it is
  possible that the goal is not provable (e.g., if you used ``unsafe'' rules
  such as \li{or.intro_left}).
\end{itemize}

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

The rewriting tactics replace equals for equals. By default, they apply to the
goal's conclusion, but they can also be applied to hypotheses specified using an
\li{at} clause:

\kern\abovedisplayskip

\noindent
\begin{tabularx}{\textwidth}{@{}p{9em}X@{}}
\li{at ⊢} & applies to the conclusion \\
\li{at h}$_\texttt{1}$ $\dots$ \li{h}$_\texttt{\itshape n}$ & applies to the specified hypotheses \\
\li{at *} & applies to all possible hypotheses and to the conclusion \\
\end{tabularx}

%\kern\belowdisplayskip

\subsection{rw}

\begin{quote}
\li{rw} \,\texttt{\itshape lemma}\, $\bigl[$\li{at} \,\texttt{\itshape position}$\bigr]$
\end{quote}
%
The \li{rw} tactic applies a single equation as a left-to-right rewrite rule,
once. To apply a lemma as a right-to-left rewrite rule, put a short left arrow
(\li{←}) in front of its name, or pass the lemma to \li{eq.symm}.

For example, given the lemma \li{l : b = a} and the goal \,\li{⊢ h a b b}, the
tactic invocation \li{rw l} produces the subgoal \,\li{⊢ h a a b}, whereas
\li{rw ←l} or \li{rw (eq.symm l)} produces the subgoal \,\li{⊢ h b b b}.

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

\subsection{simp}

\begin{quote}
\li{simp} \,$\bigl[$\li{at} \,\texttt{\itshape position}$\bigr]$
\end{quote}
%
The \li{simp} tactic applies 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. The \li{simp} tactic is more powerful than
\li{rw} because it can rewrite terms containing bound variables (e.g., bound by
\li{λ}, \li{∀}, or \li{∃}).

\begin{quote}
\li{simp} \,\li{[}\texttt{\itshape lemma}$_\texttt{1}$\li{,} $\dots$\li{,}
\texttt{\itshape lemma}$_\texttt{\itshape n}$\li{]}\,
$\bigl[$\li{at} \,\texttt{\itshape position}$\bigr]$
\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 local hypotheses. The minus sign (\li{-}) in front of a lemma name
temporarily removes the lemma from the simp set. To apply a lemma as a
right-to-left rewrite rule, prefix its name with a short left arrow (\li{←}).

For example, given the lemma \li{l : b = a} and the goal \,\li{⊢ h a b b}, the
tactic invocation \li{simp [l]} produces the subgoal \,\li{⊢ h a a a}, where
both occurrences of \li{b} have been replaced by \li{a}, whereas \li{simp [←l]}
produces the subgoal \,\li{⊢ h b b b}.

To find out exactly what \li{simp} does, you can enable tracing by
adding the command \li{set_option trace.simplify.rewrite true} to your Lean
file.

\subsection{dunfold}

\begin{quote}
\li{dunfold} \,\texttt{\itshape constant}$_\texttt{1}$ $\dots$
\texttt{\itshape constant}$_\texttt{\itshape n}$\,
$\bigl[$\li{at} \,\texttt{\itshape position}$\bigr]$
\end{quote}
%
The \li{dunfold} tactic expands the definition of one or more constants
that are specified without pattern matching (e.g., \li{not}).

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

\subsection{induction}

\begin{quote}
\li{induction} \,\texttt{\itshape variable}
\end{quote}
%
The \li{induction} tactic performs structural induction on the specified
variable. This gives rise to as many subgoals as there are constructors in the
definition of the variable's type. Induction hypotheses are available as
hypotheses in the subgoals corresponding to recursive constructors (e.g.,
\li{nat.succ} or \li{list.cons}).

\section{Proofs about Natural Numbers}
\label{sec:proofs-about-natural-numbers}

Equipped with a tactic for structural induction, we can now carry out
meaningful proofs about the addition and multiplication operations we defined
by structural 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 recursive equations on
the \emph{first} argument. We start with \li{add_zero}:

\lstinputlisting[linerange=add_zero-q]{../lean/love02_tactical_proofs_demo_master.lean}
%
The name \li{n_ih} is generated by the \li{induction} tactic. It refers to the
induction hypothesis for the induction on \li{n}. We can supply our own names,
and address the cases in an arbitrary order, by using the \li{case} keyword in
front of each case, together with the name of the case and the desired names for
the local constants and hypotheses introduced by the tactic. For example:

\lstinputlisting[linerange=add_zero₂-q]{../lean/love02_tactical_proofs_demo_master.lean}
%
Instead of \li{n} and \li{n_ih}, we choose the names \li{m} and \li{ih}.

We can write the proof more concisely if we want:

\lstinputlisting[linerange=add_zero₃-q]{../lean/love02_tactical_proofs_demo_master.lean}
%
The syntax \texttt{by} \texttt{\itshape tactic} abbreviates
\texttt{begin} \texttt{\itshape tactic} \texttt{end}. It can be used when a
single (possibly complex) tactic suffices to solve the goal.

The semicolon (\li{;}) is a tactic combinator. The complex tactic
\texttt{\itshape tactic}$_\texttt{1}$ \li{;} \texttt{\itshape tactic}$_\texttt{2}$
first applies \texttt{\itshape tactic}$_\texttt{1}$ and then applies
\texttt{\itshape tactic}$_\texttt{2}$ to all subgoals emerging from
\texttt{\itshape tactic}$_\texttt{1}$. Our example works because
\li{simp [add, *]} solves not only the induction step but also the base case
(for which \li{refl} would have sufficed).

We can keep on proving lemmas by structural induction:

\lstinputlisting[linerange=add_succ-q]{../lean/love02_tactical_proofs_demo_master.lean}
\betweenlistings
\lstinputlisting[linerange=add_comm-q]{../lean/love02_tactical_proofs_demo_master.lean}
\betweenlistings
\lstinputlisting[linerange=add_assoc-q]{../lean/love02_tactical_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{ac_refl}) know about
this. Here is the syntax to achieve this for \li{add}:

\lstinputlisting[linerange=is_commutative_associative-q]{../lean/love02_tactical_proofs_demo_master.lean}

Here is an example that uses \li{ac_refl} to reason up to associativity and
commutatitivy of \li{add}:

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

\section{Goal Management Tactics}
\label{sec:goal-management-tactics}

The following tactics help manage the goal, by allowing us to give more
meaningful names to local constants or hypotheses, remove useless hypotheses,
or undo the effect of an \li{intro} invocation.

\subsection{rename}

\begin{quote}
\li{rename} \,\texttt{\itshape constant-or-hypothesis}\, \texttt{\itshape new-name}
\end{quote}
%
The \li{rename} tactic renames a local constant or hypothesis.

\subsection{clear}

\begin{quote}
\li{clear} \,\texttt{\itshape constant-or-hypothesis}$_\texttt{1}$ $\dots$
\texttt{\itshape constant-or-hypothesis}$_\texttt{\itshape n}$
\end{quote}
%
The \li{clear} tactic removes the specified local constants and hypotheses, as long as they
are not used anywhere else in the goal.

\subsection{revert}

\begin{quote}
\li{revert} \,\texttt{\itshape constant-or-hypothesis}$_\texttt{1}$ $\dots$
\texttt{\itshape constant-or-hypothesis}$_\texttt{\itshape n}$
\end{quote}
%
The \li{revert} tactic performs the opposite of \li{intros}: Moves the specified local
constants and hypotheses into the goal's conclusion using universal quantification (\li{∀})
for constants and implication (\li{→}) for hypotheses.

For example, if the goal is \li{a : Prop, ha : a ⊢ b}, the tactic invocation
\li{revert a ha} produces the subgoal \,\li{⊢ ∀a : Prop, a → b}.

\section{Summary of New Syntax}

\small

\subsection{Commands}

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

\subsection{Proof Commands}

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

\subsection{Tactic Combinators}

\noindent
\begin{tabularx}{\textwidth}{@{}p{9em}X@{}}
\li|;| & applies the second tactic to all subgoals yielded by the first tactic \\
\texttt{\{} \ldots{} \texttt{\}} & focuses on the first subgoal; needs to solve that goal \\
\end{tabularx}

\subsection{Tactics}

\noindent
\begin{tabularx}{\textwidth}{@{}p{9em}X@{}}
\li|ac_refl| & proves \li|l = r| if \li|l| equals \li|r| up to associativity and commutativity \\
\li|apply| & matches the goal's conclusion with the lemma's conclusion \\
\li|assumption| & solves the goal using a local hypothesis \\
\li|clear| & removes a local constant or hypothesis from the goal \\
\li|dunfold| & unfolds a definition without pattern matching (e.g., \li{not}) \\
\li|exact| & solves the goal by the specified term \\
\li|induction| & performs structural induction on a variable of an inductive type \\
\li|intro|(\li|s|) & moves $\forall$-quantified variables into the goal's hypotheses \\
\li|refl| & proves \li|l = r| where \li|l| and \li|r| are equal up to computation \\
\li|rename| & renames a local constant or hypothesis \\
\end{tabularx}

\noindent
\begin{tabularx}{\textwidth}{@{}p{9em}X@{}}
\li|revert| & undoes the effect of \li{intro} \\
\li|rw| & applies the given rewrite rules once, in sequence \\
\li|simp| & applies a set of preregistered rewrite rules exhaustively \\
\li|use| & provides a witness to an existential quantifier \\
\end{tabularx}
