The Coq mailing list

[Taral <taralx AT gmail.com>]

On Sun, Jul 11, 2010 at 12:28 PM, Paul Tarau 
<paul.tarau AT gmail.com>
 wrote:
> After graciously saying that
> "half is recursively defined (decreasing on 1st argument)"

This means that the x in "S (half x)" is smaller than the n you passed in.

> "Recursive call to buggy has principal argument equal to
> "half n0" instead of n0"

This means that "half n0" (the principal argument in the recursive
call) cannot be inferred to be structurally smaller than n (the
principal argument of the main call).

This isn't about n > n0, it's about n = S (S (S ... (S n0))) for some
non-zero number of S's. And the only inference coq will do is
inspection of match clauses.

I'm sure someone here will explain the nature of the structural
fixpoint better than I could...

-- 
Taral 
<taralx AT gmail.com>
"Please let me know if there's any further trouble I can give you."
    -- Unknown