Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] even

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] even


chronological Thread 
  • From: Roland Zumkeller <Roland.Zumkeller AT polytechnique.fr>
  • To: chris jhons <chrisformal AT yahoo.co.uk>
  • Cc: coq-club AT pauillac.inria.fr
  • Subject: Re: [Coq-Club] even
  • Date: Tue, 21 Sep 2004 19:15:04 +0200
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

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





Archive powered by MhonArc 2.6.16.

Top of Page