Hello, working with mutually recursive Fixpoint led me to find this interesting and strange behavior :

```
Inductive P (A : Type) : Type :=
| PI : A -> P A.
Arguments PI {A}.
Inductive E (A : Type) : Type :=
| EZ : A -> E A
| ES : P (E A) -> E A.
Arguments EZ {A}.
Arguments ES {A}.
Fixpoint occ_e {A} (e : E A) {struct e} : nat :=
match e with
| EZ _ => 0
| ES p => 1 + occ_p p
end
with occ_p {A} (p : P (E A)) {struct p} : nat :=
match p with
| PI e => 1 + occ_e e
end.
```

This simple mutually recursive Fixpoint on E and P simply counts the number of occurrences of ES and PI constructors along an element of E. But when trying to verify this function with Coq, I get the error message :

Recursive definition of occ_p is ill-formed.

In environment

occ_e : forall A : Type, E A -> nat

occ_p : forall A : Type, P (E A) -> nat

A : Type

p : P (E A)

e : E A

Recursive call to occ_e has principal argument equal to "e" instead of a subterm of "p".

Recursive definition is: "fun (A : Type) (p : P (E A)) => match p with

| PI e => 1 + occ_e A e

end".

I don't quite get the error message because it is straight forward that e is a subterm of p. Is it a wrong behavior from Coq or is the error message just bad ?

This is a classic problem with nested inductives, it doesn't understand fixpoints on the wrapper inductive `P`

which call a mutual fixpoint on `E`

. Instead you have to use a nested fixpoint:

```
Fixpoint occ_e {A} (e : E A) {struct e} : nat :=
match e with
| EZ _ => 0
| ES p =>
let fix occ_p {A} (p : P (E A)) {struct p} : nat :=
match p with
| PI e => 1 + occ_e e
end
in
1 + occ_p p
end.
Definition occ_p {A} (p : P (E A)) : nat :=
match p with
| PI e => 1 + occ_e e
end.
```

And if I want to use Equations for the job, is there a way to overcome this issue ?

It is a bit complicated because the solution of Gaëtan inline the definition, so you don't really define functions by mutual induction anymore. If you want to do as Gaëtan did, it should indeed make it easier as Equations enables to write it almost as above an inline it automatically:

```
From Equations Require Import Equations.
Equations occ_e {A} (e : E A) : nat :=
occ_e (EZ _) => 0;
occ_e (ES p) => 1 + occ_p p
where occ_p (p : P (E A)) : nat :=
occ_p (PI e) => 1 + occ_e e.
Equations occ_p (p : P (E A)) : nat :=
occ_p (PI e) => 1 + occ_e e.
Require Import Extraction.
Extraction occ_e.
```

But if you try to define them by mutual recursion as before, it fails

```
Fail Equations occ_e {A} (e : E A) : nat :=
occ_e (EZ _) => 0;
occ_e (ES p) => 1 + occ_p p
with occ_p {A} (p : P (E A)) : nat :=
occ_p (PI e) => 1 + occ_e e.
```

And I don't think you can cheat and use well-founded recursion because to the best of my knowledge, it is not supported for mutual definitions

There might be a less direct technique but I am not aware of it

AFAIK mutual fixpoints are only allowed with all struct arguments on the same inductive family. So if `P`

and `E`

were mutual. But in this particular case you will have a strict positivity check error.

This works as well

```
Inductive P (A : Type) : Type :=
| PI : A -> P A.
Arguments PI {A}.
Inductive E (A : Type) : Type :=
| EZ : A -> E A
| ES : P (E A) -> E A.
Arguments EZ {A}.
Arguments ES {A}.
Definition occ_p_gen {A} (f : A -> nat) (p : P A) :=
match p with
| PI e => 1 + f e
end.
Fixpoint occ_e {A} (e : E A) {struct e} : nat :=
match e with
| EZ _ => 0
| ES p => occ_p_gen occ_e p
end.
Definition occ_p {A} := occ_p_gen (@occ_e A).
```

Last updated: Jun 23 2024 at 05:02 UTC