The Coq mailing list

[Thomas Braibant <thomas.braibant AT gmail.com>]

On Wed, Nov 28, 2012 at 11:37 AM, gallais 
<guillaume.allais AT ens-lyon.org>
 wrote:
> I guess it's possible in Ocaml (?) but what about pure Ltac?

It happens that I wrote such a plugin once, for demo purpose (I do not
remember exactly what the context was...) You can find it at [1] amd
it should work out of the box with coq 8.4.

Disclaimer. There is one wrinkle here: in this plugin, I made an
arbitrary choice in the way I iterate over the hypotheses, and there
are many other possible strategies and choices. I would be interested
to discuss this with people, and see what would be the right strategy
in their case.

Yet, I implemented the example that was discussed in this thread, and
benchmarked my plugin and Guillaume's Ltac solution using the
following benchmark using a benchmark in which there are [n] instances
of [P x_i] to invert.
For n = 10, the Ltac code runs in 10s, the plugin in 1.5s.
For n = 12, the Ltac code runs in 170s, the plugin in 12s.

I think the results are pretty clear here. Unfortunately, writing plugin is:
- not well documented,
- requires a bit of boilerplate,
- and it may be the case that plugins need to be adapted in depth when
the next release of Coq come out.

Nevertheless, I really think that it is worth it to build efficient
tactics (and whose implementation is often simpler than their Ltac
counterparts).

Thomas
[1]  github https://github.com/braibant/apply-once