The Coq mailing list

[Jasper Stein <jasper AT cs.kun.nl>]

Bas Spitters wrote:
Dear Coq users,

I would like to write my own tactical with a variable number of arguments.
Like Intros: we can use Intros, but also Intros a b.

How would I do this?

A related question.
I would like to make a tactical existing of several words.
Like Unfold: Unfold x in H.

How would I do this?

Thanks in advance,

Bas Spitters

Hi Bas,

I don't know if this is possible using Coq's own tactic language L_tac 
as described in the Reference Manual, but you can try and tap into Coq's 
parser. Using commands like "Print Grammar tactic tactic" one can try to 
figure out the way Coq handles other commands with variable numbers of 
arguments. This may take a bit of work to get some proper understanding, 
but the results can be rewarding,; in fact, I'd be very surprised if one 
cannot program exactly those tactics you speak of. New tactic grammar is 
then entered by "Grammar ..." commands, just as one defines new input 
grammar for terms. But instead of "Grammar constr constr0" and the like, 
one now uses e.g. "Grammar tactic simple_tactic" (which is incidentally 
the grammar parsing the "basic" tactics like Auto, Auto with ..., 
Rewrite, Apply, etc.) The top-level tactic parser is "tactic tactic", 
which invokes other more low-level parsers.

I don't know if they're still on-line, but the Coq v.6.3 reference 
manuals had some more info on this; otherwise, just ask :-)

Oh, and I forget, one also needs to analyse the resulting Abstract 
Syntax Tree (ast) that gets passed to the Coq core. For this I use the 
following thingy:

Grammar vernac vernac :=
 test ["Test" vernac:vernac($a)] -> case [$a] of (JASPER) -> 
[verygood.] esac.

This "Test" vernacular command always fails (because nothing results in 
the ast (JASPER), but the error message one gets is informative enough 
to play around with and analyse, so that one may eventually write one's 
own tactics. (One can also use it to view the passed asts for vernacular 
commands.) Notice one has to somehow enter two (instead of the regular 
one) full stops when one uses Test.

E.g. "Coq < Test Apply Lemma with arg1 arg2..
Toplevel input, characters 0-32
> Test Apply Lemma with arg1 arg2..
> ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: during interpretation of grammar rule test,
 Grammar case failure. The ast
 (SOLVE 1
    (TACTIC
       (Apply (COMMAND (QUALID Lemma))
          (BINDINGS (BINDING (COMMAND (QUALID arg1)))
             (BINDING (COMMAND (QUALID arg2)))))))
 does not match any of the patterns : (JASPER )
 with constraints :
  $a = (SOLVE 1
          (TACTIC
             (Apply (COMMAND (QUALID Lemma))
                (BINDINGS (BINDING (COMMAND (QUALID arg1)))
                   (BINDING (COMMAND (QUALID arg2)))))))

I used this technique myself for writing a tactic "Use" that behaves 
(grammatically speaking) exactly like Apply (i.e. one can say both "Use 
lemma1" and "Use lemma2 with arg1 arg2 arg3"), but if the given lemma 
doesn't apply to the subgoal, it tries one or two other lemma's first, 
then applies the given argument, and does "Auto with algebra" on all 
resulting subgoals.

I suggest playing around with this system for an afternoon or so to find 
out the exact details.

Cheers,

Jasper
--
+++ Out of Cheese error +++ MELON MELON MELON +++ Redo from Start +++