The Coq mailing list

[Viktor Vafeiadis <viktor AT mpi-sws.org>]

On 13 Dec 2013, at 08:21, Christine Paulin wrote:

> The principle is the recursive call in the definition of f x should be of 
> the form 
>     f t 
> with t a strict recursive subterm of x
> 
> there is a rule to accept a term t of the form (match u with t1 .. tn end)
> whenever all ti are recursive subterms of x 
>     in particular when u has type False (match u with end) is accepted 
[...]
> So some check needs to be added. A simple idea would be that a recursive 
> subterm could never be an abstraction, or to add some finer analysis in 
> which context u should be typable.

An even simpler fix would be to just drop the rule that accepts (match u with 
t1 .. tn end) as a subterm.

I wonder whether there are any actual proofs that rely on recursive 
definitions of such form.


Viktor