The Coq mailing list

[Georges Gonthier <gonthier AT microsoft.com>]

  As Pierre Courtieu very kindly pointed out, I've been posting nonsense, 
since the obvious way of writing half does not give a decreasing function, 
because the S before the recursive call (which I conveniently forgot when I 
tested the example) is clearly not a decreasing function...
 However half can be written as a decreasing function by using an accumulator:
  Definition half n :=
    let fix loop r m {struct r} :=
      match r, m with
      | S r', S (S m') => loop r' m'
      | S r', 1 => r'
      | _, _ => r
      end in loop n n.
However it is probably simpler to replace the non-decreasing call to half n 
in your "buggy" function, with the expression (n - half (S n)), which is (at 
least from 8.2 on) decreasing in n, and probably easy to prove equal to half 
n within the existing theory.

  Georges

-----Original Message-----
From: Georges Gonthier 
[mailto:gonthier AT microsoft.com]
 
Sent: 12 July 2010 10:40
To: Paul Tarau
Cc: 
coq-club AT inria.fr
Subject: RE: [Coq-Club] connecting the dots between Fixpoint definitions

  That's probably because the definition of pred in the version of Coq you 
are using has the same problem, so you need to correct that as well (this was 
fixed in 8.2, and your example tested OK on my installation). You seem to be 
conflating two different notions of "decreasing"
  "f is decreasing on its 1st argument" -> in all recursive calls, then 1st 
arg of f is structurally less than the formal 1st argument
  "f n is structurally less than (or less than or equal to) its 1st argument 
n"
The two are related : Coq only detects the latter property when the first one 
holds, and then (bug?) not for mutual fixpoints. However they are different, 
in spite of the somewhat confusing way in which Coq states the first property.

  Georges

-----Original Message-----
From: Paul Tarau 
[mailto:paul.tarau AT gmail.com]
 
Sent: 12 July 2010 01:30
To: Georges Gonthier
Cc: 
coq-club AT inria.fr
Subject: Re: [Coq-Club] connecting the dots between Fixpoint definitions

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
>>
>
>