The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Dear all,

  I've been thinking of adding IR to Coq for a while, but mainly thought about
the implementation issues (representation of mutual inductive/fixpoints and 
positivity). I suspect it would not be too long to add it, as the change would
mainly impact the kernel entry point for declarations of inductives and not
change the representation of terms. Basically adding I and f would 
simultaneously
introduce an inductive and a constant in the environment, they would just
have to be grouped to allow simultaneous checking. The big engineering issue 
will
be positivity/termination checking indeed. I don't have time to implement 
this now, but if you're willing to try it I'd be happy to help you Abhishek.
My (always optimistic) gut feeling is at least 6 weeks of full-time work for 
one person not knowing the code previously, with safety checking taking most 
of the time (and intelligence). I'm not very familiar with the theoretical 
justifications, surely Dybjer's and Barras's work is reusable. One thing that 
I'm not sure about is what form the fixpoints can take, i.e. do you need to
recognize a specific fix-match pattern or can allow free-form terms.

  On the related problem of encoding IR with inductives only, I guess with
polymorphic universes you will be able to apply the translation always but
of course you'll still be bumping the universe level, and indeed the 
translation
is heavy. Looking at it closely, it doesn't change the universe level if 
your inductive is in Set and you have impredicative set though, right?
  I don't know about Prop and IR, but Capretta uses Prop in his encoding and
I don't see why it would cause any problem (but you never know until it's 
been proved :).

  The universe polymorphism branch supports the use of a polymorphic
identity type instead of eq : A -> A -> Prop (in principle, in the Coq code). 
E.g., I adapted discriminate etc to work with a different eq type (perhaps not
completely, it's untested). B. Barras also has some prototypical work on 
making 
the base logic parametric in Coq, i.e. declaring type classes for different 
logics, intuitionistic, classical, in Prop, in Set/Type. The tactics using 
e.g. True would now take the truth value of the current Logic instance in the 
context, which might happen to be unit. 

  Given the interest on this and other features, a Coq Implementors Meeting 
seems
to really be in order!

Cheers,
-- Matthieu

On 12 nov. 2013, at 11:02, Gabriel Scherer 
<gabriel.scherer AT gmail.com>
 wrote:

> 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!
>>>> 
>>>> 
>>>> 
>> 
>>