The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

On 08/04/2014 05:41 AM, Arnaud Spiwack wrote:
> > 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].

Right - instead, {True}+{True} is isomorphic to bool.  That is probably 
a good source of confusion.  But in terms of information content, it is 
easier to understand: bool contains a bit of information in its "value", 
while {True}+{True} contains a bit of information in discrimination 
between its two non-Prop-kinded constructors - and these lines 
completely blur, as the "value" of bool really just amounts to 
discrimination between its own two non-Prop-kinded constructors, and 
nothing more.

But, True \/ True is isomorphic to True.  And False \/ P is isomorphic 
to P.  So, allowing analysis of either in a non-Prop context shouldn't 
impact proof irrelevance in any way.  I am not suggesting that Coq 
should strive to do ths - I was just looking for the rule Coq is using.  
At this point in the discussion, I would guess the rule is something 
like that the term is considered analyzable or not independently of its 
subterms.

>   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.

Now that I know this can happen - that Coq can "demote" certain things 
into Prop despite their declaration in Type - I think that this is a 
very good thing.  It is just a little hard to predict when it will 
happen vs. not.  It reminds me of the developments in Idris towards 
compiler-determined erasability beyond declaration-based erasability.  
As erasability is a topic of interest to me, I am very happy to see 
further developments in this area.

Thanks for the explanation, Arnaud!

-- Jonathan