## Stream: Equations devs & users

### Topic: Recursive definition is ill-formed.

#### Cong Ma (Mar 03 2023 at 20:53):

I have the following Equations definition, and Coq doesn't like the call `AA a4 a5`, and print error message(the variable names are confusing because of renaming done by Equations)

``````Recursive call to AA has principal argument equal to "a0" instead of one of the following variables:  "b" "b0" "c".
``````

Not sure why this definition is not accepted. I think it is fine because a5 of type A is a substructure of c1 of type C, which is a substructure of b1 of type B, which is a substructure of a2 of type A. So the recursion is well-founded. So what does the error message mean?

``````Inductive A : Type :=
| A_mk : B → A
with B : Type :=
| B_mk : C -> B
with C : Type :=
| C_cons : A → C → C
.

Equations AA (a1 : A) (a2 : A) : A by struct a2 := {
AA a1 (A_mk b1) => A_mk (AB a1 b1);
} where AB : A -> B -> B := {
AB a3 (B_mk c1) => B_mk (AC a3 c1);
} where AC : A -> C -> C := {
AC a4 (C_cons a5 c2) => C_cons (AA a4 a5) c2;
}.
``````

#### Yann Leray (Mar 03 2023 at 21:56):

I tried to minimise the example, I got this : (2 do work)

``````Inductive A : Type := A_mk : B -> A
with B : Type := B_mk : C -> B
with C : Type := C_mk : A -> C.

Fixpoint AA (a : A) {struct a} : False :=
let '(A_mk b) := a in AB b
with AB b :=
let '(B_mk c) := b in AC c
with AC c :=
let '(C_mk a) := c in AA a.

From Equations Require Import Equations.

Equations fA (a : A) : False := {
fA (A_mk b) => fB b;
} where fB : B -> False := {
fB (B_mk c) => fC c;
} where fC : C -> False := {
fC (C_mk a) => fA a;
}.
``````

The most surprising is that the recursive definition in the error message isn't even well-typed :

``````fun a : A =>
match a with
| A_mk b =>
(fun b0 : B => match b0 with
| B_mk _ =>
fun c0 : C => match c0 with
| C_mk a0 => fA a0
end
end) b
end
``````

#### Paolo Giarrusso (Mar 03 2023 at 23:31):

This reminds me of the shadowing bug from a couple weeks (?) ago in this stream

#### Paolo Giarrusso (Mar 03 2023 at 23:34):

See "placeholder variable renaming convention"

#### Paolo Giarrusso (Mar 03 2023 at 23:39):

(spoke too quickly again, sorry)

#### Yann Leray (Mar 04 2023 at 17:21):

Also, if we correct the definition in the error message (by adding the missing argument `c` to the inner-most lambda, taken from the currently ignored argument of `B_mk`), it is accepted

#### Matthieu Sozeau (Mar 06 2023 at 07:04):

Sounds like a de Bruijn bug…

#### Cong Ma (Mar 07 2023 at 04:43):

Thanks for confirming. I submitted a GitHub issue at https://github.com/mattam82/Coq-Equations/issues/542

Last updated: Jul 13 2024 at 03:01 UTC