example1.tex

\section{A First (Pen and Paper Style) Proof}\label{sec:hol_ex1}
%
The HOL4 features presented so far are exactly those of an interpreted
programming language.
Next, we will define our first function in HOL4, and prove a first theorem about
it.

%A common mathematical notation is $\sum_{i=0}^n f (i)$,
%summing the numbers from $0$ to $n$, and applying function $f$.
%We define a specialized version for $f (x) = x$ in HOL4:
The function we will define is a sum of natural numbers up to $n$,
$\sum_{i=0}^n i$.
A HOL4 definition looks like this:

\begin{lstlisting}
Definition sumFun_def:
  sumFun (n:num) = if (n = 0) then 0 else n + sumFun (n-1)
End
\end{lstlisting}

The \lstinline{Definition} and \lstinline{End} keyword tell the REPL that we
define a HOL4 function and mark its end.
In the REPL, \lstinline{sumFun_def} is the name of the definition, under which it
can be accessed.
As a convention, when defining function $f$ in HOL4, its definition should be
named \lstinline{f_def}.
The type annotation \lstinline{n:num} tells the HOL4 REPL to parse variable \texttt{n}
as a natural number.
To load the definition into the HOL4 REPL, mark it completely, including the \lstinline{Definition}
keyword and the \lstinline{End} keyword, and send it to the REPL with \ekey{M-h M-r}.

Alternatively, HOL4 also supports defining a function by a system of equations,
moving the \texttt{case} expression of the \lstinline{sum} function to the
outside:
%
\begin{lstlisting}
Definition sum_def:
  sum 0 = 0 /\
  sum (n:num) = n + sum (n-1)
End
\end{lstlisting}

To avoid a name clash we have renamed the function into \lstinline{sum}.
As for the definition of \lstinline{sumFun_def}, to send the definition to the REPL,
mark it and send it with \ekey{M-h M-r}.
Choosing one definition over the other has different benefits and downsides.
As a rule of thumb, it is recommended to choose the latter version, giving a
system of equations if the function requires a top-level \texttt{case}
expression.
We will do the proof for the function \texttt{sum} here, and give a general
guideline on when to prefer which version later in \autoref{subsec:tipsAndTricks}.

As a simple, first example, we will prove a closed form for \lstinline{sum n}:
\[
  \sum_{i=0}^{n} i = \frac{n * (n + 1)}{2}
\]

In HOL4 this theorem is stated as

\begin{lstlisting}
Theorem closed_form_sum:
  ! n. sum n = n * (n + 1) DIV 2
Proof
QED
\end{lstlisting}

Again, \lstinline{Theorem}, \lstinline{Proof}, and \lstinline{QED} are the
keywords marking a theorem statement in the REPL and the indented line is
the statement that we want to prove.
Similar to a definition, the name \lstinline{closed_form_sum} is an identifier
which is used later to refer to the theorem statement proven in other proofs.
This makes theorems first class citizens of the HOL4 REPL, also allowing
functions to manipulate and inspect their statements.

When proving a theorem for the first time in HOL4, the proof is usually done
interactively.
Starting an interactive proof is as simple as marking the indented line
(\lstinline{! n. sum n = n * (n + 1) DIV 2}) and pressing \ekey{M-h g}.
The HOL4 REPL prints

\begin{lstlisting}[mathescape=true, frame=single]
> val it =
   Proof manager status: 1 proof.
   1. Incomplete goalstack:
        Initial goal:
        $\forall$ n. sum n = n * (n + 1) DIV 2
   : proofs
\end{lstlisting}

In HOL4, theorems are proven by applying so-called \emph{tactics} to the current
goal.
These tactics are a group of SML functions, implemented in the HOL4
distribution, and filled in between the \lstinline{Proof} and the \lstinline{QED}
keywords.
In this tutorial, we decouple learning how the theorem prover works from
learning the syntax of the tactics language by performing interactive proofs
with Lassie using natural language.

To load Lassie and the natural language descriptions required for the proof,
run
\begin{lstlisting}
open LassieLib arithTacticsLib logicTacticsLib arithmeticTheory;
val _ = LassieLib.loadJargon "Arithmetic";
val _ = LassieLib.loadJargon "Logic";
\end{lstlisting}
interactively.

The closed form is the standard example for proofs by induction in math classes.
Following this example, we start the proof with
\begin{lstlisting}
nltac `Induction on 'n'.`
\end{lstlisting}

Here, \lstinline{nltac} is a Lassie function that parses natural language and
translates it into a HOL4 tactic.
The parameter \lstinline{`Induction on 'n'.`} is the natural language
description of the tactic used.
To apply the tactic, the line must be marked and run with \ekey{M-h e}.
After running the code, the HOL4 REPL shows
\begin{lstlisting}
> OK..
2 subgoals:
val it =

    0.  sum n = n * (n + 1) DIV 2
   ------------------------------------
        sum (SUC n) = SUC n * (SUC n + 1) DIV 2

   sum 0 = 0 * (0 + 1) DIV 2

2 subgoals
   : proof
\end{lstlisting}

The line \lstinline{2 subgoals} tells us that we must prove two separate goals
to finish the proof.
As HOL4 keeps track of these subgoals for us, we need not manage them manually
to make sure that the proof remains error-free.
Note that in the induction step, HOL4 automatically adds the inductive
hypothesis as an assumption (labeled with \lstinline{0}) above a dashed line.

First, we prove the base case \lstinline{sum 0 = 0 * (0 + 1) DIV 2}, then we
show the induction step \lstinline{sum (n + 1) = (n + 1) * (n + 2) DIV 2}.
Function \lstinline{SUC} is the HOL4 version of Peano's successor function.
Intuitively \lstinline{SUC n} refers to the natural number after \lstinline{n},
i.e. \lstinline{n + 1}.

As for a pen-and-paper proof, the base case of the induction is trivial, and
solved with the simple statement \lstinline{nltac `use [sum_def] to simplify.`},
leaving us only with the induction step from above.
In contrast to a pen-and-paper proof, we have to explicitly state that we
simplify with the definition of our summation function (\lstinline{sum_def}).
This is part of the enforced rigour required by the theorem prover\footnote{
We will show in \autoref{subsec:tipsAndTricks} how one can get rid of this in certain cases.}.

As for a pen-and-paper proof, the first step on the induction step is to
simplify:
\begin{lstlisting}
nltac `use [sum_def, GSYM ADD_DIV_ADD_DIV] to simplify.`
\end{lstlisting}

Here, \lstinline{ADD_DIV_ADD_DIV} is a theorem from the HOL4 standard library
used to enrich the simplifier with the additional knowledge.
To find out its statement, mark the theorem name only, and send it to the
REPL with \ekey{M-h M-r}.
Sending \lstinline{GSYM} to the REPL shows that the function has type
\lstinline{:thm -> thm}, meaning that it takes a theorem as input and returns a
theorem.
Function \lstinline{GSYM} is a polyML function rotating an equality theorem,
replacing equality $a = b$ with equality $b = a$.
Sending \lstinline{GSYM ADD_DIV_ADD_DIV} and \lstinline{ADD_DIV_ADD_DIV} to the REPL, one can
observe its effect easily.

Using \lstinline{GSYM} can be useful from time to time as rewriting in HOL4 is
directed from left-to-right.
If we have a theorem showing $f x = b$, HOL4 will rewrite any occurence of
$f x$ into an occurence of $b$, but it will never replace occurences of $b$
with occurences of $f x$.

After applying the tactic, the REPL will show the subgoal that remains to be proven:
\begin{lstlisting}
> OK..
1 subgoal:
val it =

    0.  sum n = (n * (n + 1)) DIV 2
   ------------------------------------
        (2 * SUC n + n * (n + 1)) DIV 2 = SUC n * (SUC n + 1) DIV 2

   : proof
\end{lstlisting}

Applying the following tactics step-by-step closes the proof:

\begin{lstlisting}
nltac `'2 * SUC n + n * (n + 1) = SUC n * (SUC n + 1)' suffices to show the goal.`
nltac `show 'SUC n * (SUC n + 1) = (SUC n + 1) + n * (SUC n + 1)' using (simplify with [MULT_CLAUSES]).`
nltac `simplify.`
nltac `show 'n * (n + 1) = SUC n * n' using (trivial using [MULT_CLAUSES, MULT_SYM]).`
nltac `'2 * SUC n = SUC n + SUC n' follows trivially.`
nltac `'n * (SUC n + 1) = SUC n * n + n' follows trivially.`
nltac `rewrite assumptions. simplify.`
\end{lstlisting}

\begin{sloppypar}
The natural language tactic \lstinline{`show 'SUC n * (SUC n + 1) = (SUC n + 1) + n * (SUC n + 1)' using (simplify with [MULT_CLAUSES]).`}
shows another feature of HOL4:
We can extend the list of assumptions with the theorem mentioned after
\lstinline{show}.
Before running the tactic, the state of the goal is
\end{sloppypar}
\begin{lstlisting}
> OK..
1 subgoal:
val it =

    0.  sum n = n * (n + 1) DIV 2
   ------------------------------------
        2 * SUC n + n * (n + 1) = SUC n * (SUC n + 1)

   : proof
\end{lstlisting}

and after running the tactic, the subgoal becomes
\begin{lstlisting}
> OK..
1 subgoal:
val it =

    0.  sum n = n * (n + 1) DIV 2
    1.  SUC n * (SUC n + 1) = SUC n + 1 + n * (SUC n + 1)
   ------------------------------------
        2 * SUC n + n * (n + 1) = SUC n * (SUC n + 1)

   : proof
\end{lstlisting}

Running all tactics, one after another, the REPL shows that the proof is finished by printiting
\begin{lstlisting}
> OK..

val it =
   Initial goal proved.
   $\vdash$ $\forall$ n. sum n = n * (n + 1) DIV 2: proof
\end{lstlisting}

To reuse the theorem later, and to make it automatically checkable by HOL4, we
have to put the natural language into a single call to \lstinline{nltac}.
The full code for the theorem is given in \autoref{fig:gaussProof}.
%
\begin{figure}[t]
\begin{lstlisting}[mathescape=true]
Theorem closed_form_sum:
  $\forall$ n. sum n = (n * (n + 1)) DIV 2
Proof
  nltac `
   Induction on 'n'.
   use [sum_def] to simplify.
   use [sum_def, GSYM ADD_DIV_ADD_DIV] to simplify.
   use [sum_def, GSYM ADD_DIV_ADD_DIV] to simplify.
   '2 * SUC n + n * (n + 1) = SUC n * (SUC n + 1)' suffices to show the goal.
   show 'SUC n * (SUC n + 1) = (SUC n + 1) + n * (SUC n + 1)' using (simplify with [MULT_CLAUSES]).
   simplify.
   show 'n * (n + 1) = SUC n * n' using (trivial using [MULT_CLAUSES, MULT_SYM]).
   '2 * SUC n = SUC n + SUC n' follows trivially.
   'n * (SUC n + 1) = SUC n * n + n' follows trivially.
   rewrite assumptions. simplify.
QED
\end{lstlisting}
\caption{Complete proof of the closed form for summing natural numbers until $n$ using Lassie}\label{fig:gaussProof}
\end{figure}

Marking the complete statement, and running it with \ekey{M-h M-r} will save the
theorem under the name \lstinline{gaussian_sum}.
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "main"
%%% End: