The Coq mailing list

[Gabriel Scherer <gabriel.scherer AT gmail.com>]

It's precisely when you have universes indexed by naturals that
induction-recursion becomes useful. I think that for the purpose of
convincing oneself that something is solid, one could decide to work
only a bounded number of universe levels (say 3 universes; 2 universes
is not quite enough to seriously study cumulativity for example), but
I'm not sure how to do that without duplicating the inductive
definition (which is a no-no).

On Tue, Nov 12, 2013 at 10:49 AM, Jason Gross 
<jasongross9 AT gmail.com>
 wrote:
> Bruno told me about his work on CIC in set theory in Coq, at
> https://github.com/barras/cic-model.  See also
> http://coq.inria.fr/pylons/pylons/contribs/view/CoqInCoq/v8.4.  Univalence
> for free (http://www.emn.fr/z-info/ntabareau/univalence_for_free/) might
> also be relevant, though I think it's an internalization of Coq in Coq aimed
> at computation rather than metatheory.  I don't know how much each of these
> treats universes, if at all.
>
> -Jason
>
>
> On Tue, Nov 12, 2013 at 4:27 AM, Gabriel Scherer 
> <gabriel.scherer AT gmail.com>
> wrote:
>>
>> Seconded. I would be very interested in inductionr-recursion (I've had
>> to give up a formal development on the metatheory of a Martin-Löf type
>> theory with universes because of it's absence; have people done that
>> in Coq?), but I would guess it's rather one year of work than a few
>> days or weeks.
>>
>> On Tue, Nov 12, 2013 at 10:11 AM, Jason Gross 
>> <jasongross9 AT gmail.com>
>> wrote:
>> > [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!
>> >
>> >
>> >
>
>