The Coq mailing list

[Alexandre Pilkiewicz <alexandre.pilkiewicz AT polytechnique.org>]

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 ?

Thanks for the help

- Alexandre