10.6 A Complete Example
In order to illustrate the implementation of a new tactic, let us come
back to the problem of deciding the equality of two elements of an
inductive type.
10.6.1 Preliminaries
Let us call newtactic the directory that will contain the
implementation of the new tactic. In this directory will lay two
files: a file eqdecide.ml, containing the Objective Caml sources that
implements the tactic, and a Coq file Eqdecide.v, containing
its associated grammar rules and the commands to generate a module
that can be loaded dynamically from Coq's toplevel.
To compile our project, we will create a Makefile with the
command do_Makefile (see section 12.3) :
do_Makefile eqdecide.ml EqDecide.v > Makefile
touch .depend
make depend
We must have kept the sources of Coq somewhere and to set an
environment variable COQTOP that points to that directory.
10.6.2 Implementing the Tactic
The file eqdecide.ml contains the implementation of the
tactic in Objective Caml. Let us recall the main steps of the proof strategy
for deciding the proposition (x,y:R){x=y}+{¬ x=y} on the
inductive type R:
-
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 analyze one by one the corresponding pairs of arguments.
If they are equal, rewrite one into the other. If they are
not, derive a contradiction from the invectiveness of the
constructor.
- Once all the arguments have been rewritten, solve the left half
of the goal by reflexivity.
In the sequel we implement these steps one by one. We start opening
the modules necessary for the implementation of the tactic:
open Names
open Term
open Tactics
open Tacticals
open Hiddentac
open Equality
open Auto
open Pattern
open Names
open Termenv
open Std
open Proof_trees
open Tacmach
The first step of the procedure can be straightforwardly implemented as
follows:
let clear_last = (tclLAST_HYP (fun c -> (clear_one (destVar c))));;
let mkBranches =
(tclTHEN intro
(tclTHEN (tclLAST_HYP h_simplest_elim)
(tclTHEN clear_last
(tclTHEN intros
(tclTHEN (tclLAST_HYP h_simplest_case)
(tclTHEN clear_last
intros))))));;
Notice the use of the tactical tclLAST_HYP, which avoids to
give a (potentially clashing) name to the quantified variables of the
goal when they are introduced.
The second step of the procedure is implemented by the following
tactic:
let solveRightBranch = (tclTHEN simplest_right discrConcl);;
In order to illustrate how the implementation of a tactic can be
hidden, let us do it with the tactic above:
let h_solveRightBranch =
hide_atomic_tactic "solveRightBranch" solveRightBranch
;;
As it was already mentioned in Section 10.3.4, the
combinator hide_atomic_tactic first registers the tactic
solveRightBranch in the table, and returns a tactic which
calls the interpreter with the used to register it. Hence, when the
tactical Info is used, our tactic will just inform that
solveRightBranch was applied, omitting all the details
corresponding to simplest_right and discrConcl.
The third step requires some auxiliary functions for constructing the
type {c1=c2}+{¬ c1=c2} for a given inductive type R and
two constructions c1 and c2, and for generalizing this type over
c1 and c2:
let mmk = make_module_marker ["#Logic.obj";"#Specif.obj"];;
let eqpat = put_pat mmk "eq";;
let sumboolpat = put_pat mmk "sumbool";;
let notpat = put_pat mmk "not";;
let eq = get_pat eqpat;;
let sumbool = get_pat sumboolpat;;
let not = get_pat notpat;;
let mkDecideEqGoal rectype c1 c2 g =
let equality = mkAppL [eq;rectype;c1;c2] in
let disequality = mkAppL [not;equality]
in mkAppL [sumbool;equality;disequality]
;;
let mkGenDecideEqGoal rectype g =
let hypnames = ids_of_sign (pf_hyps g) in
let xname = next_ident_away (id_of_string "x") hypnames
and yname = next_ident_away (id_of_string "y") hypnames
in (mkNamedProd xname rectype
(mkNamedProd yname rectype
(mkDecideEqGoal rectype (mkVar xname) (mkVar yname) g)))
;;
The tactic will depend on the Coqmodules Logic and
Specif, since we use the constants corresponding to
propositional equality (eq), computational disjunction
(sumbool), and logical negation (not), defined in
that modules. This is specified creating the module maker
mmk (cf. Section 10.5.1).
The third step of the procedure can be divided into three sub-steps.
Assume that both x and y have been introduced by the same
constructor. For each corresponding pair of arguments of that
constructor, we have to consider whether they are equal or not. If
they are equal, the following tactic is applied to rewrite one into
the other:
let eqCase tac =
(tclTHEN intro
(tclTHEN (tclLAST_HYP h_rewriteLR)
(tclTHEN clear_last
tac)))
;;
If they are not equal, then the goal is contraposed and a
contradiction is reached form the invectiveness of the constructor:
let diseqCase =
let diseq = (id_of_string "diseq") in
let absurd = (id_of_string "absurd")
in (tclTHEN (intro_using diseq)
(tclTHEN h_simplest_right
(tclTHEN red_in_concl
(tclTHEN (intro_using absurd)
(tclTHEN (h_simplest_apply (mkVar diseq))
(tclTHEN (h_injHyp absurd)
trivial ))))))
;;
In the tactic above we have chosen to name the hypotheses because
they have to be applied later on. This introduces a potential risk
of name clashing if the context already contains other hypotheses
also named ``diseq'' or ``absurd''.
We are now ready to implement the tactic SolveArg. Given the
two arguments a1 and a2 of the constructor, this tactic cuts the
goal with the proposition {a1=a2}+{¬ a1=a2}, and then
applies the tactics above to each of the generated cases. If the
disjunction cannot be solved automatically, it remains as a sub-goal
to be proven.
let solveArg a1 a2 tac g =
let rectype = pf_type_of g a1 in
let decide = mkDecideEqGoal rectype a1 a2 g
in (tclTHENS (h_elimType decide)
[(eqCase tac);diseqCase;default_auto]) g
;;
The following tactic implements the third and fourth steps of the
proof procedure:
let conclpatt = put_pat mmk "{<?1>?2=?3}+{?4}"
;;
let solveLeftBranch rectype g =
let (_::(lhs::(rhs::_))) =
try (dest_somatch (pf_concl g) conclpatt)
with UserError ("somatch",_)-> error "Unexpected conclusion!" in
let nparams = mind_nparams rectype in
let getargs l = snd (chop_list nparams (snd (decomp_app l))) in
let rargs = getargs rhs
and largs = getargs lhs
in List.fold_right2
solveArg largs rargs (tclTHEN h_simplest_left h_reflexivity) g
;;
Notice the use of a pattern to decompose the goal and obtain the
inductive type and the left and right hand sides of the equality. A
certain number of arguments correspond to the general parameters of
the type, and must be skipped over. Once the corresponding list of
arguments rargs and largs have been obtained, the
tactic solveArg is iterated on them, leaving a disjunction
whose left half can be solved by reflexivity.
The following tactic joints together the three steps of the
proof procedure:
let initialpatt = put_pat mmk "(x,y:?1){<?1>x=y}+{~(<?1>x=y)}"
;;
let decideGralEquality g =
let (typ::_) = try (dest_somatch (pf_concl g) initialpatt)
with UserError ("somatch",_) ->
error "The goal does not have the expected form" in
let headtyp = hd_app (pf_compute g typ) in
let rectype = match (kind_of_term headtyp) with
IsMutInd _ -> headtyp
| _ -> error ("This decision procedure only"
" works for inductive objects")
in (tclTHEN mkBranches
(tclORELSE h_solveRightBranch (solveLeftBranch rectype))) g
;;
;;
The tactic above can be specialized in two different ways: either to
decide a particular instance {c1=c2}+{¬ c1=c2} of the
universal quantification; or to eliminate this property and obtain two
subgoals containing the hypotheses c1=c2 and ¬ c1=c2
respectively.
let decideGralEquality =
(tclTHEN mkBranches (tclORELSE h_solveRightBranch solveLeftBranch))
;;
let decideEquality c1 c2 g =
let rectype = pf_type_of g c1 in
let decide = mkGenDecideEqGoal rectype g
in (tclTHENS (cut decide) [default_auto;decideGralEquality]) g
;;
let compare c1 c2 g =
let rectype = pf_type_of g c1 in
let decide = mkDecideEqGoal rectype c1 c2 g
in (tclTHENS (cut decide)
[(tclTHEN intro
(tclTHEN (tclLAST_HYP simplest_case)
clear_last));
decideEquality c1 c2]) g
;;
Next, for each of the tactics that will have an entry in the grammar
we construct the associated dynamic one to be registered in the table
of tactics. This function can be used to overload a tactic name with
several similar tactics. For example, the tactic proving the general
decidability property and the one proving a particular instance for
two terms can be grouped together with the following convention: if
the user provides two terms as arguments, then the specialized tactic
is used; if no argument is provided then the general tactic is invoked.
let dyn_decideEquality args g =
match args with
[(COMMAND com1);(COMMAND com2)] ->
let c1 = pf_constr_of_com g com1
and c2 = pf_constr_of_com g com2
in decideEquality c1 c2 g
| [] -> decideGralEquality g
| _ -> error "Invalid arguments for dynamic tactic"
;;
add_tactic "DecideEquality" dyn_decideEquality
;;
let dyn_compare args g =
match args with
[(COMMAND com1);(COMMAND com2)] ->
let c1 = pf_constr_of_com g com1
and c2 = pf_constr_of_com g com2
in compare c1 c2 g
| _ -> error "Invalid arguments for dynamic tactic"
;;
add_tactic "Compare" tacargs_compare
;;
This completes the implementation of the tactic. We turn now to the
Coqfile Eqdecide.v.
10.6.3 The Grammar Rules
Associated to the implementation of the tactic there is a Coq file
containing the grammar and pretty-printing rules for the new tactic,
and the commands to generate an object module that can be then loaded
dynamically during a Coq session. In order to generate an ML module,
the Coq file must contain a
Declare ML module command for all the Objective Caml files concerning
the implementation of the tactic --in our case there is only one file,
the file eqdecide.ml:
Declare ML Module "eqdecide".
The following grammar and pretty-printing rules are
self-explanatory. We refer the reader to the Section 9.2 for
the details:
Grammar tactic simple_tactic :=
EqDecideRuleG1
[ "Decide" "Equality" comarg($com1) comarg($com2)] ->
[(DecideEquality $com1 $com2)]
| EqDecideRuleG2
[ "Decide" "Equality" ] ->
[(DecideEquality)]
| CompareRule
[ "Compare" comarg($com1) comarg($com2)] ->
[(Compare $com1 $com2)].
Syntax tactic level 0:
EqDecideRulePP1
[(DecideEquality)] ->
["Decide" "Equality"]
| EqDecideRulePP2
[(DecideEquality $com1 $com2)] ->
["Decide" "Equality" $com1 $com2]
| ComparePP
[(Compare $com1 $com2)] ->
["Compare" $com1 $com2].
Important:
The names used to label the abstract syntax tree
in the grammar rules ---in this case ``DecideEquality'' and
``Compare''--- must be the same as the name used to register the
tactic in the tactics table. This is what makes the links between the
input entered by the user and the tactic executed by the interpreter.
10.6.4 Loading the Tactic
Once the module EqDecide.v has been compiled, the tactic can
be dynamically loaded using the Require command.
Coq < Require EqDecide.
[Reinterning EqDecide...done]
Coq < Goal (x,y:nat){x=y}+{~x=y}.
1 subgoal
============================
(x,y:nat){x=y}+{~x=y}
Coq < Decide Equality.
Subtree proved!
The implementation of the tactic can be accessed through the
tactical Info:
Coq < Undo.
1 subgoal
============================
(x,y:nat){x=y}+{~x=y}
Coq < Info Decide Equality.
== Intro x; Elim x.
Clear x; Intro y; Case y.
Clear y; Left; Reflexivity.
Clear y; Intro n; solveRightBranch.
Clear x; Intro n; Intro H; Intro y; Case y.
Clear y; solveRightBranch.
Clear y; Intro n0; ElimType {n=n0}+{~n=n0}.
Intro y; Rewrite y; Clear y; Left; Reflexivity.
Intro diseq; Right; Change (S n)=(S n0)->False; Intro absurd;
Apply diseq; Injection absurd; Intro H0; Exact H0.
Apply H.
Subtree proved!
Remark that the task performed by the tactic solveRightBranch
is not displayed, since we have chosen to hide its implementation.