## Stream: Equations devs & users

### Topic: Cannot define tree_eqdec mutally with other programs

#### James Wood (Jul 13 2022 at 09:51):

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

#### James Wood (Jul 13 2022 at 11:05):

For the second question, `Fixpoint` and `list_eqdec` are enough (though I don't understand what termination checking is going on there).

#### Matthieu Sozeau (Jul 13 2022 at 13:28):

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.

#### James Wood (Jul 13 2022 at 13:53):

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

#### Matthieu Sozeau (Jul 13 2022 at 14:08):

Yes

Last updated: Sep 25 2023 at 12:01 UTC