The Coq mailing list

[dehlinge AT dpt-info.u-strasbg.fr]

Oops ! Forgot the recursive calls...

The actual function I'm interested in is :
        f n = 0         if n=1
        f n = f (n+1)   if n is even
        f n = f (n-3)   if n is odd


>> I'm trying to translate the following function into Coq :
>>      f n = 0         if n=1
>>      f n = n+1       if n is even
>>      f n = n-3       if n is odd
>
> No recursion means you don't need to use Fixpoint or Fix.
> How about:
>
> Require Export Even.
>
> (* Must redefine this lemma with "Defined" instead of "Qed" *)
> Lemma even_odd_dec : forall n, {even n} + {odd n}.
> Proof.
> induction n.
> auto with arith.
> elim IHn; auto with arith.
> Defined.
>
> Definition f (n:nat) : nat :=
>   match n with
>   | 1 => 0
>   | n =>
>       match even_odd_dec n with
>       | left _ => n + 1
>       | right _ => n - 3
>       end
>   end.
>
> Eval compute in (f 5).
>
> Robert
>