The Coq mailing list

[Qinshi Wang <qinshiw AT cs.princeton.edu>]

Dear Coq community,

This is what I need in my project. I think it could be a problem for many people, not just me.

I have a tactic

Ltac my_tac := first [tac1 | tac2 ... ].

I would like to add tactics to this list, like adding hints to a hint database, like

Hint Extern tac : ...

But auto only succeed when it can solve the goal, while I want it to try the tactics in the list and do not need to solve the goal. It is possible to add tactics by redefine my_tac, as

Ltac my_tac ::= first [tac1 | tac2 | ... | new_tac1].

But it becomes troublesome, if two separated modules M1 and M2 adds their tactics to my_tac and another module M3 requires M1 and M2.

I tried Ltac2, and I find I can create a list of tactic and do first [tac_list]. But when I try to add another tactic to the list by

Ltac2 Set tac_list := new_tac :: tac_list.

it does not work, maybe because Ltac2 does not allow top level side effect. I cannot redefine a top level definition by reading its old value. I am wondering if it is possible to allow top level side effect for Ltac2.

There is another application of maintaining a list of tactics. Before starting the core part of a tactic, it calls a preprocess procedure which is a list of tactics called in sequence, as

Ltac preprocess := tac1; tac2 ...

It is also useful to add tactics to this list.

Thanks,

Qinshi Wang

Princeton University