coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: "Soegtrop, Michael" <michael.soegtrop AT intel.com>
- To: "coq-club AT inria.fr" <coq-club AT inria.fr>
- Subject: RE: [Coq-Club] Records and Inductive definitions
- Date: Thu, 1 Oct 2015 12:59:02 +0000
- Accept-language: de-DE, en-US
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=michael.soegtrop AT intel.com; spf=Pass smtp.mailfrom=michael.soegtrop AT intel.com; spf=None smtp.helo=postmaster AT mga02.intel.com
- Ironport-phdr: 9a23:ddnf5xKynGNhgD2v8dmcpTZWNBhigK39O0sv0rFitYgULf3xwZ3uMQTl6Ol3ixeRBMOAu64C1bCd7fmocFdDyKjCmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TWM5DIfUi/yKRBybrysXNWC04LpjavsotX6WEZhunmUWftKNhK4rAHc5IE9oLBJDeIP8CbPuWZCYO9MxGlldhq5lhf44dqsrtY4q3wD86Fpy8kVG679ZuEzSaFSJDUgKWE8osPx/1GXRgyWo3AYT28+kxxSAgGD4gusDbnrtS6v/NF61SaGJ8ruCfgRWD+i5qpvAle8jSYMNzc09CfMjcF/kLhcuDqgoQByx8jfZ4TDZ6k2Rb/UYd5PHTkJZc1WTSEUWo4=
Dear Petar,
you wrote that T can be a list of itself, which justifies this error message.
Maybe you meant this (which does work):
Record list_singleton (T : Type) := {lT :> list T; cond : length lT = 1}.
Inductive SomeInd (T : Type) :=
| T_main : list_singleton T -> SomeInd T.
Best regards,
Michael
-----Original Message-----
From:
coq-club-request AT inria.fr
[mailto:coq-club-request AT inria.fr]
On Behalf Of Petar Maksimovic
Sent: Thursday, October 01, 2015 2:28 PM
To:
coq-club AT inria.fr
Subject: Re: [Coq-Club] Records and Inductive definitions
Any comments? From the developer team, in particular, perhaps? :)
Cheers,
Petar
On 28 September 2015 at 17:27, Petar Maksimovic
<petar.maksimovic AT gmail.com>
wrote:
> Hello everyone,
>
> Why is it not possible to do the following in Coq:
>
> Record list_singleton (T : Type) := {lT :> list T; cond : length lT = 1}.
>
> Inductive T : Type :=
> | T_main : list_singleton T -> T.
>
> It fails with the error message: Error: Non strictly positive
> occurrence of "T" in "list_singleton T -> T".
>
> I feel that this should be able to go through, since
>
> | T_main : list T -> T
>
> would go through, and I am simply putting an extra condition on the
> lists that I allow.
>
> What I would ultimately want is to be able to use Coq's finite maps in
> constructors, somewhat like this:
>
> Module FMnat := FMapWeakList.Make(Nat_as_OT). (or FMapFullAVL, for
> that matter)
>
> Definition FMap := FMnat.t.
>
> Inductive T : Type :=
> | T_main : FMap T -> T.
>
> and I believe that the problem (in this case) boils down to a
> restriction condition in the underlying record definition of slist, on
> which FMapWeakList is based, therefore the simplified example above.
>
> Any ideas, including how I could approach this differently, are very
> appreciated.
>
> Thank you,
> Petar
>
> P.S. The following does not go through:
>
> Inductive T : Type :=
> | T_main : forall T', list_whatever T T' -> T with Record
> list_whatever (T T' : Type) := {lT :> list T; whatever : T'}.
>
> with the error message: Error: Cannot handle mutually (co)inductive
> records, whereas
>
> Record list_whatever (T T' : Type) := {lT :> list T; whatever : T'}.
>
> Inductive T : Type :=
> | T_main : forall T', list_whatever T T' -> T.
>
> goes through just fine. Why is this so?
Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Prof. Dr. Hermann Eul
Chairperson of the Supervisory Board: Tiffany Doon Silva
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928
- Re: [Coq-Club] Records and Inductive definitions, Petar Maksimovic, 10/01/2015
- RE: [Coq-Club] Records and Inductive definitions, Soegtrop, Michael, 10/01/2015
- Re: [Coq-Club] Records and Inductive definitions, Petar Maksimovic, 10/01/2015
- Re: [Coq-Club] Records and Inductive definitions, Pierre-Marie Pédrot, 10/01/2015
- Re: [Coq-Club] Records and Inductive definitions, Epiphanie, 10/01/2015
- Re: [Coq-Club] Records and Inductive definitions, Petar Maksimovic, 10/01/2015
- RE: [Coq-Club] Records and Inductive definitions, Soegtrop, Michael, 10/01/2015
- Re: [Coq-Club] Records and Inductive definitions, Petar Maksimovic, 10/05/2015
- RE: [Coq-Club] Records and Inductive definitions, Soegtrop, Michael, 10/01/2015
- Re: [Coq-Club] Records and Inductive definitions, Petar Maksimovic, 10/01/2015
- RE: [Coq-Club] Records and Inductive definitions, Soegtrop, Michael, 10/01/2015
- Re: [Coq-Club] Records and Inductive definitions, Petar Maksimovic, 10/01/2015
- RE: [Coq-Club] Records and Inductive definitions, Soegtrop, Michael, 10/01/2015
Archive powered by MHonArc 2.6.18.