The Coq mailing list

[Paul Tarau <paul.tarau AT gmail.com>]

It is just about remembering that if f is decreasing and g is
decreasing then f composed with g is also decreasing. Coq has a lot of
nice general rules that it applies quite elegantly in various modules
so it is somewhat surprising that it does not do it in this case.

> This isn't about n > n0, it's about n = S (S (S ... (S n0))) for some
> non-zero number of S's.

Given that Coq knows that S x > x, "n>n0"  should be inferred as
equivalent to "n = S (S (S ... (S n0)))" by the induction rule on nat,
shouldn't it?

Paul

On 7/11/10, Taral 
<taralx AT gmail.com>
 wrote:
> 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
>