The Coq mailing list

["Roland Zumkeller" <roland.zumkeller AT gmail.com>]

Hi,

You can verify the hypothesis that it's due to the guard condition
with the command "Guarded", which checks the condition during a proof.

When verifying the guard condition, Coq makes some reductions in order
to allow fixpoint definitions where the recursive *reduces* to a
subterm of the argument, but is not syntactically given in this way,
e.g.:
  Fixpoint f n {struct n} := match n with O => O | S n' => f (0+n') end.

Probably some of these reductions are superfluous in your case and
lead to long computations. A possible workaround is to hide the
corresponding subterms/proofs by making them section hypotheses.
You can then instantiate them after the fixpoint definition has already been
accepted.

Hope this helps.

Roland


On 10/03/2008, Jean Goubault-Larrecq 
<goubault AT lsv.ens-cachan.fr>
 wrote:
>
>  Hi, I'm generating big Coq proofs automatically,
>  which use 'fix' a lot across Remarks with transparent
>  proofs.  To state what's happening to me, Coq seems
>  to get stuck at the end of a Remark called rem_2421
>  at line 32969 --- numbers to give an idea of size.
>  Arrived here, it seems to process the closing 'Defined'
>  indefinitely.  I have been waiting for 11 minutes
>  already.  This already happened earlier in the same file,
>  but is getting more and more of a problem as Coq
>  advances in it (it is stuck at roughly 5% of the file).
>         I strongly suspect that Coq is lost checking
>  for the guard conditions in the terms.  After all,
>  my Coq process is 57360 Kb big at this point, is
>  only 8136 Kb at startup, and the rest (~ 50 Mb) is
>  roughly just one big lambda-term.
>
>         Is this a known problem with fix?
>
>         Is there a way to speed it up, apart
>  from changing my Coq proof generation algorithm?
>  (An option that I've now almost exhausted.)
>
>         I can provide the example at will, but
>  emailing it would be a breach of etiquette.  Of
>  course I cannot make any smaller example: size seems
>  precisely to be the problem.
>
>         Best,
>
>
>         -- Jean Goubault-Larrecq
>         (LSV/ENS Cachan & CNRS UMR 8643 & INRIA projet SECSI).
>
>  --------------------------------------------------------
>  Bug reports: http://logical.futurs.inria.fr/coq-bugs
>  Archives: http://pauillac.inria.fr/pipermail/coq-club
>           http://pauillac.inria.fr/bin/wilma/coq-club
>  Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
>


-- 
http://www.lix.polytechnique.fr/~zumkeller/