The Coq mailing list

[Pierre Courtieu <Pierre.Courtieu AT cnam.fr>]

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