The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT inria.fr>]

On 26/03/2014 05:22, Hugo Carvalho wrote:
> Whoa, hold on. I looked at this, and thought, "Surely it can't work
> Coq's fix is primitive recursive, so no way this kind of definition
> works without some well-founded trickery!". Sure enough, it does work,
> and even more surprisingly, you can prove a strong recursion scheme over
> the naturals using the same trick!

There must be something I am missing, as I don't understand how the 
example shows anything.

Strong recursion is just simple recursion applied to a more general 
property. So, by explicitly writing "fix" in your proof script, you are 
just complicating and obfuscating a proof that is trivial.

If the obtained lambda term was executing faster (less reduction steps 
for some evaluation strategy) with nested "fix"s rather than with a 
simple structural induction, that would be convincing. But that does not 
even seem to be true on your example.

Best regards,

Guillaume