Is there any way to have mutually-recursive functions that use well-founded recursion? `Program Fixpoint`

and `Equations`

both refuse to work, and I'm wondering if there are any workarounds (like nesting the recursive call or something... is there a version of `fix`

for well-founded recursion, maybe)?

(hmm, maybe I could manually use `Fix`

? but I'd rather not do that if I don't absolutely have to)

Mutual recursion is roughly equivalent to recursion on a sum type, that should allow you to repackage things into a single recursive function.

For example instead of

```
Fixpoint even (n : nat) : bool := ...
with odd (n : nat) : bool := ...
```

you can write it as

```
Inductive arg := Even : nat -> arg | Odd : nat -> arg.
Program Fixpoint f (x : arg) { measure (* for some measure defined on arg *) } : bool :=
match x with
| Even n => (* implementation of even *) ... not (f (Odd (n-1)) ...
| Odd n => (* implementation of odd *) ... not (f (Even (n-1)) ...
end.
```

Thanks, I'll try that!

Equations supports it using dependent pattern matching as well: http://mattam82.github.io/Coq-Equations/examples/Examples.mutualwfrec.html

@Matthieu Sozeau I see that the first step is to "declare the prototypes ouf [sic] our mutual definitions" via an `Inductive`

type—is that analogous to @Li-yao's solution, out of curiosity?

(Also, thank you for the link! I did Google my issue first, I swear :grimacing:)

Yes, its analogous. The example handles the general case where you might want different argument and return types to your functions. If it's only about the arguments then a sum type suffices indeed.

Last updated: Jun 24 2024 at 12:02 UTC