Stream: Equations devs & users

Topic: The variable was not found

Cong Ma (Mar 02 2023 at 17:37):

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. *)

Paolo Giarrusso (Mar 02 2023 at 20:36):

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.

Paolo Giarrusso (Mar 02 2023 at 20:38):

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.

Paolo Giarrusso (Mar 02 2023 at 20:41):

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?

Matthieu Sozeau (Mar 03 2023 at 06:10):

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

Cong Ma (Mar 03 2023 at 19:30):

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

Last updated: May 28 2023 at 18:29 UTC