The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Hi,

  What you’re trying to formalize are known as inductive-inductive types, when an inductive can depend through its indices on a previous inductive in the same mutual block, and constructors of later inductives can refer to constructors of the previous inductives (the exact order constraints varies, Agda implements this in a more flexible way for example). There is an experimental branch IR on my GitHub [1] which implements those, based on Coq 8.7. You have to write the eliminators by hand though and consistency is not proven for this version of the calculus yet. Maybe there are other non ind-ind encodings of your types that solve your problem though. 

[1] https://github.com/mattam82/coq/tree/IR?files=1

Best,

— Matthieu

Le mer. 15 nov. 2017 à 10:23, Merlin Göttlinger <megoettlinger AT gmail.com> a écrit :

Hi,

what I want to implement is a more complicated version of this:

Inductive A :=

| a1 : nat -> A

| a2 : nat -> A

| a3 : B -> A -> A

with B :=

     | b1 : nat -> B

     | b2 : { ae : A | P ae} -> B

with P : A -> Prop :=

     | pa3 : forall b a, P a -> P (a3 b a)

     | pa1 : forall n, P (a1 n).

However that is rejected by coq (8.6.1) with the error The reference A was not found in the current environment. at the Type of P.

Why is that the case?

One way I found to avoid this is to "bake the predicate into the type":

Inductive A : bool -> Set :=

| a1 : nat -> A true

| a2 : nat -> A false

| a3 {b} : B -> A b -> A b

with B : Set :=

     | b1 : nat -> B

     | b2 : A true -> B.

But this forces you to wrap and unwrap A everywhere where you do not care about the predicate.

Is there a better way?

Cheers,

Merlin