Can someone explain why the first Equations is accepted by Coq but not the second one? Please ignore what the equations actually means as they are minimal examples.

Section ex1.

Equations plus_two (n : nat) : nat := {

plus_two 0 => 2;

plus_two (S n) => plus_one (plus_two n)

} where plus_one (n : nat) : nat := {

plus_one 0 => 1;

plus_one (S n) => S (plus_one n)

}.

End ex1.

(* ok *)

Section ex2.

Equations plus_two (n : nat) : nat := {

plus_two 0 => 2;

plus_two (S n) => plus_one n

} where plus_one (n : nat) : nat := {

plus_one 0 => 1;

plus_one (S n) => S (plus_one n)

}.

End ex2.

(* Error: The variable plus_one was not found in the current environment. *)

It seems a bug! See the variant below (using modules). Note the example as given is _not_ valid — it should fail with `plus_two already exists.`

(just paste the first example twice to see) — but that's not the problem.

```
From Equations Require Import Equations.
Module ex1.
Equations plus_two (n : nat) : nat := {
plus_two 0 => 2;
plus_two (S n) => plus_one (plus_two n)
} where plus_one (n : nat) : nat := {
plus_one 0 => 1;
plus_one (S n) => S (plus_one n)
}.
End ex1.
(* ok *)
Module ex2.
Equations plus_two (n : nat) : nat := {
plus_two 0 => 2;
plus_two (S n) => plus_one n
} where plus_one (n : nat) : nat := {
plus_one 0 => 1;
plus_one (S n) => S (plus_one n)
}.
End ex2.
```

I've reproduced with Coq 8.16.0 and Coq-Equations 1.3+8.16; you should probably file a bug report on coq-equations' github repository.

but I'm just a fellow user — I say "should" just so this isn't forgotten even _if_ the author @Matthieu Sozeau is too busy right now — maybe unless he has a quicker answer?

It might be an issue due to the fact that in the second case it’s not mutually or nested recursive

Thanks, that should be it. We could probably use a better error message here.

Last updated: May 19 2024 at 16:02 UTC