The Coq mailing list

[Pierre Boutillier <pierre.boutillier AT pps.univ-paris-diderot.fr>]

Le vendredi 13 décembre 2013 à 11:04 +0100, Viktor Vafeiadis a écrit :
> 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.
Require Import NPeano.

Print gcd.

> 
> 
> Viktor