Exercise 7: First Proof Steps

Note: This is really just a new version of an exercise page provided by Laboratory for Applied Logic.

HOL can prove a great many things for us automatically, but it can't prove everything. Therefore we are going to have to learn how to do proofs for ourselves.

A Simple Goal

In the last exercise we proved that a CMOS implementation of a NOT gate was correct. This time we will try something a little easier. We begin by setting a suitably easy goal, do this by entering the following to HOL.

g `T /\ (!t. F ==> t)`;

In response to this HOL will reply with the following.

> val it =
    Proof manager status: 1 proof.
    1. Incomplete:
         Initial goal:
         ``T /\ (!t. F ==> t)``
    
    : GoalstackPure.proofs

This tells us that HOL is currently managing one proof attempt, and tells us what remains to be proved for that attempt.

Your task now, and at each step of a proof, is to select a tactic to expand on the current goal. The idea is to choose a tactic which will either solve the goal, or break it down into one or more simpler goals that will be easier for subsequent tactics to solve. The hard part is deciding which tactic to expand. The sad truth here is that the only way to acquire this knowledge is through practice and browsing the documentation. Lets start with the practice.

The goal is a conjunction, that is, something of the form A /\ B. Such a goal can be reduced to the simpler problem of separately proving A and proving B. We can do this by expanding the tactic CONJ_TAC on the goal.

- e CONJ_TAC;
OK..
2 subgoals:
> val it =
    ``!t. F ==> t``
    
    ``T``
    
    : GoalstackPure.goalstack

The output from HOL tells us that we have broken the original goal down into two subgoals, and displays those. We now commence work on the new goals, working our way up from the bottom.

The first goal we tackle is dead easy. We have to prove T, which is an axiom of the logic! The ML identifier TRUTH is bound to the theorem that asserts T holds. (Don't believe me, evaluate TRUTH to see for yourself.) The tactic ACCEPT_TAC theorem will solve the current goal if theorem asserts that it is true. For example, we can solve the current goal as follows.

- e (ACCEPT_TAC TRUTH);
OK..

Goal proved.
|- T

Remaining subgoals:
> val it =
    ``!t. F ==> t``
    
    
    : GoalstackPure.goalstack

HOL informs us that we have solved the current goal and shows us what remains to be proved. Note that the brackets in tactic expansion were necessary, e requires a tactic for its argument and ACCEPT_TAC is not really a tactic; its a function that takes a theorem and returns a tactic.

The remaining goal - that false implies anything - is also an axiom of the HOL logic. The theorem FALSITY encodes the axiom, so you can complete the proof using ACCEPT_TAC again, this time with FALSITY as its argument.

Tactic Descriptions

CONJ_TAC and ACCEPT_TAC are all well and good, but you need a few more tactics in your basic repertoire. You will need to know how to read the HOL documentation to you can expand your knowledge of tactics. Most tactics are described in the following notation.

      goal
================
  goal₁ goal₂ ... goal_n

Each goal is written in the form A ?- t, which expresses a desire to prove the term t under the assumptions A. For example, the manual entry for CONJ_TAC describes the tactic thus.

    A ?- t1 /\ t2
======================  CONJ_TAC
 A ?- t1      A ?- t2

This expresses that we can prove t1 /\ t2 under the assumptions A by proving t1 under the assumptions A and t2 under the assumptions A.

A Fist Full of Tactics

The following tactics are the basics of goal-directed proof in HOL. Read the manual entries for each of them.

GEN_TAC

Used to strip the outermost universal quantification from a goal. Use it when you have a goal of the form `!x. t[x]'.

CONJ_TAC

Used to break a conjunctive goal into two subgoals. Use it when you have a goal of the form `t1 /\ t2'.

DISCH_TAC

Used to strip the antecedent of an implicative goal and add the antecedent to the assumptions. Use it when you have a goal of the form `t1 ==> t2' or `~t' (which is treated as `t ==> F').

STRIP_TAC

• Works like GEN_TAC if the the goal looks like `!x. t[x]'.
• Works like CONJ_TAC if the the goal looks like `t₁ /\ t₂'.
• Works like DISCH_TAC if the the goal looks like `t<sub>1</sub> ==> t<sub>2</sub>' or `~t'.

RES_TAC

Performs modus ponens on the assumptions. Use it when you have assumptions of the form `P' and `P ==> Q', or `P[x]' and `!y. P[y] ==> Q[y]'. RES_TAC treats assumptions for the form `~t' like `t ==> F'.

EQ_TAC

Breaks a boolean equality into two implicative goals. Use EQ_TAC when your goal looks like `t₁ = t₂', where t₁ and t₂ are boolean. If EQ_TAC won't break your goal into two implications, its probably because the equality is not a boolean equality. Check your types.

EXISTS_TAC

Used to provide a witness for an existential goal. The witness is supplied as an argument to the tactic and must be a term of the correct type. Use EXISTS_TAC when your goal has the form: `?x. t[x]'.

REWRITE_TAC

Used to rewrite a goal with a list of theorems and a set of standard rewrite rules. The list of theorems is given as an argument to REWRITE_TAC. There are a number of variations on rewriting. Follow the links at the bottom of the REWRITE_TAC manual page to find out what they are.

Some Example Problems

1. (!x. P(x)) ==> ?y. P(y)

   To prove this goal, you might want to use ASM_REWRITE_TAC. Do you need to use EXISTS_TAC?

2. P(x) ==> ?y. P(y)

   How does this goal differ from the one above? Do you need to use EXISTS_TAC?

3. (!x. P(x) ==> Q(x)) /\ ~Q(a) ==> ~P(a)

   You need use only two tactics to prove this, though you need them more than once.

4. !a b c. (b = a) /\ (c = b) /\ P(a) ==> P(b) \/ P(c)
   • Could you have made use of REPEAT in your proof?
   • Would the proof had been as easy if the goal had been stated as follows?

     !a b c. (a = b) /\ (b = c) /\ P(a) ==> P(b) \/ P(c)
     

     How could you prove this?
5. (!x. P /\ Q(x)) = P /\ !x. Q(x)

   This proof needs EQ_TAC.

Managing Proofs

By now you should have several (hopefully complete) proofs in the proof manager, like the following:

Proof manager status: 4 proofs.
6. Completed: |- T /\ (!t. F ==> t)
5. Completed: |- (!x. P x) ==> (?y. P y)
4. Completed: |- P x ==> (?y. P y)
3. Completed: |- (!x. P x ==> Q x) /\ ~(Q a) ==> ~(P a)
2. Completed: |- !a b c. (b = a) /\ (c = b) /\ P a ==> P b \/ P c
1. Completed: |- (!x. P /\ Q x) = P /\ (!x. Q x)

Every time you start a new proof, you see all the previous attempted proofs in this session. Use drop() to get rid of the latest proof attempt. If you want to work on another proof, use R n (where n is a number) to Rotate proofs 1 through n to the bottom of the proof stack.