10.2 Tactic Macros
The simplest way to introduce it is to define it as new a tactic macro, as follows:Coq < Tactic Definition DecideEq [$a $b] := Coq < [<:tactic:<Destruct $a;Coq < Destruct $b;Coq < (Left;Reflexivity) Orelse (Right;Discriminate)>>].The general pattern of the proof is abstracted away using the tacticals ``;'' and Orelse, and introducing two parameters for the names of the arguments to be analyzed.
Once defined, this tactic can be called like any other tactic, just supplying the list of terms corresponding to its real arguments. Let us revisit the proof of the former theorems using the new tactic DecideEq:
Coq < Theorem decideBool : (x,y:bool){x=y}+{~x=y}.Coq < DecideEq x y.Coq < Defined.Coq < Theorem decideColor : (c1,c2:Color){c1=c2}+{~c1=c2}.Coq < DecideEq c1 c2.Coq < Defined.In general, the command Tactic Definition associates a name to a parameterized tactic expression, built up from the tactics and tacticals that are already available. The general syntax rule for this command is the following:
| Tactic Definition tactic-name | [$id1... $idn] |
| := [<:tactic:< tactic-expression >>] |
This command provides a quick but also very primitive mechanism for introducing new tactics. It does not support recursive definitions, and the arguments of a tactic macro are restricted to term expressions. Moreover, there is no static checking of the definition other than the syntactical one. Any error in the definition of the tactic ---for instance, a call to an undefined tactic--- will not be noticed until the tactic is called.
Let us illustrate the weakness of this way of introducing new tactics trying to extend our proof procedure to work on a larger class of inductive types. Consider for example the decidability of equality for pairs of booleans and colors:
Coq < Theorem decideBoolXColor : (p1,p2:bool*Color){p1=p2}+{~p1=p2}.The proof still proceeds by a double case analysis, but now the constructors of the type take two arguments. Therefore, the sub-goals that can not be solved by discrimination need further considerations about the equality of such arguments:
Coq < Destruct p1;Coq < Destruct p2; Try (Right;Discriminate);Intros.1 subgoal
p1 : bool*Color
b : bool
c : Color
p2 : bool*Color
b0 : bool
c0 : Color
============================
{(b,c)=(b0,c0)}+{~(b,c)=(b0,c0)}
The half of the disjunction to be chosen depends on whether or not b=b0 and c=c0. These equalities can be decided automatically using the previous lemmas about booleans and colors. If both equalities are satisfied, then it is sufficient to rewrite b into b0 and c into c0, so that the left half of the goal follows by reflexivity. Otherwise, the right half follows by first contraposing the disequality, and then applying the injectiveness of the pairing constructor.
As the cases associated to each argument of the pair are very similar, a tactic macro can be introduced to abstract this part of the proof:
Coq < Hint decideBool decideColor.Coq < Tactic Definition SolveArg [$t1 $t2] := Coq < [<:tactic:<Coq < ElimType {$t1=$t2}+{~$t1=$t2};Coq < [(Intro equality;Rewrite equality;Clear equality) |Coq < (Intro diseq; Right; Red; Intro absurd;Coq < Apply diseq;Injection absurd;Trivial) |Coq < Auto]>>].This tactic is applied to each corresponding pair of arguments of the arguments, until the goal can be solved by reflexivity:
Coq < SolveArg b b0;Coq < SolveArg c c0;Coq < Left; Reflexivity.Coq < Defined.Therefore, a more general strategy for deciding the property (x,y:R){x=y}+{¬ x =y} on R can be sketched as follows:
- Eliminate x and then y.
- Try discrimination to solve those goals where x and y has been introduced by different constructors.
- If x and y have been introduced by the same constructor, then iterate the tactic SolveArg for each pair of arguments.
- Finally, solve the left half of the goal by reflexivity.
The implementation of this stronger proof strategy needs to perform a term decomposition, in order to extract the list of arguments of each constructor. It also requires the introduction of recursively defined tactics, so that the SolveArg can be iterated on the lists of arguments. These features are not supported by the Tactic Definition command. One possibility could be extended this command in order to introduce recursion, general parameter passing, pattern-matching, etc, but this would quickly lead us to introduce the whole Ocaml into Coq(This is historically true. In fact, Ocaml is a direct descendent of ML, a functional programming language conceived language for programming the tactics of the theorem prover LCF.). Instead of doing this, we prefer to give to the user the possibility of writing his/her own tactics directly in Ocaml, and then to link them dynamically with Coq's code. This requires a minimal knowledge about Coq's implementation. The next section provides an overview of Coq's architecture.