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?

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

Which module is needed to have `proj_sigT1`

?

Has it got something to do with `sigT`

?

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.

`Locate "{ _ & _ }".`

with spaces

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: Jun 25 2024 at 15:02 UTC