Manual/Interaction/HOL-interaction.tex

\documentclass[a4paper,10pt]{article}

\usepackage[T1]{fontenc}
\usepackage{upquote}
\usepackage{alltt}
\usepackage{url}

\addtolength{\voffset}{-1em}
\addtolength{\textheight}{-2em}
\addtolength{\textwidth}{0.5em}
\setlength{\arraycolsep}{0.1em}
\input{../LaTeX/commands}

\begin{document}

\title{\bf\Large Guide to HOL4 interaction and basic proofs\vspace{-0.3em}}

\author{\normalsize Magnus O. Myreen}
\date{~\vspace{-2em}}

\maketitle

\newenvironment{code}{\begin{quote}%
\begin{alltt}\small}{%
\end{alltt}%
\end{quote}}
\newenvironment{enum}{\begin{enumerate}
\setlength{\itemsep}{-\parsep}
}{\end{enumerate}}

\renewcommand{\conj}{\(\begin{array}{c}\texttt{\bf\scriptsize/\textbackslash}\\[0.18em]\end{array}\)}
\newcommand{\mysec}[1]{\section{\large #1}}
\newcommand{\mysubsec}[1]{\subsection{\normalsize#1}}
\newcommand{\sq}{\textasciigrave}

\mysec{Introduction}

This document gives readers, with no experience in using HOL4, the most
minimum knowledge needed to start using HOL4. The aim is to give a
concise description of the basics in a format usable as a beginners'
reference manual.
\begin{enum}
\item[~] Section \ref{interaction}:~~Interaction with HOL4 (via emacs)
\item[~] Section \ref{search}:~~Searching for theorems and theories
\item[~] Section \ref{tactics}:~~Common proof tactics
\item[~] Section \ref{reading}:~~Further reading and general advice
\end{enum}
The text assumes that the reader has HOL4 installed. You can download and install HOL4 following the instructions on \url{https://hol-theorem-prover.org}.

\mysec{Interaction with HOL4 (via emacs)\label{interaction}}

Michael Norrish has written an emacs script which makes interaction
with HOL easy. To install the script add the following line to your emacs initialisation file ({\tt
.emacs} or \texttt{.emacs.d/init.el}) with {\tt <path>} replaced with the full path to your HOL4
installation.
\begin{code}
(load "<path>/HOL/tools/hol-mode")
\end{code}
I recommend adding the following (by Chun Tian) to the same file
in order to turn off automatic indentation for the SML mode.
\begin{code}
(defun my-sml-mode-hook ()
  "Local defaults for SML mode"
  (setq electric-indent-chars '()))

(add-hook 'sml-mode-hook 'my-sml-mode-hook)
\end{code}

If your version of emacs does not highlight the active region, also add the following line
to your initialisation file:
\begin{code}
(transient-mark-mode 1)
\end{code}
Restart emacs to make these changes take effect.

\mysubsec{Starting a HOL4 session}

\begin{enum}
\item Start emacs.
\item Press {\tt C-x C-f} to open a file for your proof script.
\item Press {\tt M-h 3} to split the emacs window into two columns and start HOL4.
\end{enum}
The HOL window should look something like this:
\begin{code}
---------------------------------------------------------------------
       HOL-4 [Kananaskis 11 (stdknl, built Mon Feb 05 12:44:20 2018)]

       For introductory HOL help, type: help "hol";
       To exit type <Control>-D
---------------------------------------------------------------------
[Use-ing configuration file /Users/myreen/.hol-config.sml]
> > > > >
\end{code}

\mysubsec{Copying input into HOL4 (Opening a theory)\label{copy}}

First, make sure you know how to select text in emacs. Either:
\begin{itemize}
\item Move the cursor while holding the shift key; or
\item Hit \texttt{C-space}, and then move the cursor normally; or
\item Use the mouse (hold the primary button and drag)
\end{itemize}

To copy and paste the selected region into the HOL session press {\tt M-h~M-r}.
For example, selecting the following line, and then pressing {\tt M-h M-r}
\begin{code}
open arithmeticTheory listTheory;
\end{code}
makes HOL4 open the library theories for arithmetic (over natural numbers)
and lists. HOL4 prints a long list of definitions and already proved results.

\noindent\rule{0em}{1.5em}\emph{Tip:} To avoid long printouts as above, prefix your command with
{\tt C-u C-u} i.e. instead of pressing {\tt M-h M-r} press
{\tt C-u C-u M-h M-r}.

\mysubsec{Starting a goal-oriented proof}

Most HOL4 proofs are constructed using an interactive \emph{goal
  stack} and then put together using the ML function {\tt prove}
(Section~\ref{prove1}, \ref{prove2}). To start the goal stack:
\begin{enum}
\item Write a goal, \eg{} {\tt \sq !n{.}~n~<~n~+~1\sq}, (we can write $\forall$ as {\tt !} in HOL4).
\item Move the cursor inside the back-quotes ({\tt \sq}).
\item Press {\tt M-h~g} to push the goal onto the goal stack.
\end{enum}
The HOL4 window should look something like this:
\begin{code}
> val it =
     Proof manager status: 1 proof.
  1. Incomplete goalstack:
       Initial goal:
       \(\forall\)n. n < n + 1

   : proofs
> val it = () : unit
\end{code}

\mysubsec{Applying a tactic\label{apply}}

Make progress in a proof using \emph{proof tactics}.

\begin{enum}
\item Write the name of a tactic, \eg{} {\tt decide\_tac},~see Section~\ref{tactics} for more tactics
\item Select the text of the tactic
\item Press {\tt M-h~e} to apply the tactic.
\end{enum}
A tactic makes HOL4 update the current goal. The HOL4 window will either
display the new goal(s) or print:
\begin{code}
    Initial goal proved.
    |- \(\forall\)n. n < n + 1 : goalstack
\end{code}
You can undo the effect of the applied tactic by pressing {\tt M-h b}. Press {\tt M-h p} to view the current goal.
To go all the way back to the start of the proof (to restart), press \texttt{M-h~R}.

\mysubsec{Ending a goal-oriented proof}

One can pop goals off the goal stack by pressing {\tt M-h d}, which gives:
\begin{code}
> OK..
val it = There are currently no proofs. : proofs
\end{code}

\mysubsec{Saving the resulting theorem\label{prove1}}

One can use {\tt prove} to store the result of a proof (called a
\emph{theorem}), \eg{} the following stores the theorem $\forall n.\;n < n +
1$ in an ML variable {\tt LESS\_ADD\_1}:
\begin{code}
val LESS_ADD_1 = Q.prove(`!n. n < n + 1`, decide_tac);
\end{code}
When the above line is copied into HOL4 (using text-selection then
{\tt M-h M-r}, as described in Section~\ref{copy}), HOL4 responds with:
\begin{code}
> val LESS_ADD_1 = |- !n. n < n + 1 : thm
\end{code}

\mysubsec{Saving proofs based on multiple tactics\label{prove2}}

Suppose we have proved the goal {\tt \sq !n{.}~n <= n * n\sq} with the following tactics:
\begin{code}
Induct_on `n`                   (* comment: induction on n  *)

  decide_tac                    (* comment: solve base case *)

  asm_simp_tac bool_ss [MULT]   (* comment: simplify goal   *)
  decide_tac                    (* comment: solve step case *)
\end{code}
Tactics can be pieced together for {\tt prove} using \ml{\gt\gt} and \ml{\gt-}. The \ml{\gt\gt} operator is an infix that composes tactics. Similarly, \ml{\gt-} \emph{tac} proves the first subgoal using \emph{tac}.
\begin{code}
val LESS_EQ_MULT = Q.prove(
  `!n:num. n <= n * n`,
  Induct_on `n`
  >- decide_tac
  >- (asm_simp_tac bool_ss [MULT]
      \gt\gt decide_tac));
\end{code}
Copy the above into HOL4 using text-selection, and then {\tt M-h M-r}, as in Section~\ref{copy}.

\newcommand{\itemz}[2]{\texttt{#1}\; &-\;\; \textrm{#2}}
\newcommand{\itemy}[2]{#1&\quad\quad&#2\\}

\begin{figure}[t]
\hrule

\begin{displaymath}
\begin{array}{lllll}
\itemy{\itemz{\rule{0em}{1.5em}M-h h}{start HOL}}{\itemz{M-h g}{push goal onto goal stack}}
\itemy{\itemz{M-h M-r}{copy region into HOL}}{\itemz{M-h e}{apply tactic to goal}}
\itemy{\itemz{M-h C-t}{display types on/off}}{\itemz{M-h b}{move back in proof}}
\itemy{\itemz{M-h C-c}{interrupt HOL}}{\itemz{M-h p}{print current goal}}
\itemy{&}{\itemz{M-h d}{drop current goal}}
\end{array}
\end{displaymath}
\caption{Most important key bindings in the emacs HOL4 mode.
Note that all of these actions are also available in the HOL menu within Emacs.}

\rule{0em}{1.5em}\hrule
\end{figure}

\mysubsec{Displaying types in HOL4}

HOL4 does not by default display types. Press {\tt M-h~C-t} to switch
printing of type information on or off.

\mysubsec{Interrupting HOL4}

Press {\tt M-h~C-c} to interrupt HOL4 --- useful when a tactic fails to terminate
(\eg{} {\tt\small metis\_tac} often fails to terminate when unsuccessfully applied).

\mysubsec{Making a definition\label{definition}}

Function can be defined using {\tt Define}, \eg{} square is defined as follows.
\begin{code}
val SQUARE_def = Define `SQUARE n = n * n`;
\end{code}

\noindent
Data-types are defined using {\tt Datatype}, \eg{} a binary tree
which holds values of type {\tt 'a} (a type variable) at the leaves:
\begin{code}
val _ = Datatype `TREE = LEAF 'a | BRANCH TREE TREE`;
\end{code}

\noindent
A valid tree is \eg{} {\tt BRANCH (LEAF 5) (BRANCH (LEAF 1) (LEAF 7))}
with type {\tt num TREE}, where {\tt  num} is the type name for a natural
number. We can define recursive functions, \eg{}
\begin{code}
val MAP_TREE_def = Define `
  (MAP_TREE f (LEAF n) = LEAF (f n)) \conj{}
  (MAP_TREE f (BRANCH u v) = BRANCH (MAP_TREE f u) (MAP_TREE f v))`;
\end{code}
{\tt  SQUARE\_def} and {\tt  MAP\_TREE\_def} are theorems containing the
above definitions. Theorems describing {\tt  TREE} can be retrieved by coping
the following into HOL4 (by pressing {\tt C-space} then {\tt M-h M-r}, Section~\ref{copy}).
\begin{code}
val TREE_11 = fetch "-" "TREE_11";
val TREE_distinct = fetch "-" "TREE_distinct";
\end{code}

\mysubsec{Making a theory}

Proofs and definitions are stored in files called scripts, \eg{} we
can store the definitions from above in a file called {\tt
  mytreeScript.sml}, which should begin with the lines
\begin{code}
open HolKernel boolLib bossLib Parse
val _ = new_theory "mytree";
\end{code}
and end with the line
\begin{code}
val _ = export_theory();
\end{code}
Replace {\tt prove} by {\tt store\_thm} for results you
wish to export from the theory, \eg{}
\begin{code}
val LESS_ADD_1 = Q.store_thm("LESS_ADD_1",{`}!n.n<n+1{`},decide_tac);
\end{code}
Make sure your script only consists of ML definitions ({\tt \small val
  x = y}, {\tt \small fun g x = y}), open commands ({\tt \small
  open x y z}) and comments {\tt \small (* comment *)}.

The theory {\tt mytreeTheory} is created by executing {\tt Holmake} in
the directory where {\tt mytreeScript.sml} is stored. A
readable version of the theory is stored under {\tt mytreeTheory.sig}.

\mysec{Searching for theorems and theories\label{search}}

\newcommand{\itemx}[2]{\texttt{\small #1} &\;\textrm{--}\;& \textrm{#2} \\}

HOL4 has a large collection of library theories. The most commonly used are:
\begin{displaymath}
\begin{array}{lcl}
\itemx{arithmeticTheory}{natural numbers, \eg{} {\tt\small 0, 1, 2, SUC 0, SUC 6}}
\itemx{listTheory}{lists, \eg{} {\tt\small [1;2;3] = 1::2::3::[], HD xs}}
\itemx{pred\_setTheory}{simple sets,\ \eg{} {\tt\small \{1;2;3\}, x IN s UNION t}}
\itemx{pairTheory}{pairs/tuples,\ \eg{} {\tt\small (1,x), (2,3,4,5), FST (x,y)}}
\itemx{wordsTheory}{n-bit words,\ \eg{} {\tt\small 0w:word32, 1w:'a word, x {!!}~1w}}
\end{array}
\end{displaymath}
Other standard theories include:
\begin{code}
arithmeticTheory  bagTheory  boolTheory  combinTheory  fcpTheory
finite_mapTheory  fixedPointTheory  floatTheory  integerTheory
limTheory  optionTheory  probTheory  ratTheory  realTheory
relationTheory  rich_listTheory  ringTheory  seqTheory
sortingTheory  state_transformerTheory  stringTheory  sumTheory
topologyTheory  transcTheory  whileTheory
\end{code}
The library theories are conveniently browsed using the following HTML reference page (created when HOL4 is compiled).
Replace {\tt <path>} with the path to your HOL4 installation.
\begin{code}
<path>/HOL/help/HOLindex.html
\end{code}

Once theories has been opened (see Section~\ref{copy}), one can search for theorems in the current
context using {\tt print\_match}, \eg{} with {\tt arithmeticTheory} opened,
\begin{code}
print_match [] {`}`n DIV m <= k{`}`
\end{code}
prints a list of theorems containing $n\; \texttt{\small DIV} \;m \leq k$ for some $n,m,k$:
\begin{code}
arithmeticTheory.DIV_LE_MONOTONE (THEOREM)
------------------------------------------
|- !n x y. 0 < n \(\land\) x <= y ==> x DIV n <= y DIV n

arithmeticTheory.DIV_LE_X (THEOREM)
-----------------------------------
|- !x y z. 0 < z ==> (y DIV z <= x <=> y < (x + 1) * z)

arithmeticTheory.DIV_LESS_EQ (THEOREM)
--------------------------------------
|- !n. 0 < n ==> !k. k DIV n <= k
\end{code}
Try to write increasingly specific queries if the returned list is long, \eg{}
{\tt\small print\_match [] \sq \sq n DIV m\sq\sq} returns a list of length 32. Note that {\tt\small print\_match [] \sq \sq DIV\sq\sq}
does not work since {\tt\small DIV} is an infix operator, but {\tt\small print\_match [] \sq \sq \$DIV\sq \sq} works.

The key-binding \texttt{M-h~m} (and the menu entry ``DB match'') will prompt for the term pattern to search for, and pass this query onto the HOL session (saving the need to type \texttt{print\_match~[]} and the enclosing quotation marks).

\mysec{Common proof tactics\label{tactics}}

Most HOL4 proofs are carried out by stating a goal and then applying
\emph{proof tactics} that reduce the goal.  This section describes
basic use of the most important proof tactics.  Press {\tt\small
  C-space} then {\tt\small M-h e} to apply a tactic
(Section~\ref{apply}).


\mysubsec{Automatic provers}

Simple goals can often be proved automatically by {\tt\small
  metis\_tac}, {\tt\small decide\_tac} or {\tt\small EVAL\_TAC}.
{\tt\small metis\_tac} is first-order prover which is good at general
problems, but requires the user to supply a list of relevant theorems,
\eg{} the following goal is proved by {\tt\small metis\_tac
  [MOD\_TIMES2,MOD\_MOD,MOD\_PLUS]}.
\begin{code}
!k. 0 < k ==> !m p n. (m MOD k * p + n) MOD k = (m * p + n) MOD k
\end{code}

\noindent
{\tt\small decide\_tac} handles linear arithmetic over natural
numbers, \eg{} {\tt\small decide\_tac} solves:
\begin{code}
!m n k. m < n \conj{} n < m+k \conj{} k <= 3 \conj{} ~(n = m+1) ==> (n = m+2)
\end{code}
{\tt\small EVAL\_TAC} is good at fully instantiated goals, \eg{} {\tt\small EVAL\_TAC} solves:
\begin{code}
0 < 5 \conj{} (HD [4;5;6;7] + 2**32 = 3500 DIV 7 + 4294966800)
\end{code}

\mysubsec{Proof set-up}

Goals that contain top-level universal quantifiers ({\tt !x.}),
implication ({\tt ==>}) or conjunction ({\tt \conj{}}) are often
taken apart using {\tt\small rpt strip\_tac} or just {\tt\small
  strip\_tac}, \eg{} the goal {\tt\small \sq !x{.}~(!z{.}~x < h z) ==> ?y{.}~f x = y\sq}
becomes the following. (Assumptions are written under the line.)
\begin{code}
    ?y. f x = y
    ------------------------------------
      !z. x < h z
\end{code}

\mysubsec{Existential quantifiers}

Goals that have a top-level existential quantifier can be given a
witness using {\tt \small qexists\_tac}, \eg{} {\tt \small
  qexists\_tac \sq 1\sq} applied to goal {\tt \small ?n{.}~!k{.}~n * k = k}
produces goal {\tt \small !k{.}~1 * k = k}.

\mysubsec{Rewrites}

Most HOL4 proofs are based on rewriting using equality theorems, \eg{}
\begin{code}
ADD_0:            |- !n. n + 0 = n
LESS_MOD:         |- !n k. k < n ==> (k MOD n = k)
\end{code} {\tt \small asm\_simp\_tac} and {\tt \small full\_simp\_tac} are two
commonly used rewriting tactics, \eg{} suppose the goal is the following:
\begin{code}
    5 + 0 + m = (m MOD 10) + (5 MOD 8)
    ------------------------------------
      0.  p = 2 + 0 + (m MOD 10)
      1.  m < 10
\end{code}
{\tt \small asm\_simp\_tac bool\_ss
  [ADD\_0,LESS\_MOD]} rewrites the
goal using the supplied theorems together with the current goal's
assumptions and some boolean simplifications {\tt \small bool\_ss}:
\begin{code}
    5 + m = m + (5 MOD 8)
    ------------------------------------
      0.  p = 2 + 0 + (m MOD 10)
      1.  m < 10
\end{code}
{\tt \small full\_simp\_tac bool\_ss [ADD\_0,LESS\_MOD]}
does the same except that it also applies the rewrites to the
assumptions:
\begin{code}
    5 + m = m + (5 MOD 8)
    ------------------------------------
      0.  p = 2 + m
      1.  m < 10
\end{code}
{\tt \small bool\_ss} can be replaced by {\tt \small std\_ss}, which
is a stronger simplification set that would infer {\tt \small 5 < 8}
and hence simplify {\tt\small 5 MOD 8} as well. I recommend that the
interested reader also reads about {\tt\small AC}, {\tt\small Once}
and {\tt\small srw\_tac}.

\mysubsec{Induction}

Use the tactic {\tt\small Induct\_on \sq x\sq} to start an induction on {\tt\small x}.
Here {\tt x} can be any variable with a recursively defined type,
\eg{} a natural number, a list or a {\tt\small TREE} as defined in
Section~\ref{definition}.  One can start a complete (or strong)
induction over the natural number {\tt\small n} using {\tt\small
  completeInduct\_on \sq n\sq}.
As with \texttt{Cases\_on} one can also induct on terms (\eg, \texttt{\small Induct\_on~\sq hi~-~lo\sq}), though these proofs can be harder to carry out.

\mysubsec{Case splits}

A goal can be split into cases using {\tt\small Cases\_on \sq x\sq}. The
goal is split according to the constructors of the type of {\tt\small
  x}, \eg{} for the following goal
\begin{code}
    !x. ~(x = []) ==> (x = HD x::TL x)
\end{code}
{\tt\small Cases\_on \sq x\sq} splits the goal into two:
\begin{code}
    ~(h::t = []) ==> (h::t = HD (h::t)::TL (h::t))

    ~([] = []) ==> ([] = HD []::TL [])
\end{code}
Case splits on boolean expressions are also useful, \eg{} {\tt\small Cases\_on \sq n < 5\sq}.

\mysubsec{Subproofs}

It is often useful to start a mini-proof inside a larger proof, \eg{} for the goal
\begin{code}
    foo n
    ------------------------------------
      0 < n
\end{code}
we might want to prove {\tt\small h n = g n} assuming {\tt\small 0 <
  n}.
We can start such a subproof by typing {\tt\small sg \sq h n = g n\sq}.%
\footnote{You can also use the emacs binding {\tt\small M-h M-s}
with the cursor inside the sub-goal.} The new goal stack:
\begin{code}
    foo n
    ------------------------------------
      0.  0 < n
      1.  h n = g n

    h n = g n
    ------------------------------------
      0 < n
\end{code}
If {\tt\small \sq h n = g n\sq} can be proved in one step, \eg{} using {\tt\small metis\_tac [MY\_LEMMA]}, then
apply {\tt\small \sq h n = g n\sq \ by metis\_tac [MY\_LEMMA]} instead of
{\tt\small sg \sq h n = g n\sq}.  If the sub-goal requires
multiple steps the tactic after the \texttt{by} will need to be
parenthesised: {\tt\small\sq\textit{goal}\sq \ by ($\mathit{tac}_1$ \ml{\gt\gt}
  $\mathit{tac}_2$ ...)}

\mysubsec{Proof by contradiction}

Use {\tt\small CCONTR\_TAC} to add the negation of the goal to the
assumptions.  The task is then to prove that one of the assumptions of
the goal is false. One can \eg{} add more assumptions using
{\tt\small \sq...\sq \ by ...}, described above, until one assumption is the
negation of another assumption (and then apply {\tt\small metis\_tac []}).

\mysubsec{More tactics\label{html}}

An HTML reference of all tactics and proof tools is created when HOL4 is compiled.
Replace {\tt\small <path>} with the path to your HOL4 installation.
\begin{code}
<path>/HOL4/help/src/htmlsigs/idIndex.html
\end{code}
The reference provides an easy way to access both the implementations of
tactics as well as their documentation (where such exists).
The interested reader may want to look up the following:
\begin{code}
CONV_TAC  disj1_tac  disj2_tac  match_mp_tac  mp_tac  pat_assum  Q
\end{code}

\mysec{Further reading and general advice\label{reading}}

General advice on using HOL4:
\begin{enum}
\item State definitions carefully with the subsequent proofs in mind.
\item Make proofs reusable by splitting them into multiple small lemmas.
\item Strive to make the most of library theories and rewriting.
\end{enum}
One can only learn HOL4 via examples, so try proving something.
Example problems and solutions are presented in the \emph{HOL
  Tutorial}, available under:
\begin{center}
\url{https://hol-theorem-prover.org/#doc}
\end{center}
The same page also contains links to:
\begin{enum}
\item[~]\emph{HOL Description} -- a description of the HOL4 system
\item[~]\emph{HOL Reference} -- a detailed descriptions of proof tactics and other tools
\item[~]\emph{HOL Logic} -- a presentation of the underlying logic
\end{enum}
For day-to-day look-ups, I find {\tt print\_match} (illustrated in
Section~\ref{search}) and the HTML reference (mentioned in
Section~\ref{html}) most helpful.

\end{document}