Stream: Coq users

Topic: "recursive-recursive" definitions

Ali Caglayan (May 26 2020 at 14:35):

I asked a question on gitter about coq's ability to specify "recursive-recursive" definitions like the following:

Fixpoint A (n : nat) : Type
with B {n : nat} : A n -> Type.

@Gaëtan Gilbert gave a possible definition of "recursion-recursion" as: when you have some mutual fixpoints where one appears in the type of the other.

With mutual fixpoints there is a trick we can do to reduce it down to a single fixpoint. The standard example being the mutually defined odd and even properties of nat. We can define a map oddeven that decides both of these properties in a product. The obvious generalization to "recursion-recursion" here is that we can replace products with sigma types. This would allow my original example to be written as

Fixpoint AB (n : nat) : {A : Type & A -> Type}.

AFAIK coq doesn't have support for these kinds of mutual fixpoints. Would it be possible to add or is there a notable difficulty that would need to be overcome?

Janno (May 26 2020 at 16:56):

Do you have a more concrete example for this? I can't quite see why the signature you propose cannot be implemented.

Ali Caglayan (May 27 2020 at 14:23):

@Janno Well when I give coq 8.11

Fixpoint A (n : nat) : Type
with B {n : nat} : A n -> Type.

I get the following message:

The reference A was not found in the current
environment.

I get the same message if I set up a fix expression:

Check (fix A (n : nat) : Type := _
with B (n : nat) : A -> Type := _
for A : nat -> Type).

but my point is that you can do what I want by defining

Fixpoint AB (n : nat) : {A : Type & A -> Type}.

and then projecting out the definitions of A and B.

So what I am asking is: Is it possible to modify fix expressions in coq so that types appearing later in the mutual fixpoint can depend on types defined earlier in the fixpoint. Currently, mutual fixpoints don't need to be declared in any particular order since there are no dependencies between them. For example odd and even can be defined like:

Fixpoint even n :=
  match n with
  | O => Unit
  | S n => odd n
  end
with odd n :=
  match n with
  | O => Empty
  | S n => even n
end.

or like

Fixpoint odd n :=
  match n with
  | O => Empty
  | S n => even n
  end
with even n :=
  match n with
  | O => Unit
  | S n => odd n
  end.

But if we allow dependencies, the order might need to be checked.

Ali Caglayan (May 27 2020 at 14:24):

By dependency I mean that the type of odd does not depend on the type of even.

Janno (May 27 2020 at 14:24):

Ooh, now I understand. So your example works, it's just inconvenient to state it that way?

Ali Caglayan (May 27 2020 at 14:25):

Yes, and the example I want to try is much more complicated which would make it rather inconvenient to bundle up into a sigma type or record.

Last updated: Oct 03 2023 at 02:34 UTC