The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

[previous messages inserted into bottom]

I would not be surprised if it took much longer than a few days, but I've never seriously worked on Coq.  I'd start by looking at where and how "Inductive" is defined.  You could also look at the changes made in https://github.com/barras/coq/tree/hit, where Bruno Barras implements a "with paths := ..." and "fixmatch" primitives as a start of higher inductive types.  I suspect that the code you need to touch is similar to/near the code that "with paths :=" modifies.

Some issues to watch out for with trying to add induction-recursion to Coq:

- Coq doesn't have "mutual" blocks, and "fix" is a special keyword that lets you mention the name of the function in it's body.  So you'll probably need to pull some hackery to get the types of the constructors to be allowed to mention the fixpoint, which can't be defined until the inductive definition is meaningful.

- Unlike Agda, Coq's termination checker is syntactic and simple; it only permits structural recursion (or well-founded recursion, if you write your own proofs), and requires that inductives be strictly positive.  For example, you can't typecheck [Inductive Bad := Build_bad : (Bad -> unit) -> Bad.]; it errors with "Error: Non strictly positive occurrence of "Bad" in "(Bad -> unit) -> Bad"."  How do you plan to extend this rule to induction-recursion?  I probably shouldn't be allowed to do "Inductive Bad := Build_bad : bad_fix -> Bad with Fixpoint bad_fix : Type := Bad -> unit.] or something silly like that.  So either you'll need to write a termination checker for Coq, which I think goes against it's philosophy, or you'll need a simple syntactic check that you can use to ensure termination and positivity.   (I'm not sure what exactly goes wrong if you allow non-positivity... perhaps it gives you some kind of impredicativity?)

- The upcoming version of Coq will mostly likely have full universe polymorphism/typical ambiguity.  Are there any subtleties to inferring and assigning universes in the presence of induction-recursion?

However, I'd be very, very interested to have induction recursion in Coq, especially if it meshes well with Bruno's higher inductive types; I've been itching to try out my understanding of computation rules for higher inductive types with defining univalent universes by higher induction recursion, and seeing if I could formalize a computational interpretation of univalence that way.  (I also think it'd be a nice feature to have in general.)  But I'd be surprised if you could do it in a few days.

With regard to Prop and IR, I'd be surprised if there was an inconsistency there, as long as the IR didn't allow you to do large elimination out of prop, or anything like that.  At worst, you could just forbid Prop from showing up in your inductive-recursive definitions (just do an after-the-fact check to make sure the identifier doesn't show up in the delta normal form), and then I'd be very surprised if you could get a contradiction from this.

There is no way to disable prop, currently; for one, [eq] is in [Prop] and many of the tactics will raise errors or anomalies if you don't have [eq : forall A, A -> A -> Prop], [True : Prop], [False : Prop], etc.  (I tried putting them in Set/Type, for HoTT, and ran into errors.)

I hope this helps,

Jason

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

On Thu, Aug 29, 2013 at 7:31 PM, Andrew Cave <acave1 AT cs.mcgill.ca> wrote:

The standard trick to encode IR in Coq is to index by the result you
want to compute.

Inductive Foo : nat -> Set :=
| fooA (n: nat) : Foo n
| fooPlus n1 (f1: Foo n1) n2 (f2: Foo n2) : Foo (n1 + n2)
| fooWeird n1 (f1: Foo n1) n2 (f2: Foo n2) (f3: Foo 10) : Foo (n1 + n2 + 10).

Now {n : nat & Foo n} corresponds to your old Foo. This trick goes
quite far, with the caveat that if you're using it to compute Types
then you have to go up a universe level. See e.g.
www.cs.ru.nl/~venanzio/publications/induction_recursion.ps

On Thu, Aug 29, 2013 at 6:38 PM, t x <txrev319 AT gmail.com> wrote:
> Jason: http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.AgdaVsCoq
> agrees with you.
>
> Rui: interesting, I think this suffices.
>
> 
> On Thu, Aug 29, 2013 at 9:43 PM, Rui Baptista <rpgcbaptista AT gmail.com>
> wrote:
>>
>> What about:
>>
>> Inductive Foo' :=
>> | fooA (n: nat)
>> | fooPlus (f1: Foo') (f2: Foo')
>> | fooWeird (f1: Foo') (f2: Foo') (f3: Foo').
>>
>> Fixpoint evalFoo f :=
>> match f with
>> | fooA n => n
>> | fooPlus f1 f2 => (evalFoo f1 ) + (evalFoo f2)
>> | fooWeird f1 f2 f3 => (evalFoo f1) + (evalFoo f2) + (evalFoo f3)
>> end.
>>
>> Definition Foo :=
>>   {f1 : Foo' | forall f2 f3 f4, f1 = fooWeird f2 f3 f4 -> evalFoo f4 =
>> 10}.
>
> On Thu, Aug 29, 2013 at 5:25 PM, Jason Gross <jasongross9 AT gmail.com> wrote:

I believe this is called induction-recursion, and I believe that agda supports it, while coq does not.  You could try implementing it in OCaml and asking the coq-devs to merge your branch, though that might be quite an undertaking.

I don't know of any work-arounds, though I haven't explored it much.

-Jason

On Aug 29, 2013 4:48 PM, "t x" <txrev319 AT gmail.com> wrote:

Hi,

  Here is my minimal failure case: https://gist.github.com/anonymous/6383213

  What I want is to simultaneouly define "Inductive Foo: Set" and "Fixpoint evalFoo: Foo -> nat"

  such that the Inductive can have a term that involves evalFoo (in particular, a proof that evalFoo gets a certain value).

Can I do this in Coq? (If so, how, if not, what is the closest alternative).

Thanks!