The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Tactic notations can be rebound while making use of the old value.  For example,

Ltac a := pose 1 as a.                                                                                                                      

Tactic Notation "nuke" := a.                                                                                                                

Ltac b := pose 2 as b.                                                                                                                      

Tactic Notation "nuke" := (nuke; b).

(As an aside, I have not figured out how to print the script of a tactic notation.  Can someone tell me how to do this?)

There is not currently a notion of a database of tactics, other than those of auto or rewrite, so you'd have to write an OCaml plugin if you wanted to use that path.  However, I vaguely recall this being mentioned on coq-club in the past, and that there might be such custom databases in future versions of Coq.  Someone more knowledgeable than I (or willing to do more archive-digging) might be able to say more.

-JAson

On Monday, August 19, 2013, t x wrote:

Hi,

  I have an tactic that looks something like:

===== nuke.v
Ltac nuke = repeat ( tac1 || tac2 || tac3 || tac4 ).

===== foo.v

Require Import nuke.

Some definitions.

Ltac foo_solver = ...

I would now like to rebind:

Ltac nuke = repeat (tac1 || tac2 || tac3 || tac4 || foo_solver).

===== bar.v

Require Import nuke foo.

Some definitions related to bar.
Ltac bar_solver = ...

I would now like to rebind:

Ltac nuke = repeat (tac1 || tac2 || tac3 || tac4 || foo_solver || bar_solver).

#### What I've tried so far:

Hint Extern <-- this does not appear to work because "auto" wants tactics that solves the subgoals. Whereas in my case, the job of each tacX is to simplify/split the goal into simpler subgoals.

#### What I'd like:

I would like something similar to a Hint Rewrite Database.

Something like:

===== nuke.v ...

Hint Use tac1 : nukedb

Hint Use tac2 : nukedb

Ltac nuke = repeat with nukedb.

===== foo.v

Hint Use foo_solver : nukedb.

(at this point, "nuke" tactic also uses foo_solver

===== bar.b

Hint Use bar_solver :nukedb.

(at this point, "nuke" tactic also uses bar_solver)

Is there a way to setup this up in Ltac, or does this go into the realms of Ocaml plugins?

Thanks!