The Coq mailing list

[Matthieu Sozeau <matthieu.sozeau AT gmail.com>]

Le 11 mars 2011 à 01:53, Alexandre Pilkiewicz a écrit :

> Dear list
> 
> 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...
> 
> In the mean time, I tried to prove it using Program. I tried to do this
> 
> Program Fixpoing lemma1 arg11 ...  arg1n {struct arg1i}: concl1 := _
> with lemma2 arg21...arg2p {struct arg2j} := _
> ...
> 
> But it does not work. When solving the obligation for lemma1, lemma2
> is not accessible. Is that a bug or a feature ?

It is a feature: to avoid using lemma1 or lemma2 inadvertently in the
obligations, Program tries to clear them from the context if possible.
You can rebind them using [let lemma1 := lemma1 in _] to force the
dependency, and set the default tactic to idtac to avoid the 
simplifier which would clear these hypotheses (they're tagged with 
[fix_proto]).

-- Matthieu