The Coq mailing list

[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