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