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: Dec 07 2023 at 09:01 UTC