coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Performing tactics on each of the matched hypothesis

From: Thomas Braibant <thomas.braibant AT gmail.com>
To: Yucheng Zhang <yczhang89 AT gmail.com>
Cc: gallais <guillaume.allais AT ens-lyon.org>, AUGER Cédric <sedrikov AT gmail.com>, coq-club AT inria.fr
Subject: Re: [Coq-Club] Performing tactics on each of the matched hypothesis
Date: Fri, 7 Dec 2012 11:01:35 +0100

This discussion gave me the momentum to write a small blog post about
writing tactics in OCaml. One can find it here [1].

Hope that helps

Thomas

[1] http://gallium.inria.fr/~scherer/gagallium/your-first-coq-plugin/

On Thu, Nov 29, 2012 at 3:23 AM, Yucheng Zhang
<yczhang89 AT gmail.com>
wrote:
> Thanks all for the solutions!
>
> On Nov 28, 2012, at 8:56 PM, Thomas Braibant
> <thomas.braibant AT gmail.com>
> wrote:
>> 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 am surprised to see both codes run so slowly until I realized that 2^n
> subgoals will be generated..

Re: [Coq-Club] Performing tactics on each of the matched hypothesis, Thomas Braibant, 12/07/2012