The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

So, what exactly is not being able to destruct H in the nat goal preventing, when I can just do this:

 

The limitations of pattern matching over proposition have two goals:

• Keeping compatibility with proof irrelevance (which is one way of ensuring that extraction can safely erase propositions (it is not that simple in practice, though)).
• Preventing False from being provable

The former is what prevents [P\/Q] from being analysable in a non-[Prop] context. Otherwise, we would have, say [True\/True] is isomorphic to [bool]. In particular proof-irrelevance would be false (this is basically what Guillaume is saying above). Note that, in the impredicative version of [Set], [P+Q] is indeed a set (for [P] and [Q] in Set). It's really specific to the semantics of [Prop].

The latter is more imperative (and holds for impredicative [Set] as well), and prevents [exists x:A,P] from being analysable in a non-[Prop] context. The reason is fairly technical but has been known at least since the late eighties (see Thierry Coquand's An analysis of Girard's paradox). Basically, being able to eliminate over existential allows for an encoding of Burali-Forti's paradox akin to Girard's paradox in System U (or even easier in Type:Type). Well… let's come entirely honest: this only prevents elimination of existential towards sorts which are above [Prop] (that is [Type]). But we cannot eliminate towards [Set] either because [exists b:bool, if b then P else Q] is isomorphic to [P\/Q], so we are back to the previous case.

None of the above applies to a conjunction however. There is no property lost from being able to analyse [A/\B] in a non-[Prop] context (apart from creating absolutely horrendous bugs and complications in the extraction procedure, of course, but this is another story). So, in fact, for [A] and [B] in [Prop], [A/\B] is isomorphic to [A*B]. Coq takes this remark one step further and considers that [A*B] is, in this case, a [Prop] (which creates further horrendous bugs an complication in the extraction procedure, but this is still another story). It is the same which happens to [sig] in your example above.

Of course, this is only an approximation and sometimes Coq will refuse unproblematic case (such as the elimination of [exists x:(A:Prop), P] in a non-proposition context as you notice). Just as it will refuse unproblematic type definitions and perfectly good strongly normalising functions. There is a bunch of theorems for that.