The Coq mailing list

[brandon_m_moore AT yahoo.com]

----- Original Message -----
> From: Julien Tesson 
> <julien.tesson AT univ-orleans.fr>
> To: 
> coq-club AT inria.fr
> Cc:
> Sent: Tuesday, July 12, 2011 5:11 PM
> Subject: [Coq-Club] Prop, Set, Type and list
>
>( *
> Hi,
> I have found a behavior in Coq that I don't understand :
> If i define a type A in Prop like
> *)
>
> Definition A:= 1=1.
>
> (*
> and then typecheck the type (list A),
> *)
>
> Check (list A).
>
> (*
> then coq reply
> list A
>     : Set
> Why is it in Set and not in Prop ? or at least in Type, as list as type Type
> -> Type ?

list is explicitly declared as an inductive type in sort Type, so
there's no surprise it's not in Prop

http://coq.inria.fr/stdlib/Coq.Lists.List.html

It ends up in Set by sort-polymorphism:

http://coq.inria.fr/refman/Reference-Manual006.html#@default346

Usually, if an inductive type is declared in Type, then any application
actually gets the smallest sort that makes the inductive type
still legal (which Prop would also do here), but also makes it legal
to pattern match on the resulting type to produce results in Prop, Set,
and (any universe level in ) Type.

Lists have more than one constructor, so a version of lists in Prop
would only allow pattern matching with results in Prop.

Adam Chlipala's chapter on universes may helpful for understanding
the relationship between sorts, and just what Type actually is.
http://adam.chlipala.net/cpdt/html/Universes.html

> Furthermore I was thinking that it was not possible to build values in Set
using
> values in Prop
> but the following definition does :
> *)

That description is simplified too much to be helpful. Simple functions
like you wrote are fine. The only thing that may not be allowed is
pattern matching on a value in Prop (if the type of the match expression
is not also in Prop).

There is even an exception to this, for inductive types with only
a single constructor where all constructor arguments are also
in Prop. (one explanation is that pattern matching on a type like that
doesn't interfere with proof erasure).

file:///usr/local/share/doc/coq/html/refman/Reference-Manual006.html#singleton

> Definition f := fun x : A => x::nil.