The Coq mailing list

[Stefan Karrmann <sk AT mathematik.uni-ulm.de>]

Hello Pierre,

Pierre Casteran (Mon, Jun 14, 2004 at 07:45:06AM +0200):
> Stefan Karrmann wrote:
> >as a newbie to coq I have some questions. As I'm used to functional
> >programs I tried to start with function definitions and extraction.
> >
> >How can I switch from coq's nat to Haskell's Integer type? The former
> >uses much more memory.
> >
> >How can I define recursive functions, e.g. the Ackermann function?
> >I found a definition which uses streams, but my try to define it
> >directly failed. Where can I find some hints? Is well-foundmess (Wf)
> >the right starting point?
> 
> It  also possible to use a well founded order on pairs of natural 
> numbers (using Coq standard library) and define ackerman of type
> nat * nat -> nat (or Z * Z -> Z)

How can this be coded? The key relation is:

Definition A : Set := pair nat nat.
Definition R (x:A)(y:A) : Prop := 
   ((fst x) < (fst y))
   \/ ((fst x = fst y)
      /\ (snd x < snd y) ).

> >------------------------------------------------------------------------------
> >Module Ackermann.
> >
> >(*
> >ackermann 0 n = n+1
> >ackermann m 0 = ackermann (m-1) 1
> >ackermann m n = ackermann (m-1) (ackermann m (n-1))
> >*)
> >Section Ackermann2.
> >
> >Require Import Wf.
> >
> >Definition A : Set := prod nat nat.
> >
> >Definition P (A:Set) : Type := nat.
> >
> >Definition R (x y : A) : Prop :=
> >   ((fst x) < (fst y))
> >   \/ ((fst x = fst y)
> >      /\ (snd x < snd y) ).
> >
> >Definition F (x:A) (f: A -> nat) : nat :=
> >   match x with
> >   | (0,n) => n+1
> >   | (m,0) => f (m-1,1)
> >   | (m,n) => f (m-1,f (m,n-1))
> >   end.
> >
> >
> >End Ackermann2.
> >
> >End Ackermann.
> >------------------------------------------------------------------------------

-- 
Stefan