The Coq mailing list

[Epiphanie <landeguy AT gmail.com>]

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