The Coq mailing list

["Harley D. Eades III" <harley.eades AT gmail.com>]

Hello.

I am trying to define a function using the well-founded annotation for function definitions.

Here is a simple example illustrating both my problem and what I am attempting:

Inductive ord : (nat * nat) -> (nat * nat) -> Prop :=

  | ord_red1 : forall n n' m m',

    n < m -> ord (n, n') (m, m')

  | ord_red2 : forall n n' m',

    n' < m' -> ord (n, n') (n, m').

Function ack (p : nat*nat) {wf ord p } : nat := 

  match p with

    | (0, n) => (S n)

    | (S m, 0) => ack (m,1)

    | (S m, S n) => ack(m, ack(S m, n))

  end.

Keep in mind that this is just an example.  The function I ultimately want to define is more complex

than this example.  

The main problem is that the above function is rejected by Coq.  I believe it is because I am not allowed

to use nested recursive calls in the body of a function; as in the last branch of ack.  

My question is, does anyone know of a way around this?  I really want to be able to use the well-founded annotation, because

the function I really want to define would be very difficult any other way.

In this case I might be able to use 'fix' to get around the above problem, but I am wondering if there are any other ways, because doing it using 'fix' essentially makes using the wf-annotation pointless.  Also, my ultimate goal is not possible using 'fix', at least I think it is.  

If anyone wants to know what this "ultimate" function is I will post it.

Thanks,

Harley