The Coq mailing list

[Pierre Casteran <casteran AT labri.fr>]

Wojciech Moczydlowski wrote:
>   Hello,
>
> I'm a Ph. D. student in computer science and a newbie to Coq. During my 
> sessions with it I encountered the following behavior:
>
> If I declare
>
> Variable x : Type -> Type 
>
> in Coq 8.0
>
> then (x nat) typechecks, that is Check (x nat) says that (x nat) : Type. 
> This seems weird, for I do not see how to derive nat : Type from the 
> inference rules in the documentation on the webpage, which seem to be 
> necessary to derive (x nat) : Type. What am I missing?
>
> Thanks.




You can derive nat:Type thanks to the convertibility order and the 
conversion rule :

 I I denote by <= the convertibility order, you have Set <= Type(i) for
any i.
 The conversion rule allows you to derive

    nat : Set   Set <= Type(0)
    ------------------------
      nat : Type(0)


For instance, take the equality predicate :

eq : forall A : Type, A -> A -> Prop


Since you have also nat : Type,
you can consider equality between two natural numbers, like
eq nat 2 3.


Pierre

P.S.

 This example is treated pages 39 and 90 of the book by Bertot et al.









> Wojtek
>
>
>
>
>
> --------------------------------------------------------
> Bug reports: http://coq.inria.fr/bin/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>           http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club



--
Pierre Casteran,
LaBRI, Universite Bordeaux-I      |
351 Cours de la Liberation        |
F-33405 TALENCE Cedex             |
France                            |
tel : (+ 33) 5 40 00 69 31
fax : (+ 33) 5 40 00 66 69
email: Pierre . Casteran @ labri .  fr  (but whithout white space)
www: http://www.labri.fr/Perso/~casteran