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;
}.
```

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
```

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

~~See "placeholder variable renaming convention"~~

(spoke too quickly again, sorry)

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

Sounds like a de Bruijn bug…

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