Chapter 7: Tactics
A deduction rule is a link between some (unique) formula, that we call
the conclusion and (several) formulæ that we call the premises. Indeed, a deduction rule can be read in two ways. The first
one has the shape: ``if I know this and this then I can deduce
this''. For instance, if I have a proof of A and a proof of B
then I have a proof of A Ù B. This is forward reasoning from
premises to conclusion. The other way says: ``to prove this I
have to prove this and this''. For instance, to prove A Ù B, I
have to prove A and I have to prove B. This is backward reasoning
which proceeds from conclusion to premises. We say that the conclusion
is the goal to prove and premises are the
subgoals. The tactics implement backward
reasoning. When applied to a goal, a tactic replaces this goal with
the subgoals it generates. We say that a tactic reduces a goal to its
subgoal(s).
Each (sub)goal is denoted with a number. The current goal is numbered
1. By default, a tactic is applied to the current goal, but one can
address a particular goal in the list by writing n:tactic which
means ``apply tactic tactic to goal number n''.
We can show the list of subgoals by typing Show (see section
6.3.1).
Since not every rule applies to a given statement, every tactic cannot be
used to reduce any goal. In other words, before applying a tactic to a
given goal, the system checks that some preconditions are
satisfied. If it is not the case, the tactic raises an error message.
Tactics are build from tacticals and atomic tactics. There are, at
least, three levels of atomic tactics. The simplest one implements
basic rules of the logical framework. The second level is the one of
derived rules which are built by combination of other
tactics. The third one implements heuristics or decision procedures to
build a complete proof of a goal.