The Coq mailing list

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

Thanks a lot, it helps indeed. And the "pattern" in your code seems reusable 
to
handle various cases of legitimate recursion. Maybe this can all be 
encapsulated
in a language construct that generates such proofs automatically?

Paul

On Sun, Jul 11, 2010 at 4:25 PM, julien forest 
<forest AT ensiie.fr>
 wrote:
> Dear Paul,
>
> On Sun, 11 Jul 2010 14:28:39 -0500
> Paul Tarau 
>Â <paul.tarau AT gmail.com>
>  wrote:
>
>> Dear Coq users,
>>
>> When trying to port some simple code from Haskell to Coq
>> I have noticed that it does not propagate what it knows
>> about a function ("half" in the following example) to
>> another function ("buggy" in the example).
>>
>> Require Import Bool.
>>
>> Fixpoint isEven (n: nat) {struct n} : bool :=
>> match n with
>> | 0 => true
>> | 1 => false
>> | S (S n) => isEven n
>> end.
>>
>> Fixpoint half (n  : nat) : nat :=
>>   match n with
>>   | O => 0
>>   | S O => 0
>>   | S (S x) => S (half x)
>>   end.
>>
>> Fixpoint buggy (n:nat) {struct n} : nat :=
>> match n with
>> | 0 => 0
>> | S n => if isEven n then 0 else S (buggy (half n))
>> end.
>>
>> After graciously saying that
>> "half is recursively defined (decreasing on 1st argument)"
> At this point, this probably only means that coq found that n is the
> only POSSIBLE decreasing argument.
>
>> it complains that
>> "Recursive call to buggy has principal argument equal to
>> "half n0" instead of n0"
>>
>> The system clearly knows that "S n" decreases to "n" and it
>> is also acknowledging that "half is decreasing" but it does
>> not seem to connect the dots and accept "half n"
>> as an argument in the recursive call to "buggy".
> No, for structural induction coq (mostly) only accepts recursive
> definitions which recurse only on syntactically smaller arguments. Here
> buggy can only recurse on n.
>
> The fact that (half n) is smaller than n is not so obvious and in fact
> needs an inductive proof. Coq cannot guess this for you and thus you
> cannot use structural fixpoint to define such a function.
>
> You can use non structural induction to define buggy (Function or
> Program Fixpoint).
>
> For example, the following code will work fine and define the
> function (I added a call to functionnal induction to show the
> advantages on using Function):
>
> Require Import Bool.
>
> Fixpoint isEven (n: nat) {struct n} : bool :=
> match n with
> | 0 => true
> | 1 => false
> | S (S n) => isEven n
> end.
>
> Function half (n  : nat) : nat :=
>  match n with
>  | O => 0
>  | S O => 0
>  | S (S x) => S (half x)
>  end.
> Require Import Recdef.
> Require Import Arith.
>
> Lemma half_decrease :
>  forall n, half n <= n.
> Proof.
>  intros n.
>  functional induction (half n);
>  auto with arith.
> Qed.
>
> Function buggy (n:nat) {measure (fun n => n) n} : nat :=
> match n with
> | 0 => 0
> | S n => if isEven n then 0 else S (buggy (half n))
> end.
> Proof.
>  intros n n' H1 H2.
>  apply le_lt_trans with n'.
>  apply half_decrease.
>  auto with arith.
> Qed.
>
>
>>
>> Can anyone suggest a simple workaround to the problem?
>>
>
> Hope this help,
> Regards,
> Julien
>
>