The Coq mailing list

[AUGER Cedric <Cedric.Auger AT lri.fr>]

Le Mon, 02 May 2011 09:17:59 +0200,
Gert Smolka 
<smolka AT ps.uni-saarland.de>
 a écrit :

> Inductive zero : Type := .
> Check zero.
> ===> zero : Prop
> 
> Inductive one : Type := O : one.
> Check one.
> ===> one : Prop
> 
> Inductive two : Type := A : two | B : two.
> Check two.
> ===> two : Set
> 
> 1. Why does Coq ignore my wish to place the types
> in one of the universes Type ranges over?

It is due to the type hierarchy:
the universes of zero, one and two do not rely on other universes;
so, as in fact "Type" is a hidden Type identifier
(enable displaying of universe levels to see it) and is defined in
terms of successor and max of other universes in a basic environment
where only Set and Prop is defined, "zero" "one" and "two" must be of
sort Set or sort Prop.

It is not the case with lists:

Print list.
==>
Inductive list (A : Type (* Coq.Init.Datatypes.153 *))
            : Type (* max(Set, Coq.Init.Datatypes.153) *) :=
    nil : list A | cons : A -> list A -> list A

For nil: Argument A is implicit and maximally inserted
For cons: Argument A is implicit
For list: Argument scope is [type_scope]
For nil: Argument scope is [type_scope]
For cons: Argument scopes are [type_scope _ _]


> 
> 2. Why are zero and one put into Prop while
> two is put into Set?

Inductive types with exactly zero constructors (and a restricted class
of inductives with exactly one constructor) are non informative,
that is you can destructure them to produce informative values;
so for these inductives, there is no real difference between Set, Type
and Prop (modulo predicativity and type hierarchy), so it is simpler to
put them in Prop.

Quickly, one constructor inductives being in this class covers
inductives whose constructor only contains non informative contents
(i.e. Prop and zero constructors types + the one-constructor types of
the class they belong).

Inductive one: Type := O.
clearly belongs to this class, so destructing it to produce something
in Type won't hurt (and in fact in this particular case, won't be
usefull at all!).

Inductive exist (T: Sort0) (f: T -> Sort1): Sort2 :=
 ex_: forall t, f t -> exist T f.
doesn't belong to this class when Sort0 or Sort1 is Set or Type,
but when Sort0 and Sort1 are in Prop (or have no constructor or only
one constructor satisfying …), you can have Sort2 = Prop and
destructure it to produce something in Type.

Inductive exist (T: Prop) (f: T -> Prop): Prop :=
 ex_: forall t, f t -> exist T f.
Lemma x: forall T f, exist T f -> {t: T & f t}.
intros.
destruct H.
exists t.
exact H.
Defined.

I hope someone will complete this mail, as I am not competent in that
part of Coq.

> 
> -- Gert
> 
> 
> 
> 
>