The Coq mailing list

[Bas Spitters <b.a.w.spitters AT gmail.com>]

> So why are they not included in Coq?


Are you really claiming that there is a detailed semantics for
CIC+IndInd and that all the meta-theory has been done?
I agree, it should work. However, I haven't seen the details yet.

On Mon, Jul 13, 2015 at 7:59 PM, Thorsten Altenkirch
<Thorsten.Altenkirch AT nottingham.ac.uk>
 wrote:
> 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.