The Coq mailing list

[Georges Gonthier <gonthier AT microsoft.com>]

The problem is in the base cases of your half function: they return a literal 
0, which is not structurally less than or equal to the argument n; try 
returning n or pred n for those cases.

Georges

-----Original Message-----
From: Paul Tarau 
[mailto:paul.tarau AT gmail.com]
 
Sent: 11 July 2010 21:05
To: Taral
Cc: 
coq-club AT inria.fr
Subject: Re: [Coq-Club] connecting the dots between Fixpoint definitions

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
>