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: May 28 2023 at 18:29 UTC