The Coq mailing list

[Abhishek Anand <abhishek.anand.iitg AT gmail.com>]

Sorry, I accidentally deleted the context in my previous email. And it was an old thread.

So, here is the complete history of this thread in case you do not have it's previous emails.

https://www.dropbox.com/sh/v114yamyeejiz69/svnROUkS5J/IR.pdf

On Mon, Nov 11, 2013 at 11:26 PM, Abhishek Anand <abhishek.anand.iitg AT gmail.com> wrote:

How would one go about adding (simultaneous)Induction-Recursion to Coq?

Has someone already done some work in this direction?

We are in a situation where this trick does not work(because of jumping up universe levels).

(Even if it did work, the original Inductive recursive definitions seem much cleaner and easier to work with.)

I guess the result of http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.219.2442

that adding Induction-Recursion increases the proof-theoretic strength of a dependent type theory inductive types applies to Coq.

So, I would assume there is no way to encode "all" inductive-recursive definitions as Inductive definitions in Coq.

If induction-recursion can be added to Coq in a few days of work, I might prefer to do that instead of dealing with complicated approximations to the "naturally" inductive-recursive definitions that we are dealing with.

Could someone give us an idea about the work involved in implementing induction-recursion(IR) and where to start?

Also, since Prop was not accounted for in the consistency proof in the above paper, I wonder if Coq with Prop and IR is consistent.

(if not, is there a way to disable Prop?)

Thanks,

Abhishek and Vincent