Example: Euclid's Theorem

In this chapter, we prove in HOL that for every number, there is a prime number that is larger, i.e., that the prime numbers form an infinite sequence. This proof has been excerpted and adapted from a much larger example due to John Harrison, in which he proved the $n = 4$ case of Fermat's Last Theorem. The proof development is intended to serve as an introduction to performing high-level interactive proofs in HOL.¹ Many of the details may be difficult to grasp for the novice reader; nonetheless, it is recommended that the example be followed through in order to gain a true taste of using HOL to prove non-trivial theorems.

Some tutorial descriptions of proof systems show the system performing amazing feats of automated theorem proving. In this example, we have not taken this approach; instead, we try to show how one actually goes about the business of proving theorems in HOL: when more than one way to prove something is possible, we will consider the choices; when a difficulty arises, we will attempt to explain how to fight one's way clear.

One ‘drives’ HOL by interacting with the ML top-level loop, perhaps mediated via an editor such as emacs or vim. In this interaction style, ML function calls are made to bring in already-established logical context, e.g., via load; to define new concepts, e.g., via Datatype, Define, and Hol_reln; and to perform proofs using the goalstack interface, and the proof tools from bossLib (or if they fail to do the job, from lower-level libraries).

Let's get started. First, we start the system, with the command <holdir>/bin/hol. We then "open" the arithmetic theory; this means that all of the ML bindings from the HOL theory of arithmetic are made available at the top level.

> open arithmeticTheory;   ... output elided ...

We now begin the formalization. In order to define the concept of prime number, we first need to define the divisibility relation:

> Definition divides_def: divides a b = ?x. b = a * x
  End
Definition has been stored under "divides_def"
val divides_def = ⊢ ∀a b. divides a b ⇔ ∃x. b = a * x: thm

Note how we are using ASCII notation to input our terms (? is the ASCII way to write the existential quantifier), but the system responds with pleasant Unicode. Unicode characters can also be used in the input. Also note how equality on booleans gets printed as the if-and-only-if arrow, while equality on natural numbers stays as an equality. The underlying constant is the same (equality) (as is implied by the fact that one can use = in both places in the input), but the system tries to be helpful when printing.

The definition is added to the current theory with the name divides_def, and also available as an ML binding with the name divides_def. In the usual way of interacting with HOL, such an ML binding is made for each definition and (useful) proved theorem: the ML environment is thus being used as a convenient place to hold definitions and theorems for later reference in the session. Note that the Definition syntax requires its keywords to be in column zero.

We want to treat divides as a (non-associating) infix:

> set_fixity "divides" (Infix(NONASSOC, 450));
val it = (): unit

Next we define the property of a number being prime: a number $p$ is prime if and only if it is not equal to $1$ and it has no divisors other than $1$ and itself:

> Definition prime_def:
    prime p <=> p <> 1 /\ !x. x divides p ==> (x=1) \/ (x=p)
  End
Definition has been stored under "prime_def"
val prime_def = ⊢ ∀p. prime p ⇔ p ≠ 1 ∧ ∀x. x divides p ⇒ x = 1 ∨ x = p: thm

There is more ASCII syntax to observe here: <> for not-equals, and ! for the universal quantifier.

That concludes the definitions to be made. Now we “just” have to prove that there are infinitely many prime numbers. If we were coming to this problem fresh, then we would have to go through a not-well-understood and often tremendously difficult process of finding the right lemmas required to prove our target theorem.² Fortunately, we are working from an already completed proof and can devote ourselves to the far simpler problem of explaining how to prove the required theorems.

Proof tools. The development will illustrate that there is often more than one way to tackle a HOL proof, even if one has only a single (informal) proof in mind. In this example, we often find proofs by using the rewriter rw to unwind definitions and perform basic simplifications, often reducing a goal to its essence.

> rw;
val it = fn: thm list -> tactic

When rw is applied to a list of theorems, the theorems will be added to HOL's built-in database of useful facts as supplementary rewrite rules. We will see that rw is also somewhat knowledgeable about arithmetic.³ Sometimes simplification with rw proves the goal immediately. Often however, we are left with a goal that requires some study before one realizes what lemmas are needed to conclude the proof. Once these lemmas have been proven, or located in ancestor theories, metis_tac⁴ can be invoked with them, with the expectation that it will find the right instantiations needed to finish the proof. Note that these two operations, simplification and resolution-style automatic proof search, will not suffice to perform all the proofs in this example; in particular, our development will also need case analysis and induction.

Finding theorems. This raises the following question: how does one find the right lemmas and rewrite rules to use? This is quite a problem, especially since the number of ancestor theories, and the theorems in them, is large. There are several possibilities

• The help system can be used to look up definitions and theorems, as well as proof procedures; for example, an invocation of

     help "arithmeticTheory"
  

  will display all the definitions and theorems that have been stored in the theory of arithmetic. However, the complete name of the item being searched for must be known before the help system is useful, so the following two search facilities are often more useful.

• DB.match allows the use of patterns to locate the sought-for theorem. Any stored theorem having an instance of the pattern as a subterm will be returned.

• DB.find will use fragments of names as keys with which to lookup information.

Tactic composition. Once a proof of a proposition has been found, it is customary, although not necessary, to embark on a process of revision, in which the original sequence of tactics is composed into a single tactic. Sometimes the resulting tactic is much shorter, and more aesthetically pleasing in some sense. Some users spend a fair bit of time polishing these tactics, although there doesn't seem much real benefit in doing so, since they are ad hoc proof recipes, one for each theorem. In the following, we will show how this is done in a few cases.

Divisibility

We start by proving a number of theorems about the divides relation. We will see that each of these initial theorems can be proved with a single invocation of metis_tac. Both rw and metis_tac are quite powerful reasoners, and the choice of a reasoner in a particular situation is a matter of experience. The major reason that metis_tac works so well is that divides is defined by means of an existential quantifier, and metis_tac is quite good at automatically instantiating existentials in the course of proof. For a simple example, consider proving $\forall x.\ x\ \mathtt{divides}\ 0$. A new proposition to be proved is entered to the proof manager via "g", which starts a fresh goalstack:

> g `!x. x divides 0`;
val it =
   Proof manager status: 1 proof.
   1. Incomplete goalstack:
        Initial goal:
        ∀x. x divides 0

The proof manager tells us that it has only one proof to manage, and echoes the given goal. Now we expand the definition of divides. Notice that $\alpha$-conversion takes place in order to keep distinct the $x$ of the goal and the $x$ in the definition of divides:

> e (rw[divides_def]);
OK..
1 subgoal:
val it =
   
   ∃x'. x = 0 ∨ x' = 0

It is of course quite easy to instantiate the existential quantifier by hand.

> e (qexists_tac `0`);
OK..
1 subgoal:
val it =
   
   x = 0 ∨ 0 = 0

Then a simplification step finishes the proof.

> e (rw[]);
OK..   ... output elided ...

Goal proved.
⊢ ∃x'. x = 0 ∨ x' = 0
val it =
   Initial goal proved.
   ⊢ ∀x. x divides 0: proof

What just happened here? The application of rw to the goal decomposed it to an empty list of subgoals; in other words the goal was proved by rw. Once a goal has been proved, it is popped off the goalstack, prettyprinted to the output, and the theorem becomes available for use by the level of the stack. When all the sub-goals required by that level are proven, the corresponding goal at that level can be proven too. This ‘unwinding’ process continues until the stack is empty, or until it hits a goal with more than one remaining unproved subgoal. This process may be hard to visualize,⁵ but that doesn't matter, since the goalstack was expressly written to allow the user to ignore such details.

We can sequence tactics with the >> operator (also known as THEN). If our three interactions above are joined together with >> to form a single tactic, we can try the proof again from the beginning (using the restart function) and this time it will take just one step:

> restart();   ... output elided ...

> e (rw[divides_def] >> qexists_tac `0` >> rw[]);
OK..
val it =
   Initial goal proved.
   ⊢ ∀x. x divides 0: proof

We have seen one way to prove the theorem. However, as mentioned earlier, there is another: one can let metis_tac expand the definition of divides and find the required instantiation for x' from the theorem MULT_CLAUSES.⁶

> restart();   ... output elided ...

> e (metis_tac [divides_def, MULT_CLAUSES]);
OK..
metis: r[+0+10]+0+0+0+1+2#
val it =
   Initial goal proved.
   ⊢ ∀x. x divides 0: proof

As it runs, metis_tac prints out some possibly interesting diagnostics. In any case, having done our proof inside the goalstack package, we now want to have access to the theorem value that we have proved. We use the top_thm function to do this, and then use drop to dispose of the stack:

> val DIVIDES_0 = top_thm();
val DIVIDES_0 = ⊢ ∀x. x divides 0: thm
> drop();
OK..
val it = There are currently no proofs.: proofs

We have used metis_tac in this way to prove the following collection of theorems about divides. As mentioned previously, the theorems supplied to metis_tac in the following proofs did not (usually) come from thin air: in most cases some exploratory work with the simplifier (rw) was done to open up definitions and see what lemmas would be required by metis_tac.

We'll assume that the above proofs have been performed, and that the appropriate ML names have been given to all of the theorems. Now we encounter a lemma about divisibility that doesn't succumb to just a single invocation of metis_tac:

Let's see how this is proved. The easiest way to start is to simplify with the definition of divides:

> g `!m n. m divides n ==> m <= n \/ (n = 0)`;   ... output elided ...

> e (rw[divides_def]);
OK..
1 subgoal:
val it =
   
   m ≤ m * x ∨ m * x = 0

This goal is a disappointing one to have the simplifier produce. Both disjuncts look as if they should simplify further: the first looks as if we should be able to divide through by m on both sides of the inequality, and the second looks like something we could attack with the knowledge that one of two factors must be zero if a multiplication equals zero.

The relevant theorems justifying such steps have already been proved in arithmeticTheory; something we can confirm with the generally useful DB.match function

   DB.match : string list -> term
                -> ((string * string) * (thm * class)) list

This function takes a list of theory names, and a pattern, and looks in the list of theories for any theorem, definition, or axiom that has an instance of the pattern as a subterm. If the list of theory names is empty, then all loaded theories are included in the search. Let's look in the theory of arithmetic for the subterm to be rewritten.

> DB.match ["arithmetic"] ``m <= m * x``;
val it =
   [(("arithmetic", "LE_MULT_CANCEL_LBARE"),
     (⊢ (m ≤ m * n ⇔ m = 0 ∨ 0 < n) ∧ (m ≤ n * m ⇔ m = 0 ∨ 0 < n), Thm,
      Located
       {exact = true, linenum = 2042, scriptpath =
        "$(HOLDIR)/src/num/theories/arithmeticScript.sml"}))]:
   public_data list

This is just the theorem we'd like to use. Using DB.match again, you should now try to find the theorem that will simplify the other disjunct. Because both are so generally useful, rw already has both rewrites in its internal database, and all we need to do is rewrite once more to get those rewrites applied:

> e (rw[]);
OK..

Goal proved.
⊢ m ≤ m * x ∨ m * x = 0
val it =
   Initial goal proved.
   ⊢ ∀m n. m divides n ⇒ m ≤ n ∨ n = 0: proof

That was gratifyingly easy! The process of finding the proof has now finished, and all that remains is for the proof to be packaged up into the single tactic we saw above. Rather than use top_thm and the goalstack, we can bypass it and use the Theorem syntax to store the proved theorem for future use. This syntax names the theorem, states the goal and provides the tactic that will prove that goal. It then stores the theorem in the current theory under the given name.

> Theorem DIVIDES_LE:
    !m n. m divides n ==> m <= n \/ (n = 0)
  Proof rw[divides_def] >> rw[]
  QED
val DIVIDES_LE = ⊢ ∀m n. m divides n ⇒ m ≤ n ∨ n = 0: thm

(Note how the statement of the goal is not given with enclosing quotation symbols (the Theorem and Proof lines take on that role). Also, all of the keywords in the Theorem-syntax have to be present starting at column 0 of the input.) Storing theorems in our script record of the session in this style (rather than with the goalstack) results in a more concise script, and also makes it easier to turn our script into a theory file, as we do in Section 4.5.

Divisibility and factorial

The next lemma, DIVIDES_FACT, says that every number greater than $0$ and $\leq n$ divides the factorial of $n$. Factorial is found at arithmeticTheory.FACT and has been defined by primitive recursion:

A polished proof of DIVIDES_FACT is the following⁷:

We will examine this proof in detail, so we should first attempt to understand why the theorem is true. What's the underlying intuition? Suppose $0 < m \leq n$, and so FACT n $= 1 * \cdots * m * \cdots * n$. To show $m\ \mathtt{divides}\ (\mathtt{FACT}\ n)$ means exhibiting a $q$ such that $q * m = \mathtt{FACT}\ n$. Thus $q = \mathtt{FACT}\ n \div m$. If we were to take this approach to the proof, we would end up having to find and apply lemmas about $\div$. This seems to take us a little out of our way; isn't there a proof that doesn't use division? Well yes, we can prove the theorem by induction on $n - m$: in the base case, we will have to prove $n\ \mathtt{divides}\ (\mathtt{FACT}\ n)$, which ought to be easy; in the inductive case, the inductive hypothesis seems like it should give us what we need. This strategy for the inductive case is a bit vague, because we are trying to mentally picture a slightly complicated formula, but we can rely on the system to accurately calculate the cases of the induction for us. If the inductive case turns out to be not what we expect, we will have to re-think our approach.

> g `!m n. 0 < m /\ m <= n ==> m divides (FACT n)`;
val it =
   Proof manager status: 2 proofs.
   2. Completed goalstack: ⊢ ∀m n. m divides n ⇒ m ≤ n ∨ n = 0
   
   1. Incomplete goalstack:
        Initial goal:
        ∀m n. 0 < m ∧ m ≤ n ⇒ m divides FACT n

Instead of directly inducting on $n-m$, we will induct on a witness variable, obtained by use of the theorem LESS_EQ_EXISTS.

> LESS_EQ_EXISTS;
val it = ⊢ ∀m n. m ≤ n ⇔ ∃p. n = m + p: thm

Now we want to induct on the $p$ that our theorem says exists. This effectively requires us to prove a slight restatement of the theorem. We might prove the restatement as a separate lemma, but it is probably just as easy to do this inline with the (infix) suffices_by tactic:

> e (`!m p. 0 < m ==> m divides FACT(m + p)`
       suffices_by metis_tac[LESS_EQ_EXISTS]);
OK..
metis: r[+0+7]+0+0+0+0+0+0+2+1#
1 subgoal:
val it =
   
   ∀m p. 0 < m ⇒ m divides FACT (m + p)

The tactic that we provide after the suffices_by checks that the first argument does indeed imply the original goal. If that tactic succeeds (as it does here), we have a new goal to prove. Now we can perform the induction:

> e (Induct_on `p`);
OK..
2 subgoals:
val it =
   
    0.  ∀m. 0 < m ⇒ m divides FACT (m + p)
   ------------------------------------
        ∀m. 0 < m ⇒ m divides FACT (m + SUC p)
   
   ∀m. 0 < m ⇒ m divides FACT (m + 0)

We now have two sub-goals to prove: a base case and a step case. The first goal the system expects us to prove is the lowest one printed (it's closest to the cursor), the base-case. This can obviously be simplified:

> e (rw[]);
OK..
1 subgoal:
val it =
   
    0.  0 < m
   ------------------------------------
        m divides FACT m

Now we can do a case analysis on $m$: if it is $0$, we have a trivial goal; if it is a successor, then we can use the definition of FACT and the theorems DIVIDES_RMUL and DIVIDES_REFL.

> e (Cases_on `m`);
OK..
2 subgoals:
val it =
   
    0.  0 < SUC n
   ------------------------------------
        SUC n divides FACT (SUC n)
   
    0.  0 < 0
   ------------------------------------
        0 divides FACT 0

Here the first sub-goal goal has an assumption that is false. We can demonstrate this to the system by using the DECIDE function to prove a simple fact about arithmetic (namely, that no number $x$ is less than itself), and then passing the resulting theorem to METIS_TAC, which can combine this with the contradictory assumption.

> e (metis_tac [DECIDE ``!x. ~(x < x)``]);
OK..
metis: r[+0+4]#

Goal proved.
 [.] ⊢ 0 divides FACT 0

Remaining subgoals:
val it =
   
    0.  0 < SUC n
   ------------------------------------
        SUC n divides FACT (SUC n)

Alternatively, we could trust that HOL's existing theories somewhere include the fact that less-then is irreflexive, find that theorem using DB.match (using the pattern x < x), and then quote that theorem-name to metis_tac.

Another alternative would be to apply the simplifier directly to the sub-goal's assumptions. Certainly, the simplifier has already been primed with the irreflexivity of less-than, so this seems natural. This can be done with the fs tactic:

> b();   ... output elided ...
> e (fs[]);
OK..

Goal proved.
 [.] ⊢ 0 divides FACT 0

Remaining subgoals:
val it =
   
    0.  0 < SUC n
   ------------------------------------
        SUC n divides FACT (SUC n)

Using the theorems identified above the remaining sub-goal can be proved with the simplifier rw.

> e (rw [FACT, DIVIDES_LMUL, DIVIDES_REFL]);
OK..   ... output elided ...

Goal proved.
⊢ ∀m. 0 < m ⇒ m divides FACT (m + 0)

Remaining subgoals:
val it =
   
    0.  ∀m. 0 < m ⇒ m divides FACT (m + p)
   ------------------------------------
        ∀m. 0 < m ⇒ m divides FACT (m + SUC p)

Now we have finished the base case of the induction and can move to the step case. An obvious thing to try is simplification with the definitions of addition and factorial:

> e (rw [FACT, ADD_CLAUSES]);
OK..
1 subgoal:
val it =
   
    0.  ∀m. 0 < m ⇒ m divides FACT (m + p)
    1.  0 < m
   ------------------------------------
        m divides FACT (m + p) * SUC (m + p)

And now, by DIVIDES_RMUL and the inductive hypothesis, we are done:

> e (rw[DIVIDES_RMUL]);
OK..   ... output elided ...

Goal proved.
⊢ ∀m p. 0 < m ⇒ m divides FACT (m + p)
val it =
   Initial goal proved.
   ⊢ ∀m n. 0 < m ∧ m ≤ n ⇒ m divides FACT n: proof

We have finished the search for the proof, and now turn to the task of making a single tactic out of the sequence of tactic invocations we have just made. We assume that the sequence of invocations has been kept track of in a file or a text editor buffer. We would thus have something like the following:

e (`!m p. 0 < m ==> m divides FACT (m + p)`
     suffices_by metis_tac[LESS_EQ_EXISTS]);
e (Induct_on `p`);
(*1*)
e (rw[]);
e (Cases_on `m`);
(*1.1*)
e (fs[]);
(*1.2*)
e (rw[FACT, DIVIDES_LMUL, DIVIDES_REFL]);
(*2*)
e (rw[FACT, ADD_CLAUSES]);
e (rw[DIVIDES_RMUL]);

We have added a numbering scheme to keep track of the branches in the proof. We can stitch the above together directly into the following compound tactic:

`!m p.  0 < m ==> m divides FACT (m + p)`
  suffices_by metis_tac[LESS_EQ_EXISTS] >>
Induct_on `p`
>- (
  rw[] >> Cases_on `m`
  >- fs[]
  >- rw[FACT, DIVIDES_LMUL, DIVIDES_REFL])
>- (rw[FACT, ADD_CLAUSES] >> rw[DIVIDES_RMUL])

The above uses two operators to compose tactics. The >> operator sequentially composes two tactics. The >- is used to create a subproof for the first goal in situations with multiple subgoals. Here, the tactic after the first top-level >- proves the base case, and the second proves the inductive case. Such subproofs can be nested, as illustrated in the base case.

This can be tested to see that we have made no errors:

> restart();   ... output elided ...
> e (`!m p.  0 < m ==> m divides FACT (m + p)`
               suffices_by metis_tac[LESS_EQ_EXISTS] >>
             Induct_on `p`
             >- (
               rw[] >> Cases_on `m`
               >- fs[]
               >- rw[FACT, DIVIDES_LMUL, DIVIDES_REFL])
             >- (rw[FACT, ADD_CLAUSES] >> rw[DIVIDES_RMUL])
     );
OK..
metis: r[+0+7]+0+0+0+0+0+0+2+1#
val it =
   Initial goal proved.
   ⊢ ∀m n. 0 < m ∧ m ≤ n ⇒ m divides FACT n: proof

For many users, this would be the end of dealing with this proof: the tactic can now be packaged into a Theorem declaration, and that would be the end of it. However, another user might notice that this tactic could be shortened.

One obvious step would be to merge the two successive invocations of the simplifier in the step case:

`!m p.  0 < m ==> m divides FACT (m + p)`
  suffices_by metis_tac[LESS_EQ_EXISTS] >>
Induct_on `p`
>- (
  rw[] >> Cases_on `m`
  >- fs[]
  >- rw[FACT, DIVIDES_LMUL, DIVIDES_REFL])
>- (rw[FACT, ADD_CLAUSES, DIVIDES_RMUL])

Now we'll make the occasionally dangerous assumption that the simplifications of the step case won't interfere with what is happening in the base case, and move the step case's tactic to precede the first >-, using >>. When the Induct tactic generates two sub-goals, the step case's simplification will be applied to both of them:

> restart();   ... output elided ...
> e (`!m p.  0 < m ==> m divides FACT (m + p)`
        suffices_by metis_tac[LESS_EQ_EXISTS] >>
     Induct_on `p` >> rw[FACT, ADD_CLAUSES, DIVIDES_RMUL]);
OK..
metis: r[+0+7]+0+0+0+0+0+0+2+1#
1 subgoal:
val it =
   
    0.  0 < m
   ------------------------------------
        m divides FACT m

The step case has been dealt with, and as we hoped the base case has not been changed at all. This means that our tactic can become

`!m p.  0 < m ==> m divides FACT (m + p)`
  suffices_by metis_tac[LESS_EQ_EXISTS] >>
Induct_on `p` >>
rw[FACT, ADD_CLAUSES,DIVIDES_RMUL] >>
(* base case only remains *)
Cases_on `m`
>- fs[]
>- rw[FACT,DIVIDES_LMUL,DIVIDES_REFL]

In the base case, we have two invocations of the simplifier under the case-split on m. In general, the two different simplifier invocations do slightly different things in addition to simplifying the conclusion of the goal:

• rw strips apart the propositional structure of the goal, and eliminates equalities from the assumptions
• fs simplifies the assumptions as well as the conclusion

However, in this case the goal where we used rw did not include any propositional structure to strip apart, and so we can be confident that using fs in the same place would also work. Thus, we can merge the two sub-cases of the base-case into a single invocation of fs:

`!m p.  0 < m ==> m divides FACT (m + p)`
  suffices_by metis_tac[LESS_EQ_EXISTS] >>
Induct_on `p` >>
rw[FACT, ADD_CLAUSES,DIVIDES_RMUL] >>
Cases_on `m` >>
fs[FACT,DIVIDES_LMUL,DIVIDES_REFL]

We have now finished our exercise in tactic revision. Certainly, it would be hard to foresee that this final tactic would prove the goal; the lemmas passed to our invocations of the simplifier, and the final structure of the tactic have been found by an incremental process of revision.

Divisibility and factorial (again!)

In the previous proof, we made an initial simplification step in order to expose a variable upon which to induct. However, the proof is really by induction on $n - m$. Can we express this directly? The answer is a qualified yes: the induction can be naturally stated, but it leads to somewhat less natural goals.

> restart();   ... output elided ...
> e (Induct_on `n - m`);
OK..
2 subgoals:
val it =
   
    0.  ∀n m. v = n − m ⇒ 0 < m ∧ m ≤ n ⇒ m divides FACT n
   ------------------------------------
        ∀n m. SUC v = n − m ⇒ 0 < m ∧ m ≤ n ⇒ m divides FACT n
   
   ∀n m. 0 = n − m ⇒ 0 < m ∧ m ≤ n ⇒ m divides FACT n

This is slighly hard to read, so we sequence a call to the simplifier to strip both arms of the proof. As before, use of >> ensures that the tactic gets applied in both branches of the induction. (We might also use rpt strip_tac if we didn't want the simplification to happen.)

> b();   ... output elided ...
> e (Induct_on `n - m` >> rw[]);
OK..
2 subgoals:
val it =
   
    0.  ∀n m. v = n − m ⇒ 0 < m ∧ m ≤ n ⇒ m divides FACT n
    1.  SUC v = n − m
    2.  0 < m
   ------------------------------------
        m divides FACT n
   
    0.  n ≤ m
    1.  0 < m
    2.  m ≤ n
   ------------------------------------
        m divides FACT n

Looking at the first goal, we can see (by the anti-symmetry of $\le$) that $m = n$. We can prove this fact, using rw and add it to the hypotheses by use of the infix operator "by":

> e (`m = n` by rw[]);
OK..
1 subgoal:
val it =
   
    0.  n ≤ m
    1.  0 < m
    2.  m ≤ n
    3.  m = n
   ------------------------------------
        m divides FACT n

We can now use simplification again to propagate the newly derived equality throughout the goal.

> e (rw[]);
OK..
1 subgoal:
val it =
   
    0.  m ≤ m
    1.  0 < m
    2.  m ≤ m
   ------------------------------------
        m divides FACT m

At this point in the previous proof we did a case analysis on $m$. However, we already have the hypothesis that $m$ is positive (along with two other now useless hypotheses). Thus we know that $m$ is the successor of some number $k$. We might wish to assert this fact with an invocation of "by" as follows:

   `?k. m = SUC k` by <tactic>

But what is the tactic? If we try rw, it will fail since the embedded arithmetic decision procedure doesn't handle existential statements very well. What to do?

In fact, that earlier case analysis will again do the job: but now we hide it away so that it is only used to prove this sub-goal. When we execute Cases_on `m`, we will get a case where m has been substituted out for 0. This case will be contradictory given that we already have an assumption 0 < m, and we can again use fs. In the other case, there will be an assumption that m is some successor value, and this will make it easy for the simplifier to prove the goal.

Thus:

> e (`?k. m = SUC k` by (Cases_on `m` >> fs[]));
OK..
1 subgoal:
val it =
   
    0.  m ≤ m
    1.  0 < m
    2.  m ≤ m
    3.  m = SUC k
   ------------------------------------
        m divides FACT m

Now the tactic we used before can finish this off:

> e (fs[FACT, DIVIDES_LMUL, DIVIDES_REFL]);
OK..   ... output elided ...

Goal proved.
 [...] ⊢ m divides FACT n

Remaining subgoals:
val it =
   
    0.  ∀n m. v = n − m ⇒ 0 < m ∧ m ≤ n ⇒ m divides FACT n
    1.  SUC v = n − m
    2.  0 < m
   ------------------------------------
        m divides FACT n

That takes care of the base case. For the induction step, things look a bit more difficult than in the earlier proof. However, we can make progress by realizing that the hypotheses imply that $0 < n$ and so we can transform $n$ into a successor, thus enabling the unfolding of FACT, as in the previous proof:

> e (`0 < n` by rw[] >> `?k. n = SUC k` by (Cases_on `n` >> fs[]));
OK..
1 subgoal:
val it =
   
    0.  ∀n m. v = n − m ⇒ 0 < m ∧ m ≤ n ⇒ m divides FACT n
    1.  SUC v = n − m
    2.  0 < m
    3.  0 < n
    4.  n = SUC k
   ------------------------------------
        m divides FACT n

The proof now finishes in much the same manner as the previous one:

> e (rw [FACT, DIVIDES_RMUL]);
OK..   ... output elided ...

Goal proved.
 [...] ⊢ m divides FACT n
val it =
   Initial goal proved.
   ⊢ ∀m n. 0 < m ∧ m ≤ n ⇒ m divides FACT n: proof

We leave the details of stitching the proof together to the interested reader.

Primality

Now we move on to establish some facts about the primality of the first few numbers: $0$ and $1$ are not prime, but $2$ is. Also, all primes are positive. These are all quite simple to prove.

Existence of prime factors

Now we are in position to prove a more substantial lemma: every number other than $1$ has a prime factor. The proof proceeds by a complete induction on $n$. Complete induction is necessary since a prime factor won't be the predecessor. After induction, the proof splits into cases on whether $n$ is prime or not. The first case ($n$ is prime) is trivial. In the second case, there must be an $x$ that divides $n$, and $x$ is not $1$ or $n$. By DIVIDES_LE, $n=0$ or $x \leq n$. If $n=0$, then $2$ is a prime that divides $0$. On the other hand, if $x \leq n$, there are two cases: if $x < n$ then we can use the inductive hypothesis and by transitivity of divides we are done; otherwise, $x=n$ and then we have a contradiction with the fact that $x$ is not 1 or $n$. The polished tactic is the following:

We start by invoking complete induction. This gives us an inductive hypothesis that holds at every number $m$ strictly smaller than $n$:

> g `!n. n <> 1 ==> ?p. prime p /\ p divides n`;
val it =
   Proof manager status: 1 proof.
   1. Incomplete goalstack:
        Initial goal:
        ∀n. n ≠ 1 ⇒ ∃p. prime p ∧ p divides n

> e (completeInduct_on `n`);
OK..
1 subgoal:
val it =
   
    0.  ∀m. m < n ⇒ m ≠ 1 ⇒ ∃p. prime p ∧ p divides m
   ------------------------------------
        n ≠ 1 ⇒ ∃p. prime p ∧ p divides n

We can move the antecedent to the hypotheses and make our case split. Notice that the term given to Cases_on need not occur in the goal:

> e (rw[] >> Cases_on `prime n`);
OK..
2 subgoals:
val it =
   
    0.  ∀m. m < n ⇒ m ≠ 1 ⇒ ∃p. prime p ∧ p divides m
    1.  n ≠ 1
    2.  ¬prime n
   ------------------------------------
        ∃p. prime p ∧ p divides n
   
    0.  ∀m. m < n ⇒ m ≠ 1 ⇒ ∃p. prime p ∧ p divides m
    1.  n ≠ 1
    2.  prime n
   ------------------------------------
        ∃p. prime p ∧ p divides n

As mentioned, the first case is proved with the reflexivity of divisibility:

> e (metis_tac [DIVIDES_REFL]);   ... output elided ...

In the second case, we can get a divisor of $n$ that isn't $1$ or $n$ (since $n$ is not prime):

> e (`?x. x divides n /\ x<>1 /\ x<>n` by metis_tac [prime_def]);
OK..
metis: r[+0+11]+0+0+0+0+0+0+1+1+1+1+0+1+1#
1 subgoal:
val it =
   
    0.  ∀m. m < n ⇒ m ≠ 1 ⇒ ∃p. prime p ∧ p divides m
    1.  n ≠ 1
    2.  ¬prime n
    3.  x divides n
    4.  x ≠ 1
    5.  x ≠ n
   ------------------------------------
        ∃p. prime p ∧ p divides n

At this point, the polished tactic simply invokes metis_tac with a collection of theorems. We will attempt a more detailed exposition. Given the hypotheses, and by DIVIDES_LE, we can assert $x < n \lor n = 0$ and thus split the proof into two cases:

> e (`x < n \/ (n=0)` by metis_tac [DIVIDES_LE,LESS_OR_EQ]);
OK..
metis: r[+0+14]+0+0+0+0+0+0+0+0+0+0+1+0+1#
2 subgoals:
val it =
   
    0.  ∀m. m < n ⇒ m ≠ 1 ⇒ ∃p. prime p ∧ p divides m
    1.  n ≠ 1
    2.  ¬prime n
    3.  x divides n
    4.  x ≠ 1
    5.  x ≠ n
    6.  n = 0
   ------------------------------------
        ∃p. prime p ∧ p divides n
   
    0.  ∀m. m < n ⇒ m ≠ 1 ⇒ ∃p. prime p ∧ p divides m
    1.  n ≠ 1
    2.  ¬prime n
    3.  x divides n
    4.  x ≠ 1
    5.  x ≠ n
    6.  x < n
   ------------------------------------
        ∃p. prime p ∧ p divides n

In the first subgoal, we can see that the antecedents of the inductive hypothesis are met and so $x$ has a prime divisor. We can then use the transitivity of divisibility to get the fact that this divisor of $x$ is also a divisor of $n$, thus finishing this branch of the proof:

> e (metis_tac [DIVIDES_TRANS]);
OK..
metis: r[+0+11]+0+0+0+0+0+0+0+1+0+4+1+0+3+0+2+1#

Goal proved.
 [.......] ⊢ ∃p. prime p ∧ p divides n

Remaining subgoals:
val it =
   
    0.  ∀m. m < n ⇒ m ≠ 1 ⇒ ∃p. prime p ∧ p divides m
    1.  n ≠ 1
    2.  ¬prime n
    3.  x divides n
    4.  x ≠ 1
    5.  x ≠ n
    6.  n = 0
   ------------------------------------
        ∃p. prime p ∧ p divides n

The remaining goal can be clarified by simplification:

> e (rw[]);
OK..
1 subgoal:
val it =
   
    0.  ∀m. m < 0 ⇒ m ≠ 1 ⇒ ∃p. prime p ∧ p divides m
    1.  0 ≠ 1
    2.  ¬prime 0
    3.  x divides 0
    4.  x ≠ 1
    5.  x ≠ 0
   ------------------------------------
        ∃p. prime p ∧ p divides 0

We know that everything divides 0:

> DIVIDES_0;
val it = ⊢ ∀x. x divides 0: thm

So any prime will do for p.

> e (metis_tac [PRIME_2, DIVIDES_0]);
OK..
metis: r[+0+10]#   ... output elided ...

Goal proved.
 [.] ⊢ n ≠ 1 ⇒ ∃p. prime p ∧ p divides n
val it =
   Initial goal proved.
   ⊢ ∀n. n ≠ 1 ⇒ ∃p. prime p ∧ p divides n: proof

Again, work now needs to be done to compose and perhaps polish a single tactic from the individual proof steps, but we will not describe it.⁸ Instead we move forward, because our ultimate goal is in reach.

Euclid's theorem

Theorem. Every number has a prime greater than it.

Informal proof. Suppose the opposite; then there's an $n$ such that all $p$ greater than $n$ are not prime. Consider $\mathtt{FACT}(n) + 1$: it's not equal to 1 so, by PRIME_FACTOR, there's a prime $p$ that divides it. Note that $p$ also divides $\mathtt{FACT}(n)$ because $p \leq n$. By DIVIDES_ADDL, we have $p=1$. But then $p$ is not prime, which is a contradiction. End of proof.

A HOL rendition of the proof may be given as follows:

Let's prise this apart and look at it in some detail. A proof by contradiction can be started by using the bossLib function spose_not_then. With it, one assumes the negation of the current goal and then uses that in an attempt to prove falsity (F). The assumed negation $\neg(\forall n.\ \exists p.\ n < p \land \mathtt{prime}\ p)$ is simplified a bit into $\exists n.\ \forall p.\ n < p\,\Rightarrow\,\neg\,\mathtt{prime}\ p$ and then is passed to the tactic strip_assume_tac. This moves its argument to the assumption list of the goal after eliminating the existential quantification on $n$.

> g `!n. ?p. n < p /\ prime p`;   ... output elided ...

> e (spose_not_then strip_assume_tac);
OK..
1 subgoal:
val it =
   
    0.  ∀p. n < p ⇒ ¬prime p
   ------------------------------------
        F

Thus we have the hypothesis that all $p$ beyond a certain unspecified $n$ are not prime, and our task is to show that this cannot be. At this point we take advantage of Euclid's great inspiration and we build an explicit term from $n$. In the informal proof we are asked to ‘consider’ the term $\mathtt{FACT}\ n + 1$.⁹ This term will have certain properties (i.e., it has a prime factor) that lead to contradiction. Question: how do we ‘consider’ this term in the formal HOL proof? Answer: by instantiating a lemma with it and bringing the lemma into the proof. The lemma and its instantiation are:¹⁰

> PRIME_FACTOR;
val it = ⊢ ∀n. n ≠ 1 ⇒ ∃p. prime p ∧ p divides n: thm

> val th = SPEC ``FACT n + 1`` PRIME_FACTOR;
val th = ⊢ FACT n + 1 ≠ 1 ⇒ ∃p. prime p ∧ p divides FACT n + 1: thm

It is evident that the antecedent of th can be eliminated. In HOL, one could do this in a so-called forward proof style (by proving $\vdash \neg(\mathtt{FACT}\ n + 1 = 1)$ and then applying modus ponens, the result of which can then be used in the proof), or one could bring th into the proof and simplify it in situ. We choose the latter approach.

> e (mp_tac (SPEC ``FACT n + 1`` PRIME_FACTOR));
OK..
1 subgoal:
val it =
   
    0.  ∀p. n < p ⇒ ¬prime p
   ------------------------------------
        (FACT n + 1 ≠ 1 ⇒ ∃p. prime p ∧ p divides FACT n + 1) ⇒ F

The invocation mp_tac ($\vdash M$) applied to a goal $(\Delta, g)$ returns the goal $(\Delta, M \Rightarrow g)$. Now we simplify:

> e (rw[]);
OK..
2 subgoals:
val it =
   
    0.  ∀p. n < p ⇒ ¬prime p
   ------------------------------------
        ¬prime p ∨ ¬(p divides FACT n + 1)
   
    0.  ∀p. n < p ⇒ ¬prime p
   ------------------------------------
        FACT n ≠ 0

We recall that zero is less than every factorial, a fact found in arithmeticTheory under the name FACT_LESS. Thus we can solve the top goal by simplification:

> e (rw[FACT_LESS, DECIDE ``!x. x<>0 <=> 0 < x``]);
OK..

Goal proved.
⊢ FACT n ≠ 0

Remaining subgoals:
val it =
   
    0.  ∀p. n < p ⇒ ¬prime p
   ------------------------------------
        ¬prime p ∨ ¬(p divides FACT n + 1)

Notice the ‘on-the-fly’ use of DECIDE to provide an ad hoc rewrite. Looking at the remaining goal, one might think that our aim, to prove falsity, has been lost. But this is not so: a goal $\neg P \lor \neg Q$ is logically equivalent to $P \Rightarrow Q \Rightarrow \mathtt{F}$. In the following invocation, we use the equality $\vdash A \Rightarrow B = \neg A \lor B$ as a rewrite rule oriented right to left by use of GSYM.¹¹

> IMP_DISJ_THM;
val it = ⊢ ∀A B. A ⇒ B ⇔ ¬A ∨ B: thm

> e (rw[GSYM IMP_DISJ_THM]);
OK..
1 subgoal:
val it =
   
    0.  ∀p. n < p ⇒ ¬prime p
    1.  prime p
   ------------------------------------
        ¬(p divides FACT n + 1)

We can quickly proceed to show that $p\ \mathtt{divides}\ (\mathtt{FACT}\ n)$, so that if it also divides FACT n + 1, then $p$ divides 1, meaning that $p = 1$. But then $p$ is not prime, at which point we are done. This can all be packaged into a single invocation of METIS_TAC:

> e (metis_tac [DIVIDES_FACT, DIVIDES_ADDL, DIVIDES_ONE,
                NOT_PRIME_1, NOT_LESS, PRIME_POS]);
OK..
metis: r[+0+12]+0+0+0+0+0+0+0+0+0+0+0+1+1+1+1+1+4#   ... output elided ...

Goal proved.
 [.] ⊢ F
val it =
   Initial goal proved.
   ⊢ ∀n. ∃p. n < p ∧ prime p: proof

Euclid's theorem is now proved, and we can rest. However, this presentation of the final proof will be unsatisfactory to some, because the proof is completely hidden in the invocation of the automated reasoner. Well then, let's try another proof, this time employing the so-called ‘assertional’ style. When used uniformly, this can allow a readable linear presentation that mirrors the informal proof. The following proves Euclid's theorem in the assertional style. We think it is fairly readable, certainly much more so than the standard tactic proof just given.¹²

Turning the script into a theory

Having proved our result, we probably want to package it up in a way that makes it available to future sessions, but which doesn't require us to go all through the theorem-proving effort again. Even having a complete script from which it would be possible to cut-and-paste is an error-prone solution.

In order to do this we need to create a file with the name $x$Script.sml, where $x$ is the name of the theory we wish to export. This file then needs to be compiled. In fact, we really do use the ML compiler, carefully augmented with the appropriate logical context. However, the language accepted by the compiler is not quite the same as that accepted by the interactive system, so we will need to do a little work to massage the original script into the correct form.

We'll give an illustration of converting to a form that can be compiled using the script <holdir>/examples/euclid.sml as our base-line. This file is already close to being in the right form. It has all of the proofs of the theorems in “sewn-up” form so that when run, it does not involve the goal-stack at all. In its given form, it can be run as input to HOL thus:

$ cd examples/
$ ../bin/hol < euclid.sml
  ...

> val EUCLID = |- !n. ?p. n < p /\ prime p : thm
  ...

> val EUCLID_AGAIN = |- !n. ?p. n < p /\ prime p : thm
-

However, we now want to create a euclidTheory that we can load in other interactive sessions. So, our first step is to create a file euclidScript.sml, and to copy the body of euclid.sml into it.

The first non-comment line opens arithmeticTheory. However, when writing for the compiler, we need to explicitly mention the other HOL modules that we depend on. We must add

   open HolKernel boolLib Parse bossLib

The next line that poses a difficulty is

   set_fixity "divides" (Infixr 450);

While it is legitimate to type expressions directly into the interactive system, the compiler requires that every top-level phrase be a declaration. We satisfy this requirement by altering this line into a “do nothing” declaration that does not record the result of the expression:

   val _ = set_fixity "divides" (Infixr 450)

The only extra changes are to bracket the rest of the script text with calls to new_theory and export_theory. So, before the definition of divides, we add:

   val _ = new_theory "euclid";

and at the end of the file:

   val _ = export_theory();

Now, we can compile the script we have created using the Holmake tool. To keep things a little tidier, we first move our script into a new directory.

$ mkdir euclid
$ mv euclidScript.sml euclid
$ cd euclid
$ ../../bin/Holmake
Analysing euclidScript.sml
Trying to create directory .HOLMK for dependency files
Compiling euclidScript.sml
Linking euclidScript.uo to produce theory-builder executable
<<HOL message: Created theory "euclid".>>
Definition has been stored under "divides_def".
Definition has been stored under "prime_def".
Meson search level: .....
Meson search level: .................
 ...
Exporting theory "euclid" ... done.
Analysing euclidTheory.sml
Analysing euclidTheory.sig
Compiling euclidTheory.sig
Compiling euclidTheory.sml

Now we have created four new files: various forms of euclidTheory with four different suffixes (three of which are hidden in the .holobjs directory). Only euclidTheory.sig is really suitable for human consumption, and this is put into the same directory as the euclidScript.sml file. While still in the euclid directory that we created, we can demonstrate:

$ ../../bin/hol
[...]

[closing file "/local/scratch/mn200/Work/hol98/tools/end-init-boss.sml"]
- load "euclidTheory";
> val it = () : unit
- open euclidTheory;
> type thm = thm
  val DIVIDES_TRANS =
    |- !a b c. a divides b /\ b divides c ==> a divides c
    : thm
  ...
  val DIVIDES_REFL = |- !x. x divides x : thm
  val DIVIDES_0 = |- !x. x divides 0 : thm

Summary

The reader has now seen an interesting theorem proved, in great detail, in HOL. The discussion illustrated the high-level tools provided in bossLib and touched on issues including tool selection, undo, ‘tactic polishing’, exploratory simplification, and the ‘forking-off’ of new proof attempts. We also attempted to give a flavour of the thought processes a user would employ. Following is a more-or-less random collection of other observations.

• Even though the proof of Euclid's theorem is short and easy to understand when presented informally, a perhaps surprising amount of support development was required to set the stage for Euclid's classic argument.

• The proof support offered by bossLib (rw, metis_tac, DECIDE, Cases_on, Induct_on, and the "by" construct) was nearly complete for this example: it was rarely necessary to resort to lower-level tactics.

• Simplification is a workhorse tactic; even when an automated reasoner such as metis_tac is used, its application has often been set up by some exploratory simplifications. It therefore pays to become familiar with the strengths and weaknesses of the simplifier.

• A common problem with interactive proof systems is dealing with hypotheses. Often metis_tac and the "by" construct allow the use of hypotheses without directly resorting to indexing into them (or naming them, which amounts to the same thing). This is desirable, since the hypotheses are notionally a set, and moreover, experience has shown that profligate indexing into hypotheses results in hard-to-maintain proof scripts.

  We also found that we could directly simplify in the assumptions by using the fs tactic. Nonetheless, it can be clumsy to work with a large set of hypotheses, in which case the following approaches may be useful.

  One can directly refer to hypotheses by using UNDISCH_TAC (makes the designated hypothesis the antecedent to the goal), ASSUM_LIST (gives the entire hypothesis list to a tactic), pop_assum (gives the top hypothesis to a tactic), and qpat_assum (gives the first matching hypothesis to a tactic). (See the REFERENCE for further details on all of these.) The numbers attached to hypotheses by the proof manager could likely be used to access hypotheses (it would be quite simple to write such a tactic). However, starting a new proof is sometimes the most clarifying thing to do.

  In some cases, it is useful to be able to delete a hypothesis. This can be accomplished by passing the hypothesis to a tactic that ignores it. For example, to discard the top hypothesis, one could invoke pop_assum kall_tac.

• In the example, we didn't use the more advanced features of bossLib, largely because they do not, as yet, provide much more functionality than the simple sequencing of simplification, decision procedures, and automated first order reasoning. The >> tactical has thus served as an adequate replacement. In the future, these entrypoints should become more powerful.

• It is almost always necessary to have an idea of the informal proof in order to be successful when doing a formal proof. However, all too often the following strategy is adopted by novices: (1) rewrite the goal with a few relevant definitions, and then (2) rely on the syntax of the resulting goal to guide subsequent tactic selection. Such an approach constitutes a clear case of the tail wagging the dog, and is a poor strategy to adopt. Insight into the high-level structure of the proof is one of the most important factors in successful verification exercises.

  The author has noticed that many of the most successful verification experts work using a sheet of paper to keep track of the main steps that need to be made. Perhaps looking away to the paper helps break the mesmerizing effect of the computer screen.

  On the other hand, one of the advantages of having a mechanized logic is that the machine can be used as a formal expression calculator, and thus the user can use it to quickly and accurately explore various proof possibilities.

• High powered tools like metis_tac, and rw are the principal way of advancing a proof in bossLib. In many cases, they do exactly what is desired, or even manage to surprise the user with their power. In the formalization of Euclid's theorem, the tools performed fairly well. However, sometimes they are overly aggressive, or they simply flounder. In such cases, more specialized proof tools need to be used, or even written, and hence the support underlying bossLib must eventually be learned.

• Having a good knowledge of the available lemmas, and where they are located, is an essential part of being successful. Often powerful tools can replace lemmas in a restricted domain, but in general, one has to know what has already been proved. We have found that the entrypoints in DB help in quickly finding lemmas.

1. The proofs discussed below may be found in examples/euclid.sml of the HOL distribution. ↩

2. This is of course a general problem in doing any kind of proof. ↩

3. Linear arithmetic especially: purely universal formulas involving the operators SUC, $+$, $-$, numeric literals, $<$, $\leq$, $>$, $\geq$, $=$, and multiplication by numeric literals. ↩

4. The metis_tac tactic performs resolution-style first-order proof search. ↩

5. Perhaps since we have used a stack to implement what is notionally a tree! ↩

6. You might like to try typing MULT_CLAUSES into the interactive loop to see exactly what it states. ↩

7. This and subsequent proofs use the theorems proved on page \pageref{euclid:extra-proofs}, which were added to the ML environment after being proved. ↩

8. Indeed, the tactic can be simplified into complete induction followed by an invocation of METIS_TAC with suitable lemmas. ↩

9. The HOL parser thinks $\mathtt{FACT}\ n + 1$ is equivalent to $(\mathtt{FACT}\ n) + 1$. ↩

10. The function SPEC implements the rule of universal specialization. ↩

11. Loosely speaking, GSYM swaps the left and right hand sides of any equations it finds. ↩

12. Note that CCONTR_TAC, which is used to start the proof, initiates a proof by contradiction by negating the goal and placing it on the hypotheses, leaving F as the new goal. ↩