The Coq mailing list

[Pierre Casteran <casteran AT labri.fr>]

Hello Stefan,

  You can find in Coq's standard library the module

Coq.Wellfounded.Lexicographic_Product

which proves that the lexicogrqphic product of two wf sets
is wf.

If you want to work with Z, you can use the order
 Zwf (c x y:Z) := c <= y /\ x < y.

which is wf too (see library Coq.ZArith.Zwf)


Pierre



Stefan Karrmann wrote:
> 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.
> > > ------------------------------------------------------------------------------



--
Pierre Casteran,
LaBRI, Universite Bordeaux-I      |
351 Cours de la Liberation        |
F-33405 TALENCE Cedex             |
France                            |
tel : (+ 33) 5 40 00 69 31
fax : (+ 33) 5 40 00 66 69
email: Pierre . Casteran @ labri .  fr  (but whithout white space)
www: http://www.labri.fr/Perso/~casteran