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

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.

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: Apr 19 2024 at 13:02 UTC