The Coq mailing list

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

On 04/08/2014 01:59, Jonathan wrote:
> It would certainly be nice if the rule was simply that
> anything at all that contains no information can be case analyzed in any
> context.  I would even argue that things like "False \/ P" should be
> case analyzable in any context - because (and, of course) it can be
> turned into P by use of assert, applying a lemma or a rewrite.

How can you argue that a value of type "False \/ P" contains no 
information? There are two constructors! If we were to follow your line 
of thoughts, then, whatever the inductive type T, values of that type 
should be destructible in any context, because we are always able to 
create a function from T to True and values of type True are known to be 
destructible in any context.

The important point, both in your earlier example and in that "False \/ 
P" case, is that, as a user, you tell the system how to create a 
singleton and thus discard any information present in your original value.

If you are ever able to destruct a value that is not a singleton in 
order to create a value with a type in Set, then you will have found a 
major bug in Coq. But for now, Section "4.5.4 Destructors" of the manual 
still applies.

Best regards,

Guillaume