Filter
Top Products
10.2. BASIC TACTICS 83
10.2 Basic tactics
The most basic tactics correspond to the basic logical derived rules, but working
the other way round. We have seen some of them above. For example, where CONJ
takes two theorems and gives their conjunction, the tactic CONJ TAC breaks down a
conjunctive goal and returns the two subgoals. Similarly DISJ1 TAC reduces a goal
with conclusion p ∨ q to one with conclusion p, i.e. allows the user to decide to
prove the first disjunct. Again, DISCH TAC reverses the effect of the rule DISCH, i.e.
it reduces a goal Γ
?
p ⇒ q to Γ ∪ {p}
?
q.
Tactics are especially useful for using rules like CHOOSE. If one has a theorem
∃x.p, then one can just put p into the assumptions of the goal using CHOOSE TAC.
Thereafter, it is as if one had picked some x such that p holds and can use it to
solve the goal; HOL handles the appropriate application of CHOOSE.
The tactics MP TAC and MATCH MP are a bit tricker to understand, in that it’s
not quite so clear how they amount to reversals of MP and MATCH MP. In fact their
behaviour is quite different, going well beyond one performing matching and one
not. Given a goal with conclusion q and a theorem that after matching is of the
form p ⇒ q, then MATCH MP TAC reduces the goal to p. For example:
#g ‘0 <= SUC n‘;;
it : goalstack = 1 subgoal (1 total)
‘0 <= SUC n‘
#e(MATCH_MP_TAC LT_IMP_LE);;
it : goalstack = 1 subgoal (1 total)
‘0 < SUC n‘
MP TAC, on the other hand, simply places the theorem as an antecedent of the
goal:
#g ‘0 <= SUC n‘;;
it : goalstack = 1 subgoal (1 total)
‘0 <= SUC n‘
#e(MP_TAC LT_IMP_LE);;
it : goalstack = 1 subgoal (1 total)
‘(!m n. m < n ==> m <= n) ==> 0 <= SUC n‘
However this effect can be quite useful, since it’s often more convenient to do
things like rewrite on the conclusion of a goal, rather than the assumptions.
None of the tactics we have considered so far solves goals completely. The most
primitive tactic that does is ACCEPT TAC, which is used with a theorem with the
same conclusion as the goal. A slightly more general version, MATCH ACCEPT TAC,
will do some matching, e.g.
#g ‘x + 1 = 1 + x‘;;
it : goalstack = 1 subgoal (1 total)
‘x + 1 = 1 + x‘
#e(MATCH_ACCEPT_TAC ADD_SYM);;
it : goalstack = No subgoals
Another group of tactics can be created from conversions, using CONV TAC. This
creates a tactic that applies the given conversion to the goal, e.g.