The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

Alexandre Pilkiewicz wrote:
> I have three mutually recursive inductive on which I would like to
> prove three mutually recursive lemmas.
>
> The proof itself goes well (it's a few line, with almost no automation
> to avoid using a lemma to prove itself). It is at the Qed that
> everything goes wrong. After a time between 30 minutes and a few hours
> (I gave up watching it), and without really increasing its memory
> usage, Coq answers "Error: Cannot guess decreasing argument of fix.".
> I guess the long time is due to the fact coq checks all the
> combination of possible decreasing argument. So my first question is:
> is there a way to specify the decreasing arguments on lemmas, so that
> the checking goes faster. Because I can't try new proofs if it always
> take 2 hours to check them...
>    

Are you using an induction principle generated by [Scheme]?  There 
shouldn't be any need for explicit [fix]es if so.