The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

The partial way out of this issue is to put some fuel (a large number of Acc_intro constructors) in front of your opaque proof, as is done by Wf.Acc_intro_generator

On Mon, Feb 6, 2017 at 12:01 PM Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr> wrote:

Le 06/02/2017 à 08:55, Gaetan Gilbert a écrit :
>>But if you use the second method (acc_rect_alt), it seems to me that
> there would be no need to advance in the computation of the
> accessibility proof while reducing a term defined by induction on that
> predicate, even within Coq internal evaluation strategies. I am not
> sufficiently aware of Coq's internal evaluation mechanism to be certain
> of that but I do not think that added axioms would block the evaluation
> because the proof of accessibility is never needed to reduce the term.
> It might however saturate the memory if it is never reduced ...
>
> Fixpoints only unfold if the principal argument is a constructor. For
> acc_rec_alt the principal argument is the (Hx : acc x) so it needs to be
> reduced.
> This is because otherwise you would get an infinite reduction
>
> acc_rec_alt x Hx ↦ f x (fun y Hy => acc_rec_alt ...)
> ↦ f x (fun y Hy => f y (fun z Hz => acc_rec_alt ...))
> ↦ ...

Ok this is a bit unfortunate ... it means anything defined with
the Fix operator or by induction over a predicate will almost
certainly have its evaluation blocked because most proof terms
are Opaque in Coq ... this is not specific to this particular
fixpoint computation.

D.