The Coq mailing list

[Roland Zumkeller <Roland.Zumkeller AT polytechnique.fr>]

The first function can be translated directly:

Fixpoint even (n:nat) : bool := match n with
| 0 => true
| 1 => false
| S (S n') => even n'
end.

One way to do cope with the mutual recursive definition is it to write 
both functions in one, and to define projections:

Fixpoint even'_odd (n:nat) : bool * bool  :=
  let even' i := fst (even'_odd i) in
  let odd i := snd (even'_odd i) in
  (match n with
  | 0 => true
  | S n => odd n
  end,
  match n with
  | 0 => false
  | S n => even' n
  end).

Definition even' i := fst (even'_odd i).
Definition odd i := snd (even'_odd i).

(Of course this can be written somewhat shorter, but i'd like to 
suggest a more or less general scheme).

With lazy evaluation you can avoid caculating the values of both 
functions if you need just one.

Roland