The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

On 08/04/2014 02:10 PM, Maxime Dénès wrote:
> I meant phi returns Props, not booleans (although the same works with 
> bool).
>
> On 08/04/2014 02:08 PM, Maxime Dénès wrote:
> > The main concern is not extraction, but proof irrelevance. If you 
> > allow unrestricted elimination from True \/ True, you can build the 
> > following function:
> >
> > Definition phi (p : True \/ True) : bool :=
> >   match p with
> >   | or_introl _ => True
> >   | or_intror _ => False
> >   end
> >
> > Then you can refute proof irrelevance: assume it, deduce or_introl I 
> > = or_intror I hence phi (or_introl I) = phi (or_intror I), hence True 
> > = False, hence False.

Ah - that's the example I needed to jar me out of this rut!  Thanks, 
Maxime!

My naive view of rewrite rules as information preservation devices must 
be untrue in some way.  But, what is the difference between those kinds 
of bits in Prop can be created/destroyed arbitrarily by rewrite rules 
vs. those that can't?

It is almost as though the bit in or is necessarily irrelevant (note: P 
\/ Q <-> Q \/ P), independent of the proof irrelevance axiom, where the 
others are contingently irrelevant based on inclusion or not of the 
proof irrelevance axiom.  Or, "semi-contingently irrelevant" - with the 
proof irrelevance axiom, they are, but without it they merely "might 
be".  But that "might be" is strong enough to prevent arbitrary 
creation/destruction due to rewrites.

Regardless, the case analysis rules have to prevent any and all 
irrelevant bits from becoming relevant.

-- Jonathan