The Coq mailing list

[Thorsten Altenkirch <Thorsten.Altenkirch AT nottingham.ac.uk>]

Hi,

 

Frederik Forsberg investigated ind-ind types (IITs) in his PhD thesis.

https://personal.cis.strath.ac.uk/fredrik.nordvall-forsberg/thesis/thesis.pdf

 

Interestingly he couldn’t find a satisfying translation of IITs into ordinary inductive types. However, we have recently revisited his topic and found that at least for our standard example there is a translation if you have quotient types. I realize that this is not of much help in Coq,, though.

 

There are many interesting examples of induction-induction if you allow equality constructors – we call this quotient inductive inductive types. They are special cases of HITs or more precisely HIITs.

 

Cheers,

Thorsten

 

From: <coq-club-request AT inria.fr> on behalf of Matthieu Sozeau <mattam AT mattam.org>
Reply-To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Date: Wednesday, 15 November 2017 at 10:26
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Mutual inductive types with a predicate

 

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

This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please send it back to me, and immediately delete it. 

Please do not use, copy or disclose the information contained in this
message or in any attachment.  Any views or opinions expressed by the
author of this email do not necessarily reflect the views of the
University of Nottingham.

This message has been checked for viruses but the contents of an
attachment may still contain software viruses which could damage your
computer system, you are advised to perform your own checks. Email
communications with the University of Nottingham may be monitored as
permitted by UK legislation.