The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

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.