HOL4tactics.tex

\section{Learning HOL4 Tactics}

In the previous examples we have used Lassie to prove theorems in HOL4 in a
rigorous but still human readable format.
HOL4 itself supports a richer set of so-called tactics that are commonly used
when proving theorems.

We will next show how Lassie can be used to learn a first set of basic tactics
and explain some of their intricacies that a beginner may struggle with.
Instead of using function \lstinline{nltac} to parse textual descriptions into HOL4
tactics, we next use Lassie's proof-REPL \lstinline{nlexplain} to interactively
develop a first proof script by looking again at the proof of the gaussian sum
in \autoref{fig:gaussProof}.

Therefore we (re-)start the interactive proof with \lstinline{g `! n. sum n = (n * (n + 1)) DIV 2`}
and sending it to the REPL with \ekey{M-h M-r}.
The HOL4 REPL prints:
\begin{lstlisting}[frame=single, mathescape=true, deletekeywords={Proof}]
> > # # # val it =
   Proof manager status: 1 proof.
   1. Incomplete goalstack:
     Initial goal:
     $\forall$ n. sum n = n * (n + 1) DIV 2
   : proofs
\end{lstlisting}

As before the interactive proof shows us the current goal that we have to proof.
Next, we start the Lassie's proof-REPL with \lstinline{nlexplain()} and
sending it with \ekey{M-h M-r}.
Note that the REPL changes from \lstinline{>} to \lstinline{|>} to denote that
Lassie is capturing the input.
Instead of sending the full proofscript with \lstinline{nltac}, one can now send
each step separately and observe its output.
Sending the first step from the Lassie proof (\lstinline{Induction on 'n'.}) with
\ekey{M-h M-r} prints
%
\begin{lstlisting}[frame=single]
Induct_on ` n `
 >- (
 sum 0 = 0 * (0 + 1) DIV 2)
 >- (
  0.  sum n = n * (n + 1) DIV 2
 ------------------------------------
      sum (SUC n) = SUC n * (SUC n + 1) DIV 2)
\end{lstlisting}

This tells us that the HOL4 equivalent to Lassies ``Induction on 'n''' is the
tactic \lstinline{Induct_on `n`}.
The tactic takes a HOL4 expression, called a term as input and tries to perform
an induction on it using the underlying types induction scheme.

Next, we see a so-called tactic combinator that can be used to chain tactics
together.
In Lassie's proofs we relied on the ``.'' to do this for you, similar to
pen-and-paper proofs.
A HOL4 tactic proof however requires manually putting the tactics together.
Here we see \lstinline{>-} which combines a tactic (\lstinline{Induct_on})
with a tactic solving a single subgoal.

If we send the next step, \lstinline{use [sum_def] to simplify.}, from the Lassie proof, the REPL shows
%
\begin{lstlisting}[frame=single]
Induct_on ` n `
 >- (
 fs [ sum_def ])
 >- (
  0.  sum n = n * (n + 1) DIV 2
 ------------------------------------
      sum (SUC n) = SUC n * (SUC n + 1) DIV 2)
\end{lstlisting}

The tactic \lstinline{fs [ sum_def ]} has been used by Lassie to solve the first subgoal
of the proof, but the second subgoal remained unchanged.
If we want to also simplify the second goal, we have to send the Lassie step again,
leaving us with
%
\begin{lstlisting}[frame=single]
Induct_on ` n `
 >- (
 fs [ sum_def ])
 >- (
 fs [ sum_def ] >>
   0.  sum n = n * (n + 1) DIV 2
  ------------------------------------
       SUC n + n * (n + 1) DIV 2 = SUC n * (SUC n + 1) DIV 2)
\end{lstlisting}

Here, we also see another tactic combinator of HOL4, \lstinline{>>}, which can
alternatively be written as \lstinline{\\}.
Applying tactic \lstinline{t1 >> t2} applies tactic \lstinline{t2} to every
subgoal  generated by \lstinline{t1} and fails if \lstinline{t2} fails on one of
the subgoals.
Note that for all tactic combinators, their second argument can themselves be
tactics composed by applications of \lstinline{>>} and \lstinline{>-}.

We recommend sending each of steps of the Lassie proof separately to construct a
full proof script and getting an intuitive meaning of the tactics.
If a step should be undone one can send the command \lstinline{back.}, and
\lstinline{help.} prints a quick help message.
Sending \lstinline{exit.} ends the \lstinline{nlexplain} session.
The proof script generated by Lassie can then be copied and played with
interactively to get a feeling for the tactics themselves.
We recommend using the goal manager used before to start an interactive proof of
the closed form of the summation.
Tactics from the proof script can then be send separately or joined together by
marking them and pressing \ekey{M-h e}.