The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

I'm glad it works.  Is the meaning of ::= documented somewhere in the reference manual?  What does it do?

-Jason

On Aug 20, 2013 2:38 AM, "t x" <txrev319 AT gmail.com> wrote:

Jason: your idea worked.

  Using the following, I can fake a "add only tactic database"

==== nuke.v

Tactic Notation "nuke_tacs" := initial_set_of_tacs.

Ltac nuke_update := nuke_tacs.

Ltac nuke :=
  .... do some stuff ...;
  repeat (nuke_update || ... tacs ...);
  .... do some more stuff ... .


==== to register a new tac

Tactic Notation "nuke_tacs" := new_tac || nuke_tacs.

(* Tactic Notation does not support recursion.
   Thus, the second nuke_tacs gets the old value. *)

(* Now, we need to force the "nuke" tactic
   to use the latest nuke_tacs *)

Ltac nuke_update ::= nuke_tacs.

(* the ::= ensure taht nuke_update has the latest nuke_tacs; and forces
   nuke to use the latest nuke_update *).
  

On Tue, Aug 20, 2013 at 6:29 AM, t x <txrev319 AT gmail.com> wrote:

re re-binding:

  I was

  * playing with "Ltac ... ::=" (note the double ::), for examp;e

Ltac nuke_split := new_tac || nuke_split

  * getting stack overflows

  * attributing said stack overflows to the 2nd nuke_split referring to the new rather than the old value (since Ltacs can recursively call itself)

  * however, perhaps Tactic Notation's inability to recurse might be useful in this case.

  * I will re-investigate on this and report back.

re plugins:

  I'm going the OCaml route. If anyone knows of any tutorial besides http://gallium.inria.fr/blog/your-first-coq-plugin/ I would appreciate it. (It seems like the main difficulties is just understanding boiler plate.)

On Tue, Aug 20, 2013 at 4:16 AM, Jason Gross <jasongross9 AT gmail.com> wrote:

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!