10.5 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.5.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 Ocaml 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. The following file Makefile is used to automatically update the files in the directory newtactic using the tool make:
#-------------------------------------------------------
# To be filled in:
#COQTOP= <Coq's home directory>
#COQBIN= <Coq's bin directory>
ZLIBS= -I $(COQTOP)/src/lib/util -I $(COQTOP)/src/meta \
-I $(COQTOP)/src/constr -I $(COQTOP)/src/typing \
-I $(COQTOP)/src/proofs -I $(COQTOP)/src/tactics \
-I $(COQTOP)/src/parsing -I $(COQTOP)/tactics
COQC=$(COQBIN)/coqc -I $(ZLIBS)
CAMLDEP=$(COQBIN)/coqdep -c
objects = eqdecide.cmo
vofiles = EqDecide.vo
byte: $(objects) $(vofiles)
ALLFILES=$(objects) $(objects:.cmo=.cmi) $(vofiles)
.mli.cmi:
ocamlc -c $(ZLIBS) $<
.ml.cmo:
ocamlc -c $(ZLIBS) $<
.ml.cmx:
ocamlopt -c $(ZLIBS) $<
.v.vo:
$(COQC) $*
clean:
rm -f *.cm* *.o *.v?
depend:
$(CAMLDEP) $(ZLIBS) *.ml *.mli *.v > .depend
include .depend
#-------------------------------------------------------
10.5.2 Implementing the Tactic
The file eqdecide.ml contains the implementation of the tactic in Ocaml. 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 mkDecideEqGoal rectype c1 c2 g =
let eq = pf_parse_const g "eq"
and sumbool = pf_parse_const g "sumbool"
and not = pf_parse_const g "not" in
let equality = mkAppL [eq;rectype;c1;c2] in
let disequality = mkAppL [not;equality]
in mkAppL [sumbool;equality;disequality]
;;
let mkGenDecideEqGoal rectype g =
let xname = id_of_string "x"
and yname = id_of_string "y"
in (mkNamedProd xname rectype
(mkNamedProd yname rectype
(mkDecideEqGoal rectype (mkVar xname) (mkVar yname) g)));;
The tactic will depend on the initial context of Coq, since we assume that the constants corresponding to propositional equality, computational disjunction and logical negation are already present in the context.
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 solveLeftBranch g =
let conclpatt = put_pat mmk "{<?1>?2=?3}+{?4}" in
let (typ::(lhs::(rhs::_))) =
try (dest_somatch (pf_concl g) conclpatt)
with UserError ("somatch",_)-> error "Unexpected conclusion!" in
let headtyp = hd_app typ in
let nparams = mind_nparams headtyp 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 decideGralEquality = (tclTHEN mkBranches (tclORELSE h_solveRightBranch solveLeftBranch)) ;;
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.5.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 Ocaml 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.5.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]
[Loading ML file eqdecide.cmo ...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; Trivial.
Apply H.
Subtree proved!
Remark that the task performed by the tactic solveRightBranch is not displayed, since we have chosen to hide its implementation.