The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

I had two very large hypotheses which were defined via [Let], and which I substituted in to the goals before my intros, because I wanted to make the rest of the proof [abstract] and not have the theorem depend on the [Let] statements.  Changing [destruct H] to [elim H; clear H; intro] (because all of these things are records with one field) shaved off one second.  Changing the [Let]s to [Definition]s and unfolding them only after the [intros] shaved off another 9 seconds.

Thanks!

-Jason

On Thu, Jul 26, 2012 at 4:48 AM, Pierre Courtieu <Pierre.Courtieu AT cnam.fr> wrote:

Hi,

Do you have a lot of hypothesis? Destruct is not a basic tactic. It
does rather a lot of work managing the context of the proof. Maybe you
can try using the more basic tactic elim.

Hope this helps,
Pierre



2012/7/26 Jason Gross <jasongross9 AT gmail.com>:

> Hi,
> I have a goal that looks like [forall a b c d e, f = g], and each of the
> quantified variables is a record type with a single constructor.  The tactic
>   repeat (let H := fresh in intro H; destruct H); simpl in *;
>     apply f_equal.
> takes 15 seconds to run.  When I run the tactics separately, the [repeat]
> tactic takes 15 seconds to run, and the [apply] tactic takes 1 second.
> Moving [simpl in *] inside the parentheses reduced the time of the [repeat]
> tactic to 12 seconds, removing the [in *] brings it down to 11.  It takes so
> long because there are so many terms in the proof; when I [Set Printing
> All], and throw the result into a word counter, it tells me that there are
> 29251 words and almost 600000 characters (with spaces).  The obvious
> solution is to hide more things inside of records and pass fewer arguments
> around, but this is hard, because I make extensive use of sort polymorphism.
> Does anyone have generic advice for improving the speed of [apply] and,
> especially, [destruct]?
>
> (If anyone wants to try giving specific advice, my current codebase is
> available at https://www.dropbox.com/s/19tzk0kisxb38i5/catdb.zip, the full
> version (with already compiled files) is at
> https://www.dropbox.com/s/7c9zq3hr91fnidw/catdb-full.zip.  I'm working on
> line 87 of DataMigrationFunctors.v.)
>
> Thanks!
>
> -Jason