The Coq mailing list

[Edsko de Vries <Edsko.de.Vries AT cs.tcd.ie>]

Hi Yves,

> 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.

Thanks for clarifying that. Indeed, I had thought that there should be  
an additional bullet point to deal with the "special case" I mentioned  
earlier. What you are saying makes perfect sense, and simplifies my  
view of the world :)

Thanks again,

Edsko