tipsTricks.tex

\section{Small Tips and Tricks}\label{subsec:tipsAndTricks}

We end this tutorial by giving some helpful tips and tricks, and giving pointers
where to find more information about HOL4.

\subsection{Extending the Simplifier}
While proving the gaussian sum in \autoref{sec:hol_ex1} we had to explicitly
tell the simplifier that it should also use the definition of function
\lstinline{sum} while proving properties about the function.
In a pen-and-paper proof, one would never explicitly write this down and as such
it is desirable to have the same convenience in HOL4.
We can do so by slightly changing the definition of \lstinline{sum}:
%
\begin{lstlisting}
Definition sum_def[simp]:
  sum 0 = 0 /\
  sum n = n + sum (n-1)
End
\end{lstlisting}

By appending \lstinline{[simp]} to the name of the function, HOL4 automatically
adds \lstinline{sum_def} to the list of theorems used by the simplifier.
A similar mechanism exists for adding theorems to the simplifier.
However, this mechanic has to be used with caution as it is very easy to make
the simplifier diverge.

As an example, suppose we used the old definition of \lstinline{sum} which
defines the function as a recursive function not in equational style:

\begin{lstlisting}
Definition sum_def[simp]:
  sum n = if (n = 0) then 0 else n + sum (n-1)
End
\end{lstlisting}

If we restart the proof for the gaussian sum now, and run through the first two
tactics only (\lstinline{nltac `Induction on 'n'. simplify.`}) HOL4 will just
keep running.
As a rule of thumb, it is recommended to be conservative and rather mention a
definition than adding it to the simplifier.
The machinery can be useful for (non-recursive) abbreviations.
For theorems, one should refrain from adding commutativity or associativity
theorems, but adding theorems of the form $\forall x. P x \rightarrow Q x$, where
$Q$ does not depend on $P$ should be fine.

\subsection{Making Proof Scripts More Robust}
The most cumbersome work once a proof has been developed is making sure that it
remains correct even when versions of HOL4 change.
We give some simple recommendations that have proven quite useful over time.

First, we recommend commenting larger case splits and induction proofs.
While it may seem obvious now which case is being worked on by the proofscript
this might not be the case in a month, or a year of time after writing the
initial version.

Second, we recommend using tactics like
\lstinline{first_x_assum, last_assum, qpat_x_assum}.
These tactics are independent of the specific order of assumptions and thus make
the proof more robust to additional assumptions, or their removal.

\subsection{Getting More Help}
This small tutorial has only covered the basics.
More reference material can be found on \url{https://hol-theorem-prover.org/#doc}.
We especially recommend looking at the documentation of the emacs mode
(\url{https://hol-theorem-prover.org/hol-mode.html}), and the description manual.

The help index located at \lstinline{<HOLDIR>/help/HOLindex.html} provides
documentation for a lot of tactics and contains signature files for all of the
HOL4 distributions libraries and theories.

Finally, the HOL-info mailing list
(\url{https://sourceforge.net/projects/hol/lists/hol-info}) is a good place to
ask further questions, as well as the \texttt{\#hol} channel of the Slack of the
CakeML project (\url{https://join.slack.com/t/cakeml/shared_invite/MjM1NjEyODgxODkzLTE1MDQzNjgwMTUtYjI4YTdlM2VmMQ}).