The Coq mailing list

[Remi Vanicat <remi.vanicat AT gmail.com>]

On Tue, 21 Sep 2004 19:15:04 +0200, Roland Zumkeller
<roland.zumkeller AT polytechnique.fr>
 wrote:
> 
> 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).

doesn't the with construct made for this ?

Fixpoint even (n;nat) : bool :=
  match n with
  | O => true
  | S n => negb (odd n)
end
with odd (n:nat) : bool :=
match n with
  | O => false
  | S n => negb (even n)
end

(nto tested, but it should work)