The Coq mailing list

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

Hi Jason,

afaik there is no easy way to do this. I discussed this recently with Frederik Forsberg, whose PhD thesis is a good source of information about induction-induction. See section 5.3.

You can approximate inductive-inductive definition using a similar technique as for induction-recursion but you don’t get the right eliminator. E.g. If you define a family A : Set, B : A -> Set you expect that the elimination operators have the form

elim-A : (X : Set)(Y : X -> Set) -> … -> A -> X

elim-B : (X : Set)(Y : X -> Set) -> … -> (a : A) -> B a -> Y (elim-A X Y … a)

the problem here is the dependency of the 2nd operator on the first.

However, unlike the problem with univalence and extensionality this one is relatively easy to fix as Agda shows. Inductive-inductive definitions have a straightforward operational semantics and also it is no problem to derive eliminators and recursors for them. So why are they not included in Coq?

Thorsten

From: Jason Gross <jasongross9 AT gmail.com>
Reply-To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Date: Sunday, 12 July 2015 04:58
To: coq-club <coq-club AT inria.fr>
Subject: [Coq-Club] Faking induction-induction in Coq?

Hi,

Is there a (known) way to fake induction-induction in Coq?

Abhishek mentioned http://www.cs.ru.nl/~venanzio/publications/induction_recursion.ps last year as a way of faking induction-recursion in Coq.  I'm curious, in particular, about how to define well-typed syntax for dependent type theory in Coq, and, more specifically, one that supports a quotation function, which sends any syntactic term to a syntactic representation of that syntax, i.e., sends (app 'S' '0'), the syntax representing the numeral 1, to (app (app 'app' "S") "0").

Thanks,

Jason

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.