Chapter 7: Tactics

A deduction rule is a link between some (unique) formula, that we call the conclusion and (several) formulae 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 goalto 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:tac which means ``apply tactic tacticto 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. Here is a table of all existing atomic tactics in Coq:

Retrieved by Memoweb from http://pauillac.inria.fr/coq/doc/node.1.2.html at 8/10/98