\chapter{Metaprogramming}
\label{chap:metaprogramming}

Like most proof assistants, Lean can be extended with custom tactics and other
functionality. Programming Lean itself, as opposed to merely using it, is called
metaprogramming. Lean's metaprogramming framework mostly uses the same notions
and syntax as Lean's input language, so that we do not need to learn a different
language to program Lean. Monads are used to access Lean's state.

Abstract syntax trees, presented as inductive types, reflect internal data
structures. The proof assistant's internals are exposed through Lean functions,
which we can use to access the current goal, unify terms, query and modify the
global context, and set attributes (e.g., \li{@[simp]}).

Here are some example applications of metaprogramming:

\begin{itemize}
\item goal transformations (e.g., applying safe introduction rules, putting the
  goal in negation normal form);

\item heuristic proof search (e.g., applying unsafe introduction rules with
  backtracking);

\item decision procedures (e.g., for linear arithmetic, propositional logic);

\item definition generators (e.g., Haskell-style \li{deriving} for inductive
  types);

\item advisor tools (e.g., theorem finders, counterexample generators);

\item exporters (e.g., documentation generators);

\item ad hoc proof automation (to avoid boilerplate or duplication).
\end{itemize}
%
%But there is also trouble in Eden.%
%\footnote{https://jiggerwit.wordpress.com/2018/09/18/a-review-of-the-lean-theorem-prover/}
%
As mathematician and Lean user Kevin Buzzard wrote:%
\footnote{\url{https://xenaproject.wordpress.com/2020/02/09/lean-is-better-for-proper-maths-than-all-the-other-theorem-provers/}}
%
\begin{quote}
%Note that
If you find yourself ``grinding'' (to use a computer game phrase),
doing the same sort of stuff over and over again because you need to do it to
make progress, then you can try to persuade a computer scientist to write a
tactic to do it for you (or even write your own tactic if you're brave enough
to write \li{meta} Lean code).
\end{quote}

\section{Tactic Combinators}
\label{sec:tactic-combinators}

First, some terminology: A tactic \emph{fails} if applying it produces an error;
otherwise, it \emph{succeeds}. One way for a tactic to succeed is to fully prove
the goal. Another is to produce new subgoals that replace the current goal. Some
tactics succeed by doing nothing.

When programming our own tactics, we often need to repeat some actions on
several goals, or to recover if a tactic fails. Tactic combinators help in such
cases.
One of the most useful tactic combinators is \li|repeat'| \ttvar{tactic}. It
invokes \ttvar{tactic} repeatedly on all goals, then on the emerging subgoals,
then on the emerging subsubgoals, and so on until \ttvar{tactic} fails on all
the available goals. Here is an example of \li{repeat'} involving the
\li{Even} predicate presented in Chapter~\ref{chap:inductive-predicates}:

\lstinputlisting[linerange=repeat'_example-q]{../lean/LoVe/LoVe08_Metaprogramming_DemoMaster.lean}
%
After the first \li{repeat'} line, the proof state consists of four goals:
%
\begin{align*}
  & \text{\lic|\⊢ Even 4|}
& & \text{\lic|\⊢ Even 7|}
& & \text{\lic|\⊢ Even 3|}
& & \text{\lic|\⊢ Even 0|}
\end{align*}
%
Notice that all conjunctions are gone. The second \li{repeat'},
which applies the theorem \li{Even.add_two : ∀k, Even k → Even (k + 2)} over and
over, leaves us with these goals:
%
\begin{align*}
  & \text{\lic|\⊢ Even 0|}
& & \text{\lic|\⊢ Even 1|}
& & \text{\lic|\⊢ Even 1|}
& & \text{\lic|\⊢ Even 0|}
\end{align*}

The first and last goals are annoying because they correspond to the theorem
\li{Even.}\allowbreak\li{zero}. We can prove them by trying to apply
\li{Even.zero} whenever applying \li{Even.add_two} fails. This is achieved as
follows:
%
\lstinputlisting[linerange=repeat'_first_example-q]{../lean/LoVe/LoVe08_Metaprogramming_DemoMaster.lean}
%
The tactic combinator
\li$first |$ \ttvar{tactic}$_\texttt{1}$ \li$| ⋯ |$ \ttvar{tactic}$_\ttvar{n}$
first tries to execute its first argument, \ttvar{tactic}$_\texttt{1}$. If this
fails, \ttvar{tactic}$_\texttt{2}$ is tried, and so on. If all the specified
tactics fail, the entire combinator fails. In the example above, we have two
unprovable goals left:
%
\begin{align*}
  & \text{\lic|\⊢ Even 1|}
& & \text{\lic|\⊢ Even 1|}
\end{align*}

The next combinator, \li{all_goals} \ttvar{tactic}, invokes a tactic exactly
once on each goal. The combinator succeeds only if \ttvar{tactic} succeeds on
\emph{all} goals. It fails in the example below, because
\hbox{\li{Even.}}\allowbreak\li{add_two} cannot be applied to the goal \li{⊢ Even 0}:
%
\lstinputlisting[linerange=all_goals_example-q]{../lean/LoVe/LoVe08_Metaprogramming_DemoMaster.lean}
%
To ignore failures of \ttvar{tactic}, we can wrap it in the \li{try} combinator:
%
\lstinputlisting[linerange=all_goals_try_example-q]{../lean/LoVe/LoVe08_Metaprogramming_DemoMaster.lean}
%
The resulting state is
%
\begin{align*}
  & \text{\lic|\⊢ Even 2|}
& & \text{\lic|\⊢ Even 5|}
& & \text{\lic|\⊢ Even 1|}
& & \text{\lic|\⊢ Even 0|}
\end{align*}
%
The construct \li|try |\ttvar{tactic} is equivalent to
\li$first |$ \ttvar{tactic}\li$ | skip$, where \li{skip} is a tactic that
succeeds without doing anything. Hence \li{try} \ttvar{tactic} always succeeds.
A related tactic is \li{done}: It succeeds if there are no goals left and fails
otherwise.

Another variant is the \li{any_goals} \ttvar{tactic} combinator. It tries to
invoke \ttvar{tactic} once on each goal, but unlike \li{all_goals}, it succeeds
if \ttvar{tactic} succeeds on \emph{any} goal. The example
%
\lstinputlisting[linerange=any_goals_example-q]{../lean/LoVe/LoVe08_Metaprogramming_DemoMaster.lean}
%
results in the state
%
\begin{align*}
  & \text{\lic|\⊢ Even 2|}
& & \text{\lic|\⊢ Even 5|}
& & \text{\lic|\⊢ Even 1|}
& & \text{\lic|\⊢ Even 0|}
\end{align*}
%
This is the same state as in the previous example. In general, the difference is
that \li{any_goals} \ttvar{tactic} can fail whereas
\li$all_goals try$ \ttvar{tactic} always succeeds.

Sometimes we want to leave a goal alone unless we can fully prove it. The
combinator \li$solve |$ \ttvar{tactic}$_\texttt{1}$ \li$| ⋯ |$ \ttvar{tactic}$_\ttvar{n}$
first tries to execute its first argument, \ttvar{tactic}$_\texttt{1}$. If this
fails to prove the goal, \ttvar{tactic}$_\texttt{2}$ is tried, and so on. If all
the specified tactics fail to prove the goal, the entire combinator fails.
(Compare this behavior with that of
\li$first |$ \ttvar{tactic}$_\texttt{1}$ \li$| ⋯ |$ \ttvar{tactic}$_\ttvar{n}$,
which only requires one of the specified tactics to succeed, not to prove the
goal.) Consider this example:
%
\lstinputlisting[linerange=any_goals_solve_repeat_first_example-q]{../lean/LoVe/LoVe08_Metaprogramming_DemoMaster.lean}
%
The first and fourth goals are proved, and we are left with the two unprovable
goals exactly as they stand in the theorem statement:
%
\begin{align*}
  & \text{\lic|\⊢ Even 7|}
& & \text{\lic|\⊢ Even 3|}
\end{align*}

Note that the \li{repeat'} combinator can lead to infinite looping. Consider
this example:
%
\lstinputlisting[linerange=repeat'_not_example-q]{../lean/LoVe/LoVe08_Metaprogramming_DemoMaster.lean}
%
The \li{Not.intro} rule is \li{(?a → False) → ¬ ?a}, so it applies once to
transform the goal into \li{⊢ Even 1 → False}. Because \li{¬ ?a} is defined as
\li{?a → False}, the rule applies again, yielding the same goal again. The
tactic loops.

Finally, the ``and then'' operator \li{<;>} can be used to
join two tactics. The left-hand side is executed on the first goal. The
right-hand side is executed on every emerging subgoal (but not on the original
second goal, third goal, etc.). Thus, we can write
%
\begin{center}
\begin{tabular}{@{}l@{}}
\licw$by$ \\
\licw$  induction n <;>$ \\
\licw$    aesop$ \\
\end{tabular}
\end{center}
%
instead of the more verbose
%
\begin{center}
\begin{tabular}{@{}l@{}}
\licw$by$ \\
\licw$  induction n with$ \\
\licw$  | zero       => aesop$ \\
\licw$  | succ n' ih => aesop$ \\
\end{tabular}
\end{center}

\section{Macros}
\label{sec:macros}

Let us do some actual metaprogramming, by coding a custom tactic
as a macro. The tactic embodies the behavior we hardcoded in the \li{solve}
example above:
%
\lstinputlisting[linerange=intro_and_even-q]{../lean/LoVe/LoVe08_Metaprogramming_DemoMaster.lean}

The first line declares \li{intro_and_even} as a macro belonging to the \hbox{\li|tactic|}
syntactic category. On the remaining lines, the \li$`(tactic| $
\ttvar{tactic}\li$)$ construct embeds the specified tactic, \ttvar{tactic}, in a
macro. The tactic itself is specified using standard syntax.

Once we have defined a custom tactic, we can invoke it in a proof:
%
\lstinputlisting[linerange=intro_and_even_example-q]{../lean/LoVe/LoVe08_Metaprogramming_DemoMaster.lean}
%
This yields the subgoals
%
\begin{align*}
  & \text{\lic|\⊢ Even 7|}
& & \text{\lic|\⊢ Even 3|}
\end{align*}

\section{The Metaprogramming Monads}
\label{sec:the-metaprogramming-monads}

Macros are a mechanism that can be used to program simple proof
automation. For most metaprogramming tasks, however, we need to use the
metaprogramming monads, \li{MetaM} and \li{TacticM}.

\li{MetaM} combines the attributes of several kinds of monads:
%
\begin{itemize}
\item It is a state monad providing access to
  the global context (including all definitions and inductive types),
  notations, and attributes (e.g., the list of \li{@[simp]} theorems),
  among others.

\item It behaves like an option monad. The metaprogram
  \li{failure} signals that a tactic has failed.

\item It supports tracing, so we can use the program \li{logInfo} to display
  messages.

\item It supports imperative constructs such as \li{for}--\li{in} loops,
  \li{continue} statements, and \li{return} statements.
\end{itemize}

\li{TacticM} extends \li{MetaM} with goal management: It provides access to the
list of goals. It also allows us to run Lean to fill in the implicit \li|{ }|
and type class \li|[ ]| arguments in expressions, to expand macros, and more.

Inside Lean, each goal is represented as a metavariable \li{?m} standing for a
missing term (typically, a proof term). Each metavariable has a type (typically,
a proposition) and a local context specifying the variables and hypotheses that
can be used to prove the goal associated with the metavariable.

Let us put \li{TacticM} to some use by defining a tactic that uses
\li{TacticM}'s tracing facilities to display the Lean version number, the list
of goals, and the target of the first goal (which Lean calls the \emph{main}
goal):

\lstinputlisting[linerange=traceGoal-q]{../lean/LoVe/LoVe08_Metaprogramming_DemoMaster.lean}

The code has many interesting features:
%
\begin{itemize}
\item The first line declares a function \li{traceGoals} of
  type \hbox{\li{TacticM}} \li{Unit}---the type of tactics that return
  \li{Unit} (a trivial type of cardinality one). Notice that a metaprogramming
  function is defined using the same syntax as any Lean function.

\item The second line enters the monad. The remaining lines are effectful
  operations that access Lean's internals.

\item The \li|m!"…"| syntax specifies a string in which every occurrence of
  %%% typesetting \!\!
  \hbox{\li|{|\!\!\ttvar{term}\li|}|,} where \ttvar{term} is a Lean term, is
  evaluated and serialized into a string. For example, if
  \hbox{\li{Lean.versionString}} is ``\leanversion'', then
  \li|m!|\allowbreak\hbox{\li|"Lean|} \li|version| \li|{Lean.|\allowbreak\li|versionString}"|
  evaluates to the string ``Lean version \leanversion''.

\item The last two lines register a new tactic called \li{trace_goal} that
  simply calls the \li{traceGoals} function.
\end{itemize}

Here is an example of how we can use the new tactic:
%
\lstinputlisting[linerange=Even_18_and_Even_20-q]{../lean/LoVe/LoVe08_Metaprogramming_DemoMaster.lean}
%
The output, which is made visible by hovering over \li{trace_goals}, is as follows:
\begin{quote}
\texttt{Lean version \leanversion} \\
\li|All goals:| \\
\li|[case left| \\
\li|α : Type| \\
\li|a : α| \\
\li|⊢ Even 18,| \\
\phantom{\li|x|}\li|case right| \\
\li|α : Type| \\
\li|a : α| \\
\li|⊢ Even 20]| \\
\li|First goal's target:| \\
\li|Even 18|
\end{quote}
%
Although Lean displays goals using the familiar goal syntax \li{C ⊢ P},
they are actually metavariables.

The constants used in the above program have the following types:
%
\begin{center}
\begin{tabular}{@{}r@{}l@{}}
\lic|logInfo| & \lic| : MessageData → TacticM Unit| \\
\lic|getUnsolvedGoals| & \lic| : TacticM (List MVarId)| \\
\lic|getMainTarget| & \lic| : TacticM Expr| \\
\end{tabular}
\end{center}
%
where \li{MessageData} represents a message,
\li{MVarId} represents a metavariable identifier, and \li{Expr} represents
a term.

\section{First Example: An Assumption Tactic}
\label{sec:first-example-an-assumption-tactic}

Our first larger example implements a \hbox{\li{hypothesis}} tactic
that, like the predefined \li{assumption} tactic, looks for a hypothesis of the
right type (i.e., the right proposition) and applies it to prove the goal:

\lstinputlisting[linerange=hypothesis-q,keywords={def,do,let,for,in,if,then,return,elab}]{../lean/LoVe/LoVe08_Metaprogramming_DemoMaster.lean}

In the \li{hypothesis} function, we start by extracting the first goal's target and the
local context. To make sure that \li{getLCtx} gives us the local context of the
current first goal, we pass the entire \li{do} block to the \li{withMainContext}
function. In general, any \hbox{\li{TacticM}} computation is performed within an
ambient local context that gives meaning to the free variables occurring in
expressions. The \li{withMainContext} function sets this local context to the
local context of the current first goal.

Inside the \li{do} block, we iterate over all declarations in the local
context, using the convenient monadic construct \li|for|--\li|in|.
%
For each local variable or hypothesis \li|h| that is not a so-called
implementation detail (i.e., a hypothesis inserted by Lean that is invisible to
users), we check if its type (typically, its proposition) is equal to the target
up to computation and instantiation of metavariables, and if so, we get the
metavariable \li|?m| associated with the first goal and assign \li|?m := h|,
thereby proving the goal. Finally, we \li|return|.

Since goals are represented by metavariables, assigning a term to a
metavariable \hbox{\li|?m|} is Lean's low-level way of proving a goal.
New metavariables occurring in that term correspond to new subgoals that must be
proved.

A simple invocation of \li{hypothesis} follows:

\lstinputlisting[linerange=hypothesis_example-q]{../lean/LoVe/LoVe08_Metaprogramming_DemoMaster.lean}
%
If we add tracing, we can see that \li{α}, \li{p}, and \li{a} are tried in turn
before the matching hypothesis \li{hpa} is found and successfully applied.

The example used the following new constants:
%
\begin{center}
\begin{tabular}{@{}r@{}l@{}}
\lic|getLCtx| & \lic| : TacticM LocalContext| \\
\lic|LocalDecl.isImplementationDetail| & \lic| : LocalDecl → Bool| \\
\lic|isDefEq| & \lic| : Expr → Expr → TacticM Bool| \\
\lic|LocalDecl.type| & \lic| : LocalDecl → Expr| \\
\lic|getMainGoal| & \lic| : TacticM MVarId| \\
\lic|MVarId.assign| & \lic| : MVarId → Expr → TacticM Unit| \\
\lic|LocalDecl.toExpr| & \lic| : LocalDecl → Expr| \\
\lic|failure {α : Type}| & \lic| : TacticM α| \\
\end{tabular}
\end{center}

\section{Expressions}
\label{sec:expressions}

The metaprogramming framework revolves around the type \li{Expr} of expressions
or terms. An important component of expressions are names, of type \li{Name}.
We begin with them.

Names can be specified using a single backtick. For example, \li|`x| represents
the name \li|x|, which can be given to a variable or constant. When referring to
constants, we must specify the full name, including namespaces; thus, to refer
to the \li|Even| predicate of Chapter~\ref{chap:inductive-predicates}, we must
write \li|`LoVe.Even| and not \li|`Even|.

If we want to refer to an existing constant, Lean offers the double-backtick
syntax, which looks up the name using Lean's usual name elaboration rules and
expands it to its full name. Thus, both \li|``Even| and \li|``LoVe.Even| refer
to the name \li|LoVe.Even|, and if we write some name that is not declared, such
as \hbox{\li|``EvenIf|,} Lean gives an error.

The type \li{Expr} is defined as follows:
%
\begin{lstlisting}
inductive Expr : Type where
  | const   : Name → List Level → Expr
  | sort    : Level → Expr
  | fvar    : FVarId → Expr
  | mvar    : MVarId → Expr
  | app     : Expr → Expr → Expr
  | lam     : Name → Expr → Expr → BinderInfo → Expr
  | bvar    : Nat → Expr
  | forallE : Name → Expr → Expr → BinderInfo → Expr
  | letE    : Name → Expr → Expr → Expr → Bool → Expr
  | lit     : Literal → Expr
  | mdata   : MData → Expr → Expr
  | proj    : Name → Nat → Expr → Expr
\end{lstlisting}

Let us review the main constructors:

\begin{sloppy}
\begin{itemize}
\item \li{Expr.const name levels} represents a constant called \li{name}, such as
  \li{Nat.}\allowbreak\li{add} or \hbox{\li{ℕ}.} The \li{levels} argument
  represents universe levels, a concept that will be explained in
  Chapter~\ref{chap:logical-foundations-of-mathematics}. For example,
  \li|Expr.const ``Nat.add []| represents \li{Nat.add} and
  \li|Expr.const ``Nat []| represents \li{Nat} (i.e., \li{ℕ}).

\item \li{Expr.sort level} is used to represent the types of types. For example,
  \li{Expr.}\allowbreak\li{sort} \hbox{\li{Level.zero}} stands for \li{Prop}, and
  \li{Expr.sort (Level.succ Level.}\allowbreak\li{zero)} stands for \li{Type}.

\item \li{Expr.fvar id} represents a free variable in the local context (e.g.,
  \li{a}, \li{h}). The \li{id} argument is a unique identifier for the variable.

\item \li{Expr.mvar id} represents a metavariable, i.e., a variable \li{?m} with a
  question mark. The \li{id} argument is a unique identifier for the
  metavariable.

\item \li{Expr.app t u} represents the application of a function \hbox{\li{t}}
  to an argument \li{u}. For example,
  \hbox{\li|Expr.app (Expr.const ``Nat.succ|} \li|[] (Expr.const| \li|``Nat.zero| \li|[])|
  represents \li{Nat.succ Nat.zero}.

\item \li{Expr.lam name σ t bi} represents an anonymous function
  (or $\lambda$-expression).
  The \li{name} argument is the bound variable's name, the \li{σ} argument is
  the bound variable's type, the \li{t} argument is the function's body, and the
  \li{bi} argument stores whether the variable is an explicit \li{( )}, implicit
  \li${ }$, or type class \li{[ ]} argument.

\item \li{Expr.bvar i} represents a bound variable, using a
  notation known as De Bruijn index. \li{Expr.var 0} refers to
  the variable bound by the closest binder, \li{Expr.var 1} refers to the
  variable bound by the second closest binder, and so on.
%
  Thus,
%
  \[\begin{aligned}[t]
    & \text{\li|Expr.lam `x (Expr.const ``Nat []) (Expr.bvar 0)|} \\[-\jot]
    & \text{\texttt{~~}\li|BinderInfo.default|}
    \end{aligned}\]
  represents \li|fun x : ℕ ↦ x|, and
%
  \[\begin{aligned}[t]
    & \text{\li|Expr.lam `x (Expr.const ``Nat [])|} \\[-\jot]
    & \text{\texttt{~~}\li|(Expr.lam `y (Expr.const ``Nat []) (Expr.bvar 1)|} \\[-\jot]
    & \text{\texttt{~~~~~}\li|BinderInfo.default)|} \\[-\jot]
    & \text{\texttt{~~}\li|BinderInfo.default|}
    \end{aligned}\]
%
  represents \li|fun x y : ℕ ↦ x|.

\item \li{Expr.forallE name σ τ bi} represents a possibly dependent function type.
  The \li{name} argument is the name of the bound variable, the \li{σ} argument
  is the domain type, the \li{τ} argument is the result type, and
  \li{bi} is as for \li{Expr.lam} above. For example,
%
  \[\begin{aligned}[t]
    & \text{\li|Expr.forallE `n (Expr.const ``Nat [])|} \\[-\jot]
    & \text{\texttt{~~}\li|(Expr.app (Expr.const ``Even []) (Expr.bvar 0))|} \\[-\jot]
    & \text{\texttt{~~}\li|BinderInfo.default|}
    \end{aligned}\]
%
  represents \li|(n : ℕ) → Even n| (also written \li|∀n : ℕ, Even n|), and
%
  \[\begin{aligned}[t]
    & \text{\li|Expr.forallE `dummy (Expr.const `Nat [])|} \\[-\jot]
    & \text{\texttt{~~}\li|(Expr.const `Bool []) BinderInfo.default|}
    \end{aligned}\]
%
  represents \li|ℕ → Bool|.
\end{itemize}
\end{sloppy}

%\begin{sloppypar}
%To each constructor corresponds a discriminator of type \hbox{\li{Expr →}}
%\hbox{\li{Bool}.} For example, \li{Expr.isApp e} returns \li{true} if \li{e} is
%of the form \li{Expr.app …}\,; otherwise, it returns \li{false}.
%For the main constructors, the functions are called
%\hbox{\li{Expr.}}\allowbreak\hbox{\li{isConst},}
%\li{Expr.isSort},
%\li{Expr.isFVar},
%\li{Expr.isMVar},
%\li{Expr.isApp},
%\li{Expr.isLambda},
%\li{Expr.isBVar}, and
%\li{Expr.isForall}.
%It is also possible to pattern-match on \li{Expr} values.
%\end{sloppypar}

\section{Second Example: A Conjunction-Destructing Tactic}
\label{sec:second-example-a-conjunction-destructing-tactic}

In this and the next section, we define two further tactics that accomplish
well-defined tasks. The first of these two tactics, called \li{destruct_and},
automates the elimination of conjunctions in premises. Our aim is to automate
proofs such as the following:

\lstinputlisting[linerange=example_1_2_3-q]{../lean/LoVe/LoVe08_Metaprogramming_DemoMaster.lean}
%
In each case, we would like to simply write \li{by destruct_and h} as the proof.

Our tactic relies on a helper function, which takes as argument a proof term
\li{hP} (initially the hypothesis \li{h}) from which we extract conjuncts:

\lstinputlisting[linerange=destructAndExpr-q]{../lean/LoVe/LoVe08_Metaprogramming_DemoMaster.lean}

As with \li{hypothesis}, we pass the entire \li{do} block to the
\hbox{\li{with}}\-\li{MainContext} function. This ensures that \li{inferType}
and \li{isDefEq} operate within the right local context.
%
Inside the \li{do} block, we first extract the first goal's target and \li{hP}'s
type (typically, its proposition) \li{P}. If they are equal up to computation
and instantiation of metavariables, we close the goal by assigning to its
metavariable, as we did in the \li{hypothesis} example, and we return \li{true}
to indicate success. Otherwise, we check whether \li{hP}'s proposition is of the
form \hbox{\li{Q ∧ R}.} If so, we call the helper function recursively with the proof
term \li{hQ := And.left hP}, which is a proof of \li{Q}. If this succeeds, we
are done; otherwise, we try the proof term \hbox{\li{hR := And.right}} \li{hP}, which is a
proof of \li{R}.

Note the presence of the keyword \li{partial} at the beginning of the function
definition. It is needed here because Lean fails to prove that the function
always terminates. Since the function will be used only as a metaprogram, and
not inside a proposition, termination is optional, and we can disable the
termination check by specifying \li{partial}.

Also noteworthy is the \li{mkAppM} function, which is used to construct a
curried application of a constant to an array of arguments. Arrays are similar
to lists but are written prefixed with the symbol \li|#| (e.g., \li|#[1, 2, 3]|). Using
\li{mkAppM} is more convenient than applying the \li{Expr.app} constructor
multiple times. Additionally, \li{mkAppM} allows us to omit implicit arguments
such as the propositions \li{Q} and \li{R}, which we would otherwise have to
provide as arguments to \hbox{\li{And.left}} and \li{And.right}.

The main function has very little left to do:

\lstinputlisting[linerange=destructAnd_main-q]{../lean/LoVe/LoVe08_Metaprogramming_DemoMaster.lean}
%
The function retrieves the hypothesis \li{h} using \hbox{\li{getFVarFromUserName}} and
calls the helper function. If the helper returns \li{false}, the tactic fails.

We can now use our new gadget on the motivating examples:

\lstinputlisting[linerange=example_4_5_6-q]{../lean/LoVe/LoVe08_Metaprogramming_DemoMaster.lean}

The following new constants were used in the above metaprogram:
%
\begin{center}
\begin{tabular}{@{}r@{}l@{}}
\lic|inferType| & \lic| : Expr → TacticM Expr| \\
\lic|Expr.and?| & \lic| : Expr → Option (Expr × Expr)| \\
\lic|mkAppM| & \lic| : Name → Array Expr → TacticM Expr| \\
\lic|getFVarFromUserName| & \lic| : Name → TacticM Expr|
\end{tabular}
\end{center}

\section{Third Example: A Direct Proof Finder}
\label{sec:third-example-a-direct-proof-finder}

Sometimes we state a theorem, prove it, and later realize that the theorem already
existed. This can be prevented by using
\hbox{\li{prove_}}\allowbreak\hbox{\li{direct},} a tactic that traverses all
available theorems and checks whether one of them can prove the current goal. We
will review its code in steps.

The first step is a
function \li{isTheorem} that returns \li{true} if a declaration is an axiom or
a theorem and \li{false} otherwise:

\lstinputlisting[linerange=isTheorem-q]{../lean/LoVe/LoVe08_Metaprogramming_DemoMaster.lean}
%
We will use this function to filter out the declarations that do not
interest us.

The next function applies the theorem called \li{name} to the current goal:

\lstinputlisting[linerange=applyConstant-q]{../lean/LoVe/LoVe08_Metaprogramming_DemoMaster.lean}
%
Given a name, the \li{mkConstWithFreshMVarLevels} function creates an
expression \li{cst} representing the constant.
The allusion to ``fresh metavariable levels'' in the function's
name will become clearer in Chapter~\ref{chap:logical-foundations-of-mathematics}.
\li{MVarId.apply} (not to be confused with \li{MVarId.assign}) then applies the
constant to the current goal, setting \li{?m} := \li{cst ?m}$_\texttt{1}$
\ldots{} \li{?m}$_\ttvar{n}$ and
returning the fresh metavariables \li{?m}$_\ttvar{j}$, which represent the
premises of \li{cst}.

The \li{liftMetaTactic} function retrieves the identifier of the first goal,
runs the given function on the goal within the lower-level \li{MetaM} monad, and
replaces the goal with the subgoals returned by the function.

The next function implements a combinator that behaves like \li{<;>} but that
can be used from a metaprogram:

\lstinputlisting[linerange=andThenOnSubgoals-q]{../lean/LoVe/LoVe08_Metaprogramming_DemoMaster.lean}

The \li{TacticM} monad keeps track of the current goals to prove. We can
retrieve the list using \li{getGoals} and set it using \li{setGoals}. Setting
the list of subgoals is useful if we want the tactic to temporarily focus on
specific subgoals.

Here, we first focus on the first goal (\li{setGoals [mainGoal]}) and invoke the
first tactic. For each subgoal that emerges, we focus on it
(\li{setGoals [subgoal]}) and invoke the second tactic. All the unsolved
subsubgoals emerging from the second tactic are collected in the mutable
variable \li{newGoals}. Since proving a goal can sometimes instantiate another
metavariable, we check at each iteration whether the current subgoal
metavariable is assigned and skip the subgoal if it is. At the end, we update
the goals to include all the pending goals:\ those in \li{newGoals} and all but
the first goal of \li{origGoals}, which we have not considered.

In general, at the end of a tactic, we should make sure that the list
of goals consists of all goals that remain to be proved. Otherwise, we may get
cryptic~errors such as
%
\begin{quote}
\tabletsmall\ttfamily\raggedright
declaration has metavariables
\end{quote}

We also need a tactic that attempts to prove the goal using a
theorem specified by its name and that invokes \li{hypothesis} to prove any
emerging subgoals:

\lstinputlisting[linerange=proveUsingTheorem-q,keywords={def}]{../lean/LoVe/LoVe08_Metaprogramming_DemoMaster.lean}
%
This is the programmatic equivalent of the proof \li{apply} \ttvar{name}
\li{<;> hypothesis}.

Finally, we are ready to review the main function:

\lstinputlisting[linerange=proveDirect-q]{../lean/LoVe/LoVe08_Metaprogramming_DemoMaster.lean}
%
We focus on the first goal, then iterate over all constants declared in the environment.
If the constant is a theorem and is not ``unsafe'' (a Lean concept unrelated to
our notion of unsafe rules and tactics), we try to apply it
using our helper \hbox{\li{proveUsingTheorem}.} If this succeeds, we
print ``Proved directly by \ttvar{name},'' where \ttvar{name} is the name of
the theorem, and return. On failure, we keep
iterating. If the entire iteration is exhausted, we report a failure.

Here is the tactic in action:
%
\lstinputlisting[linerange=Nat.eq_symm-q]{../lean/LoVe/LoVe08_Metaprogramming_DemoMaster.lean}
%
This prints ``Proved directly by {symm}.''
The message is helpful because we can apply the specified theorem directly
instead of relying on the relatively slow \li{prove_}\allowbreak\li{direct} tactic.
Specifically, we can apply the theorem \li{symm} in conjunction with
\li{hypothesis} as follows:
%
\lstinputlisting[linerange=Nat.eq_symm_manual_proof-q]{../lean/LoVe/LoVe08_Metaprogramming_DemoMaster.lean}

Here is a list of new constants featured in this example:
%
\begin{center}
\tabletsmall
\begin{tabular}{@{}r@{}l@{}}
\lic|mkConstWithFreshMVarLevels| & \lic| : Name → TacticM Expr| \\
\lic|liftMetaTactic| & \lic| : (MVarId → MetaM (List MVarId)) →| \\
& \phantom{~\li|:|~}\lic|TacticM Unit| \\
\lic|MVarId.apply| & \lic| : MVarId → Expr → MetaM (List MVarId)| \\
\lic|getGoals| & \lic| : TacticM (List MVarId)| \\
\lic|setGoals| & \lic| : List MVarId → TacticM Unit| \\
\lic|MVarId.isAssigned| & \lic| : MVarId → TacticM Bool| \\
\lic|getEnv| & \lic| : TacticM Environment| \\
\lic|SMap.toList| & \lic| : ConstMap → List (Name × ConstantInfo)| \\
\lic|Environment.constants| & \lic| : Environment → ConstMap| \\
\lic|ConstantInfo.isUnsafe| & \lic| : ConstantInfo → Bool| \\
\end{tabular}
\end{center}

This concludes our review of \li{prove_direct}. A similar tactic is available
as \li{apply?} in \li{mathlib}.

\section{Miscellaneous Tactics}
\label{sec:miscellaneous-tactics}

Although the focus of this chapter was on developing new tactics, we encountered
three predefined tactics.

\subsection*{skip}

The \li{skip} tactic succeeds without doing anything. It is sometimes useful as
a building block when we develop custom tactics.

\subsection*{done}

The \li{done} tactic raises a failure if there are some goals left; otherwise,
it succeeds without doing anything. Like \li{skip}, it can be useful as a
building block.

\subsection*{apply?}

The \li{apply?} tactic searches the loaded libraries for a theorem that
exactly proves the goal. On success, it suggests a tactic invocation of the form
\li{exact …}\,, which can be inserted in the formalization.

\section{Summary of Newly Introduced Lean Constructs}

\begingroup
\summarysize

\subsection*{Declaration}

\noindent
\begin{xltabular}{\textwidth}{@{}p{9em}X@{}}
\lic|partial| & prefixes declarations of possibly nonterminating metaprograms \\
\end{xltabular}

\subsection*{Quotations}

\noindent
\begin{xltabular}{\textwidth}{@{}p{9em}X@{}}
\lic|`|\ttvar{n} & quotes a literal name \\
\lic|``|\ttvar{n} & quotes a literal name with elaboration and checking \\
\end{xltabular}

\subsection*{Tactics}

\noindent
\begin{xltabular}{\textwidth}{@{}p{9em}X@{}}
\lic|apply?| & searches for a theorem that proves the current goal \\
\lic|done| & fails if there are some goals left \\
\lic|skip| & does nothing \\
\end{xltabular}

\subsection*{Tactic Combinators}

\noindent
\begin{xltabular}{\textwidth}{@{}p{9em}X@{}}
\lic|<;>| & invokes the second tactic on all subgoals from the \hbox{first tactic} \\
\lic|all_goals| & invokes a tactic once on each goal, expecting \hbox{only successes} \\
\lic|any_goals| & invokes a tactic once on each goal, expecting at least one~success \\
\lic$first | ⋯ |  ⋯$ & tries the tactics in turn until one succeeds \\
\lic|repeat'| & repeatedly invokes a tactic on all goals and subgoals \hbox{until~failure} \\
\lic$solve | ⋯ |  ⋯$ & tries to fully prove the current goal using the tactics in turn \\
\lic|try| & tries to invoke a tactic; does nothing on failure \\
\end{xltabular}

\endgroup
