The Coq mailing list

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

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