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