The Coq mailing list

[Dimitri Hendriks <Dimitri.Hendriks AT phil.uu.nl>]

Dear all,

Is it possible to define a function recursive in 2 arguments?

Suppose e.g. I want to define a function which, given 2 lists of a's and b's,
merges these lists into one sorted list. This can't (I believe) be written
using a single fixpoint construction, as it's not always the same argument 
which
is actually decreasing. So I tried the following mutual recursive definitions
of f1 and f2, the first is recursive in its first argument, the second in the
second. But they're not accepted:

"Error: Recursive call applied to an illegal term
 The 1-th recursive definition f2 :=
 [...]
 is not well-formed."

How to do it?

Thans, Dimitri

*********************

Require Export PolyList.

Inductive AB : Set := a : AB | b : AB.

Fixpoint f1 [l1:(list AB)] : (list AB)->(list AB) :=
[l2] Cases l1 l2 of
|(cons a t1)(cons a t2) => (cons a (cons a (f1 t1 t2)))
|(cons b t1)(cons a t2) => (cons a (f2 l1 t2))
|(cons a t1)(cons b t2) => (cons a (f1 t1 l2))
|(cons b t1)(cons b t2) => (app (f1 t1 t2)(cons b (cons b (nil AB))))
| _          _          => (app l1 l2)  w
end
with f2 [l1,l2:(list AB)] : (list AB) :=
Cases l1 l2 of
|(cons a t1)(cons a t2) => (cons a (cons a (f1 t1 t2)))
|(cons b t1)(cons a t2) => (cons a (f2 l1 t2))
|(cons a t1)(cons b t2) => (cons a (f1 t1 l2))
|(cons b t1)(cons b t2) => (app (f1 t1 t2)(cons b (cons b (nil AB))))
| _          _          => (app l1 l2)
end.