## Stream: Coq users

### Topic: Mutual well-founded recursion

#### Joshua Grosso (Nov 13 2020 at 19:33):

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)?

#### Joshua Grosso (Nov 13 2020 at 19:37):

(hmm, maybe I could manually use `Fix`? but I'd rather not do that if I don't absolutely have to)

#### Li-yao (Nov 13 2020 at 19:42):

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

#### Li-yao (Nov 13 2020 at 19:44):

``````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.
``````

#### Joshua Grosso (Nov 13 2020 at 19:47):

Thanks, I'll try that!

#### Matthieu Sozeau (Nov 13 2020 at 19:51):

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

#### Joshua Grosso (Nov 13 2020 at 19:57):

@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?

#### Joshua Grosso (Nov 13 2020 at 19:57):

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

#### Matthieu Sozeau (Nov 13 2020 at 19:59):

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