Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Records and Inductive definitions

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Records and Inductive definitions


Chronological Thread 
  • From: Petar Maksimovic <petar.maksimovic AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Records and Inductive definitions
  • Date: Thu, 1 Oct 2015 15:12:55 +0200
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=petar.maksimovic AT gmail.com; spf=Pass smtp.mailfrom=petar.maksimovic AT gmail.com; spf=None smtp.helo=postmaster AT mail-wi0-f174.google.com
  • Ironport-phdr: 9a23:p7fynhR2wH10ywSyYK0ev38xqNpsv+yvbD5Q0YIujvd0So/mwa64YBKN2/xhgRfzUJnB7Loc0qyN4/ymBzZLv8/JmUtBWaIPfidNsd8RkQ0kDZzNImzAB9muURYHGt9fXkRu5XCxPBsdMs//Y1rPvi/6tmZKSV3BPAZ4bt74BpTVx5zukbvip9uNOU4W3XKUWvBbElaflU3prM4YgI9veO4a6yDihT92QdlQ3n5iPlmJnhzxtY+a9Z9n9DlM6bp6r5YTGfayQ6NtRrtBST8iLmod5cvxtBCFQxHcyGEbVzAunwZBGUDg5RLhX5L2rCrx/r5l1TWTJ4vzRLMvWDGl8aZgYBDtgSYDcTU+9TeE2YRLkKtHrUf59FREyInObdTNOQ==

Dear Michael,

I don't think that is the problem leading to the error message,
because this works:

Inductive T : Type :=
| T_main : list T -> T.

and something like this also works:

Record list_singleton (T : Type) := {lT :> list T; n : nat; cond : n > 37}.

Inductive T : Type :=
| T_main : list_singleton T -> T.

I think that the length condition that I had (length lT = 1) is
causing the issue, but I don't quite understand why.

Best regards,
Petar

On 1 October 2015 at 14:59, Soegtrop, Michael
<michael.soegtrop AT intel.com>
wrote:
> 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



Archive powered by MHonArc 2.6.18.

Top of Page