coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Gabriel Scherer <gabriel.scherer AT gmail.com>
- To: Jason Gross <jasongross9 AT gmail.com>
- Cc: Abhishek Anand <abhishek.anand.iitg AT gmail.com>, Andrew Cave <acave1 AT cs.mcgill.ca>, t x <txrev319 AT gmail.com>, Rui Baptista <rpgcbaptista AT gmail.com>, coq-club <coq-club AT inria.fr>, vincent rahli <vincent.rahli AT gmail.com>
- Subject: Re: [Coq-Club] co-defining an Inducive + a Fixpoint
- Date: Tue, 12 Nov 2013 10:27:22 +0100
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!
>
>
>
- Re: [Coq-Club] co-defining an Inducive + a Fixpoint, Abhishek Anand, 11/12/2013
- Message not available
- Re: [Coq-Club] co-defining an Inducive + a Fixpoint, Abhishek Anand, 11/12/2013
- Message not available
- Re: [Coq-Club] co-defining an Inducive + a Fixpoint, Jason Gross, 11/12/2013
- Re: [Coq-Club] co-defining an Inducive + a Fixpoint, Gabriel Scherer, 11/12/2013
- Re: [Coq-Club] co-defining an Inducive + a Fixpoint, Bas Spitters, 11/12/2013
- Re: [Coq-Club] co-defining an Inducive + a Fixpoint, Jason Gross, 11/12/2013
- Re: [Coq-Club] co-defining an Inducive + a Fixpoint, Gabriel Scherer, 11/12/2013
- Re: [Coq-Club] co-defining an Inducive + a Fixpoint, Matthieu Sozeau, 11/12/2013
- Re: [Coq-Club] co-defining an Inducive + a Fixpoint, Abhishek Anand, 11/15/2013
- Re: [Coq-Club] co-defining an Inducive + a Fixpoint, Matthieu Sozeau, 11/12/2013
- Re: [Coq-Club] co-defining an Inducive + a Fixpoint, Gabriel Scherer, 11/12/2013
- Re: [Coq-Club] co-defining an Inducive + a Fixpoint, Gabriel Scherer, 11/12/2013
Archive powered by MHonArc 2.6.18.