The Coq mailing list

[Jean-Christophe Filliatre <Jean-Christophe.Filliatre AT lri.fr>]

> Why is "nat" defined to be of type "Set"? 
> 
> In the file 
>   V6.2/lib/coq/theories/SETS/Integers.v 
> there is a proof of the fact that the natural numbers (why is the file
> called "Integers.v"?) is an infinite set. But a lot of energy is
> expended to first set up a bijection between "nat" and "Nat" of type
> "Type", so that we can now work with the "Ensemble" of natural
> numbers.

Actually, it could not be stated this  way: natural numbers were first
defined, and it was natural to  define them in sort  Set since we want
them  to be   informative and we   want  to  do extraction  on  proofs
involving natural numbers (proofs of gcd, euclidean quotient, etc)

Sets were defined  independently, and  then  it was natural  to define
them in sort Type   in order to  be able  to define  sets of sets  for
instance (I think that  it is the  main reason; sombebody will correct
me if I am wrong).

The proof  that natural numbers are  infinite could  have used natural
numbers defined directly in sort Type, as  you suggest it, but I think
that the  authors of this  development wanted  to re-use some theorems
already defined  on the existing natural  numbers, and  didn't want to
prove them once more with natural numbers in sort Type.

> It seems that if we originally defined
>   Inductive Nat : Type := NatO : Nat | NatS : Nat -> Nat.
> this proof at least would have been much easier. Are there other
> things that you would then not have been able to do?

Yes, extraction for instance.

I hope this will answer your question.
Best regards,
-- 
Jean-Christophe FILLIATRE
  
mailto:Jean-Christophe.Filliatre AT lri.fr
  http://www.lri.fr/~filliatr