The Coq mailing list

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

Hello,

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?

------------------------------------------------------------------------------
Module Ackermann.

(*
ackermann 0 n = n+1
ackermann m 0 = ackermann (m-1) 1
ackermann m n = ackermann (m-1) (ackermann m (n-1))
*)

Require Import Arith.

Section Ackermann1.

Require Import Streams.

CoFixpoint nats_from (n:nat) : Stream nat :=
   Cons n (nats_from (n+1)).

CoFixpoint col_from (n : nat)(x:Stream nat) : Stream nat :=
   let v := Str_nth n x
   in Cons v (col_from v x).

CoFixpoint ack_from (c:Stream nat) : Stream (Stream nat) :=
   Cons c (ack_from (col_from 1 c)).

Definition ack_tab : Stream (Stream nat) :=
   ack_from (nats_from 1).

Definition ack (m n : nat) : nat :=
   Str_nth n (Str_nth m ack_tab).

(* Eval compute in ack 2 2.  *)

End Ackermann1.

(*
Extraction "ackermann" ack.
Extraction Language Haskell.
Extraction "ackermann" ack.
*)

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.

(*
This fails:
*)

Fixpoint ack' (x:A) : nat :=
   F x ack'.

Definition ack2 (m n:nat):nat :=
   ack' (m,n).

End Ackermann2.

End Ackermann.
------------------------------------------------------------------------------

Sincerly,
-- 
Stefan