Filter
Top Products
Chapter 10
Tactics
Rules give a way of performing proofs in a step-by-step, forward manner. However
it’s often more convenient to prove theorems in a backwards fashion, starting with
the goal and reducing it to various subgoals until these can be solved. The tactic
mechanism of HOL Light allows one to tackle proofs in a mixture of forward and
backward steps. The user starts with a goal, which is roughly speaking, the theorem
(sequent) that is desired: a list of assumptions and a conclusion.
A tactic takes a goal and reduces it to a list of subgoals. But it also keeps track of
how to construct a proof of the main goal if the user succeeds in proving the subgoal;
this is simply an ML function. So the user can keep applying tactics, and the forward
proof is reconstructed by HOL. It’s rather as if the machine automatically reverses
the user’s proof and converts it to the standard primitive inferences. The user can
perform the proof via a mixture of forward and backward steps, as desired.
10.1 The goalstack
Proofs can be discovered interactively using the goal stack. This allows tactic steps
to be performed, and if necessary retracted and corrected. The user sets up an
initial goal using g, e.g.
#g ‘p /\ q ==> p‘;;
it : goalstack = 1 subgoal (1 total)
‘p /\ q ==> p‘
It is then possible to apply a tactic to the current goal, e.g.
#e DISCH_TAC;;
it : goalstack = 1 subgoal (1 total)
‘p‘
0 [‘p /\ q‘]
If the user makes a mistake, b() backs up to the previous level. The goal can
be finished here by rewriting:
#e(ASM_REWRITE_TAC[]);;
it : goalstack = No subgoals
There are no subgoals; the proof is finished. To make HOL generate the desired
theorem, use top thm():
81