The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT inria.fr>]

Le lundi 18 juillet 2011 à 20:56 +0200, Julien Tesson a écrit :

> > BUT, sometimes it is not eliminated for typing reasons.
> > For instance in your list example, you cannot remove the "__", since
> > the constructor of a list always expect an argument.
> Actually, that's why I expected the whole type [list A] to be in Prop when 
> [A] is in Prop ...
> so that a list of "proofs" would be eliminated at extraction.
> That's why I am still curious to see an example where such a list would be 
> useful.

While the elements themselves do not carry any information, the list
does carry some information: its length! That's why it can't be in Prop
and you could probably devise a function that depends on the length of
the list but not on the values of its elements.

Now you could imagine that the extraction would produce a special
constructor for lists when the elements are in Prop. But that would
break polymorphism for functions length, map, and so on. That's why it
has to keep the standard constructor.

Best regards,

Guillaume