The Coq mailing list

[Aaron Bohannon <bohannon AT cis.upenn.edu>]

On Tue, Oct 19, 2010 at 6:12 PM, Adam Chlipala 
<adam AT chlipala.net>
 wrote:
> Aaron Bohannon wrote:
>>
>> Hi, I am running into a performance issue.  I have a moderately large
>> but straightforward proof.  Basically, it breaks down into 256 cases,
>> almost all of which are solved by one use of the "inversion" tactic
>> (that does not generate additional subgoals), followed by a use of the
>> "congruence" tactic.  It is easy to write a tactic definition to
>> finish the whole proof at once.  It takes about 20 seconds on my
>> machine to run the tactic in CoqIDE, and get "Proof completed."  If I
>> type "Qed," it takes about another 20 seconds to complete the proof.
>> If I say "Defined," CoqIDE will crash after about 20 seconds (coqc on
>> the command-line does not crash but doesn't work any faster).
>>
>
> Have you tried wrapping each case-solving tactic with the [abstract]
> tactical?  This can have a dramatic effect on the amount of memory used for
> intermediate data structures.
>

Thanks.  With "abstract", I can use "Defined" without crashing CoqIDE,
and it works quickly (proof search is still slow, of course).

I'll look into the other tips, too, when I get a chance...

 - Aaron