The following program gives the following error. Why? No reason is given.

```
From Equations Require Import Equations.
Inductive tree : Type :=
| node : list tree -> tree.
Equations? tree_eqdec : EqDec tree := {
| s, t => _
}
where list_tree_eqdec : EqDec (list tree) := {
| ss, ts => _
}.
(* Error: Cannot define tree_eqdec mutually with other programs *)
```

Also, how can I complete such a program (with Equations or otherwise)?

For the second question, `Fixpoint`

and `list_eqdec`

are enough (though I don't understand what termination checking is going on there).

That's a problem of elaboration, Equations tries to guard-check your definition a bit too early and expects to see `list_tree_eqdec`

be used in `tree_eqdec`

to build a nested fixpoint, hence the error. The following works:

```
Equations? tree_eqdec : EqDec tree := {
| node s, node t with list_tree_eqdec s t := {
| left _ => left _
| right _ => right _
}
}
where list_tree_eqdec : EqDec (list tree) := {
| nil, nil => left _
| cons x ss, cons y ts with tree_eqdec x y := _
{ | left _ := _ with list_tree_eqdec ss ts :=
{ | left _ => left _
| right _ => right _ }
| right _ => _
}
| _, _ => right _ }.
```

Then you can do:

```
Proof.
```

And it should show you the remaining subgoals.

Note that for recursive definitions like this, you should make the recursive calls apparent in the program, and not in the `Proof. ... Defined/Qed`

part.

So was the key to put in all of the recursive calls, and only then check whether the mutually recursive definition can be done?

Yes

Last updated: Sep 25 2023 at 12:01 UTC