The Coq mailing list

[Eddy Westbrook <westbrook AT kestrel.edu>]

All,

I thought that induction-recursion greatly increases the proof-theoretic strength of a system, because it allows building an inductive encoding of the types of the system in the system itself, which in turn allows one to build a model of the system (without I-R). This makes it seem to me like this is not a trivial extension...

Is this not the case here? Maybe I do not understand the difference between induction-recursion and what you are calling induction-induction?

-Eddy

On Jul 14, 2015, at 6:01 AM, Fredrik Nordvall Forsberg <fredrik.nordvall-forsberg AT strath.ac.uk> wrote:

Hi Bas,

On 13/07/15 19:49, Bas Spitters wrote:

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.

The classical set-theoretic semantics of MLTT + inductive-inductive
definitions should extend to an impredicative Prop very
straightforwardly. However, you are right that there are no proofs of
e.g. normalization for this theory (or for induction-recursion, for that
matter). I would expect this to work with no problems.

Best regards,
Fredrik

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

-- 
Fredrik Nordvall Forsberg,
Department of Computer and Information Sciences,
University of Strathclyde.
The University of Strathclyde is a charitable body, registered in
Scotland, with registration number SC015263.