The Coq mailing list

[Micaela Mayero <Micaela.Mayero AT inria.fr>]

>Bonjour,
>
>A ma grande surprise je me suis rendu compte que les fonctions ayant
>pour type "Type->A"
>pouvaient etre appliquees a des objets de type "Set" tels que "nat",  ou
>des objets de type Prop tels que "O=O".
>
>Cela semble faire de "Set "et "Prop" des sous-types de "Type", alors que
>jusque -la je les voyais
>essentiellement comme des objets de type Type.


En fait il s'agit de la propriete de cumulativite et en particulier
la notation Prop correspond a une extension de la notation Type(i)
pour i=0.


>Du coup, je me demande si on aurait pas interet a formaliser d'abord
>dans la sorte "Type"
>avant de particulariser a Prop ou a Set.
>
>Par exemple, il est facile de montrer le lemme suivant:
>(A:Set)(a1,a2:A)a1=a2<->a1==a2.
>Intuitivement, il me semble que "eqT" est par consequent une stricte
>généralisation de "eq".
>
>De meme, je me demande pourquoi on ne definit pas le type "list" de la
>facon suivante:
>
>Inductive Tlist[T:Type]:Set := tnil:(Tlist T) | tcons:T->(Tlist
>T)->(Tlist T).
>
>ce qui permettrait de construire non seulement des listes d'entiers mais
>aussi des listes de propositions
>ou de types.
>
>Evidemment j'imagine qu'il doit y avoir quelque chose qui cloche mais je
>ne vois pas quoi.

Cette maniere de proceder est possible de par les modeles de Set, Prop et 
Type: toutes les definitions dans Set restent vraies dans Type [l'inverse
n'etant pas vrai pour l'instant (il suffit de considerer pour cela 
l'interpretation des fonctions de A->B dans Set et dans Type)].
 
Cependant, il y a un probleme majeur: le fait de definir le type list
dans Type permet de l'instancier avec nat et prop mais l'extraction
(pour nat) restera impossible. C'est un inconvenient important puisque
Set sert justement pour l'extraction (a l'heure actuelle; il me semble
qu'une extraction pour Type est a l'etude).

Cordialement,

Micaela Mayero.