The Coq mailing list

[Benjamin Werner <werner AT pauillac.inria.fr>]

> Hi,
> 
> I'm trying to define a function of the following shape
> 
> f (Tcons a) (Tcons b) = g (f a (Tcons b)) (f (Tcons a) b)
> 
> (plus adequate terminating cases)
> 
> where
>  - Tcons is the constructor of the type T
>  - g is a simple expression of type T->T->T
> 
> I have read the papers of Venanzio Capretta and Ana Bove about
> modelling general recursion in type theory, but their accessibility
> predicate will here have the shape:
[...]

Hi,

Your function seems to have a form similar to Ackermann's function. I
do not think it is a good idea to use general well-founded recursion
here, but rahter stay inside structural recursion.

all you have to do is use two embeded fixpoints.

To illustrate, here is a definition of Ackermann's function in Coq :

Fixpoint Ack [n:nat] : nat -> nat :=
 Cases n of 
  O => [m:nat](S m)
| (S n') => Fix aux {aux [m:nat] : nat :=
             Cases m of
              O => (Ack n' (S O))
           | (S m') => (Ack n' (aux m'))
end}
end.



Hope this helps, cheers,


Benjamin