Using Hal


The best thing to do is to read the book, but here are some brief examples which should be enough to let people who already know something about logic and theorem proving to play with the applet.

A simple propositional proof

Hal implements a theorem prover for first order classical logic. You start by saying what it is that you want to prove. For example, to prove one direction of the commutativity of conjunction you would type
goal "P & Q --> Q & P"
Hal responds by reminding you of the top-level goal and showing what subgoals you currently have:
P & Q --> Q & P
 1. empty |- P & Q --> Q & P
You can then do the proof interactively from the bottom up, by repeatedly applying a particular sequent calculus rule to a particular subgoal. In this case, we might proceed as follows:
by (impR 1)
P & Q --> Q & P
 1. P & Q |- Q & P
Here we've applied the implication right rule to subgoal 1, yielding the new subgoal of proving Q & P under the assumption P & Q. Next we apply the conjunction left rule to that subgoal which leaves us having to prove Q & P under the two assumptions P and Q:
by (conjL 1)
P & Q --> Q & P
 1. P, Q |- Q & P
Next we apply the conjunction right rule to that subgoal, yielding two subgoals:
by (conjR 1)
P & Q --> Q & P
 1. P, Q |- Q
 2. P, Q |- R
Both of those are instances of the basic axiom, so we just have to apply that twice:
by (basic 2)
P & Q --> Q & P
 1. P, Q |- Q

by (basic 1)
P & Q --> Q & P
No subgoals left!
When there are no subgoals left, we have proved the theorem.

A proof with quantifiers

Hal can also cope with quantifiers. Here's a simple one:
goal "(ALL x.P(x)) --> P(a)"
(ALL x. P(x)) --> P(a)
 1. empty |- (ALL x. P(x)) --> P(a)

by (impR 1)
(ALL x. P(x)) --> P(a)
 1. ALL x. P(x) |- P(a)

by (allL 1)
(ALL x. P(x)) --> P(a)
 1. P(?_a), ALL x. P(x) |- P(a)

by (unify 1)
(ALL x. P(x)) --> P(a)
No subgoals left!
Note how the left rule for universal quantification introduces a fresh metavariable ?_a. The unify tactic tries to find a substitution for the metavariables which will make the subgoal be an instance of the basic axiom. In this case it succeeds using the substitution which maps ?_a to the ordinary variable a.

A more complicated quantifier proof

The sequent rules for quantifiers include side conditions which induce restrictions on which variables can be free in terms substituted for metavariables. This is demonstrated by the following proof:
goal "EX z. P(z) --> (ALL x. P(x))"
EX z. P(z) --> (ALL x. P(x))
 1. empty |- EX z. P(z) --> (ALL x. P(x))

by (exR 1)
EX z. P(z) --> (ALL x. P(x))
 1. empty
    |- P(?_a) --> (ALL x. P(x))
       EX z. P(z) --> (ALL x. P(x))

by (impR 1)
EX z. P(z) --> (ALL x. P(x))
 1. P(?_a)
    |- ALL x. P(x), EX z. P(z) --> (ALL x. P(x)) 

by (allR 1)
EX z. P(z) --> (ALL x. P(x))
 1. P(?_a)
    |- P(_b), EX z. P(z) --> (ALL x. P(x)) 
_b not in ?_a

by (exR 1)
EX z. P(z) --> (ALL x. P(x))
 1. P(?_a)
    |- P(?_c) --> (ALL x. P(x)), P(_b),
       EX z. P(z) --> (ALL x. P(x))
_b not in ?_a

by (impR 1)
EX z. P(z) --> (ALL x. P(x))
 1. P(?_c), P(?_a)
    |- ALL x. P(x), P(b),
       EX z. P(z) --> (ALL x. P(x))
_b not in ?_a

by (unify 1)
EX z. P(z) --> (ALL x. P(x))
No subgoals left!
One of the interesting features of this proof is the way in which the new variable _b generated by the application of the universal quantification right rule is constrained not to be free in any term which gets substituted for the metavariable ?_a. This restriction is shown under the current set of subgoals and prevents the proof from being finshed off with an application of unify straight after the first application of allR.

Tacticals

Hal also lets you use tacticals: higher-order functions which let you generate new tactics from old. These can significantly shorten proofs. As a silly example, suppose we started off like this:
goal "P --> P & (P & (P & P))"
P --> P & (P & (P & P))
 1. empty |- P --> P & (P & (P & P))

by (impR 1)
P --> P & (P & (P & P))
 1. P |- P & (P & (P & P))
then it's obvious that we'll have to apply conjunction right and the basic axiom several times. Instead of doing that by applying the individual tactics manually, we can use the tacticals repeat and || to produce a new tactic that does the whole thing in one go:
by (repeat ((conjR 1) || (basic 1)))
P --> P & (P & (P & P))
No subgoals left!
The || tactical combines two tactics into the tactic that tries to do the first and, if that fails, then tries to do the second. The repeat tactical takes a single tactic as argument and returns the tactic which repeatedly applies that argument until it fails.

Hal has some useful tactics built from the elementary logical rules using tacticals. These can prove quite a few things automatically and can significantly shorten interactive proofs. The depth tactic, for example, does a depth-first search of the proof tree. This can get stuck down dead-ends, but works quite often:

goal "~ (EX x. ALL Y. J(x,y) <-> ~J(y,y))"
~(EX x. ALL Y. J(x, y) <-> ~J(y, y))
 1. empty 
    |- ~(EX x. ALL Y. J(x, y) <-> ~J(y, y))
by depth
~(EX x. ALL Y. J(x, y) <-> ~J(y, y))
No subgoals left!

Hal applet syntax summary

The Hal applet implements an interpreter for a little combinatory language with base types int, string, unit and tactic. The built-in identifiers are
goal : string -> unit 
Parses its argument as a formula and makes that the current goal.

by : tactic -> unit
Attempts to apply its argument to the current proof state.

all : tactic
no : tactic
The tactics which always fail and succeed, respectively.

conjL, conjR, disjL, disjR, impL, impR, negL, negR, 
iffL, iffR, exL, exR, allL, allR, basic : int -> tactic
Apply the appropriate sequent calculus rule to the numbered subgoal.

safeSteps : int -> tactic
Applies a sequence of `safe' rules to the numbered subgoal.

quant : int -> tactic
Expands quantifiers in numbered subgoal.

depth : tactic
Solves all subgoals by depth-first search (incompletely).

step : int -> tactic
Tries to use safe steps on numbered subgoal, otherwise using 
unification and quantifier expansion.

depthIt : int -> tactic
Solves all subgoals using depth-first iterative deepening with 
increment given as argument. Compared to depth, this is slower
but doesn't get stuck down blind alleys.

--, ||, |@| : tactic * tactic -> tactic (infix)
Sequential composition, committed and non-commited choice of tactics.

try : tactic -> tactic
Attempts to apply its argument.

repeat : tactic -> tactic
Keeps on trying to apply its argument until it fails.

repeatDeterm : tactic -> tactic
Like repeat, but only considers the first result from each iteration.
The syntax of logical formulae should be fairly obvious from the above examples. Just to summarise the ASCII representation of the connectives:
Universal quantification   : ALL x. 
Existential quantification : EX x.
Conjunction                : &
Disjunction                : |
Implication                : -->
Biimplication              : <->
Negation                   : ~


MLj home Comments to: mlj@dcs.ed.ac.uk