## Stream: Coq users

### Topic: Mutual recursion function in type

#### Julin S (Jun 13 2022 at 06:22):

Can we not use one of the mutually recursive functions as part of the type?

I tried:

``````Fixpoint iseven (n:nat) : Prop :=
let hrv := helper n in (* Just to use helper *)
match n with
| O => True
| S n' => isodd n'
end
with isodd (n:nat) : Prop :=
let hrv := helper n in (* Just to use helper *)
match n with
| O => False
| S n' => iseven n'
end
with helper (n:nat) : {iseven n} + {isodd n}.
``````

got error as:

``````The reference iseven was not found in the current environment.
``````

But a version without occurrence of one of those functions in the type worked:

``````Fixpoint iseven (n:nat) : Prop :=
let hrv := helper n in (* Just to use helper *)
match n with
| O => True
| S n' => isodd n'
end
with isodd (n:nat) : Prop :=
let hrv := helper n in (* Just to use helper *)
match n with
| O => False
| S n' => iseven n'
end
with helper (n:nat) : Prop :=
let e := iseven n in     (* Just to use iseven *)
let o := isodd n in       (* Just to use isodd *)
False.
``````

Is there a way around this?

#### Kenji Maillard (Jun 13 2022 at 07:56):

I don't think there is currently a way to write exactly this kind of "recursion-recursion" in Coq, but you can often encode it with a dependent sum.
For instance in your setting you could write a single function

``````Fixpoint iseven_isodd_helper (n : nat) : { iseven : Prop & { isodd : Prop & { iseven } + {isodd} } := ...

Definition iseven (n : nat) : Prop := proj_sigT1 (iseven_isodd_helper n).
Definition isodd (n : nat) : Prop := proj_sigT1 (proj_sigT2 (iseven_isodd_helper n)).
Definition helper (n : nat) : {iseven n} + {isodd n} := proj_sigT2 (proj_sigT2 (iseven_isodd_helper n)).
``````

#### Julin S (Jun 13 2022 at 09:00):

Which module is needed to have `proj_sigT1`?

Has it got something to do with `sigT`?

#### Julin S (Jun 13 2022 at 09:06):

And is the `&` same as the one in `sigT`?

``````Inductive sigT (A : Type) (P : A -> Type) : Type :=
existT : forall x : A, P x -> {x : A & P x}
``````

`Locate "{_ & _}".` didn't show anything.

#### Gaëtan Gilbert (Jun 13 2022 at 09:16):

`Locate "{ _ & _ }".` with spaces

#### Gaëtan Gilbert (Jun 13 2022 at 09:17):

Julin S said:

Which module is needed to have `proj_sigT1`?

Has it got something to do with `sigT`?

they probably meant `projT1`

Last updated: Oct 01 2023 at 19:01 UTC