The Coq mailing list

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

I have seen that pattern in some library examples, but defining

Fixpoint half (n  : nat) : nat :=
  match n with
  | O => n
  | S O => pred n
  | S (S x) => S (half x)
  end.

will not help too much. On the other hand, in functions where recursion
is the innermost in a composition things go well. For instance mult1 is ok in

Fixpoint plus1 (n m:nat) {struct n} : nat :=
  match n with
  | O => m
  | S p => S (plus1 p m)
  end.

Fixpoint mult1 (n m:nat) {struct n} : nat :=
  match n with
  | O => O
  | S p => plus1 m (mult1 p m)
  end.

which makes me think that there's no deep reason for not "connecting the 
dots",
as the implementation trusts plus1 as decreasing when it happens to occur
outside mult1.

Paul

On Sun, Jul 11, 2010 at 4:58 PM, Georges Gonthier
<gonthier AT microsoft.com>
 wrote:
> 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
>>
>
>