The Coq mailing list

[Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr>]

Now I do understand the reason for this Acc_intro_generator ...

I have another question regarding "singleton elimination".
As explained earlier, it is not needed for well-founded recursion.
It is not need either for False_rect elimination (I agree
it is more "void" than "singleton" elimination):

Fixpoint False_rect_prog (H : False) : forall X, X :=
   False_rect_prog (match H with end).

So my question is: does "singleton elimination" add some
expressivity to the CIC/Coq or is it just introduced in the
calculus as a convenience/shortcut ?

D.


Le 06/02/2017 à 14:10, Matthieu Sozeau a écrit :
> 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
> <mailto: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.
>