The Coq mailing list

[Michiel Helvensteijn <mhelvens AT gmail.com>]

Hi all,

I have two mutually recursive functions with two arguments each
(simplified example):

Fixpoint f (a: T) (b: U) : V := ...
with g (a: T) (b: U) : V := ...

I know that they terminate because, as a pair, the arguments are
structurally decreasing. That is to say, in `f`, `a` decreases and `b`
is passed unchanged, and in `g`, `a` is passed unchanged and `b`
decreases.

`Fixpoint` accepts only a single decreasing argument as evidence for
termination. Apparently the `Function` construct is more flexible
w.r.t. termination evidence, but not, it seems, for mutual recursion.

Sure, I could add a third argument to decrease on, such as a `c: nat`
containing the sum of the structural depths of `a` and `b`. But that
would involve a lot of tedious boilerplate code, not to mention
preconditions and proofs of the fact that `c` always remains large
enough.

Is there a technique or construct I'm unaware of? Something that will
make this easier?

Thanks in advance!

--
www.mhelvens.net