The Coq mailing list

[Yves Bertot <Yves.Bertot AT sophia.inria.fr>]

Frederic Blanqui wrote:
> Edsko de Vries a écrit :
> > > or perhaps the special case were
> > > `a' does not occur free in `B':
> > >
> > >        E,Γ |- A:Prop      E,Γ |- B:Set
> > >        ----------------------------------
> > >            E,Γ |- A->B:Set
> > >
> > > Is it possible to give some meaningful examples of terms that can be
> > > constructed this way?
> >
> > Such functions are valid only in special cases; in particular, it is 
> > possible to use a proof as argument to a function that returns an 
> > argument in Set if the proof is used *only* to guard termination of 
> > the function, but cannot otherwise influence the value returned. If 
> > you are working through Coq'Art, you'll get to such functions 
> > eventually: Sections 14.2.3 and 15.2.
>
> Could someone give bibliographic references about this limitation?
>
> --------------------------------------------------------
> Bug reports: http://logical.saclay.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

I think this topic evolves far beyond Matej's initial question.  There 
are only very few links between typing the prod-rule and general 
recursion as handled in the chapters cited by Edsko.  Concentrating
on chaps. 4 to 9 is probably more productive for Matej.

The rest of this message is for Edsko and Frédéric.

From what I understood of Coq, there is no specific mechanism that 
takes care of verifying that pattern-matching is only used to ensure 
termination.  What is used in general recursion is a combination of the 
following three features of the theory of inductive types in Coq:

- Pattern-matching is allowed on any Prop if what you need to produce is 
in sort Prop.
- Structural guardedness is verified modulo beta-iota-zeta-delta-reduction.
- An expression is a legitimate argument for a structural recursive 
guarded call if it is a variable (or the output of a function given as a 
a variable) obtained through pattern-matching from the recursive 
function's main argument, or if it is a pattern-matching expression 
where all branches are (recursively) legitimate arguments for a 
structural recursive guarded call.
 * in particular, (p. 399), Acc_inv A R x H y Hr is structurally 
smaller than H, this expression is a legitimate argument for a 
structural recursive call if H is the principal argument of the 
recursive function (as in Acc_iter).
 * Moreover, the type of
            Acc_inv A R x H y Hr
is
            Acc R y ,
this type is in sort Prop, so the first feature applies.

This combination of features can be used in an even more clever way.  
There is  a message by Christine Paulin on August 19, 2002 where this is 
explained (entitled "Re: How widely applicable is Coq? (beginner)").   
Chap. 15.4 is a re-formulation of the technique.

If you plan to read section 14.2.2, please note that there are errors in 
the book, the corrections are given
at http://www.labri.fr/perso/casteran/CoqArt/induc-fond/index.html

Yves