The Coq mailing list

[Robert R Schneck-McConnell <schneck AT math.berkeley.edu>]

> 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