The Coq mailing list

[Petar Maksimovic <petar.maksimovic AT gmail.com>]

Thanks Pierre-Marie and Epiphanie,

Vectors would work if my example hadn't been somewhat
under-illustrative. What I would really like is

Record list_noDup (T : Type) := {lT :> list T; cond: noDup lT}.

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

but for that I think I'll need some sort of workaround.

Cheers,
Petar

On 1 October 2015 at 15:59, Epiphanie 
<landeguy AT gmail.com>
 wrote:
> Dear Petar,
>
> Strictly positive occurrence states that you are not allowed to create a
> type from a function that takes an argument of this type (the reason for
> this is obvious if you consider omega in lambda calculus)
> So I believe the reason it does not work is that cond has the type T -> list
> T -> Prop that guarantees that your list is a singleton.
> So cond cannot be in the constructor of the type you want to define, T
>
> I am not sure I understand exactly what you want to do, but it seems like
> you want to map list of one element onto the type of this element
> In which case, you could try to do a coercion between the two
>
> Cheers,
> Epiphanie
>
>
> Le 1 octobre 2015 15:12:55 UTC+02:00, Petar Maksimovic
> <petar.maksimovic AT gmail.com>
>  a écrit :
>>
>> 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