The Coq mailing list

[Maxime Dénès <mail AT maximedenes.fr>]

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.
>
> Note that in CIC, proof irrelevance is a consequence of excluded 
> middle, so the formalism would become anti-classical.
>
> Applying your handwavy reasoning to "exists" could even make it 
> inconsistent, as Arnaud said (getting strong sums and impredicativity).
>
> Maxime.
>
>
> On 08/04/2014 01:55 PM, Jonathan wrote:
> > On 08/04/2014 01:19 PM, Maxime Dénès wrote:
> > > ...
> > > Now, you were asking: is the answer to that question the same for 
> > > proofs of two equivalent propositions. No, as Guillaume showed it : 
> > > True and True \/ True are logically equivalent. Yet, if you allow to 
> > > eliminate a proof of True to Set, you don't reveal anything, whereas 
> > > allowing the same elimination from a proof of True \/ True reveals 
> > > one bit of information. Relaxing the elimination restriction on True 
> > > \/ True made it isomorphic to bool.
> > >
> > > Maxime.
> >
> > I am sorry for being slow here, but I still don't see any bit of 
> > information in True \/ True that could be revealed under any 
> > circumstance.  Is my claim that having a rewrite rule True \/ True 
> > <-> True demonstrates that both sides have the same information 
> > content false?  If so, I think we must be using the word 
> > "information" in different ways.
> >
> > I guess if you are worried about extraction, and you allowed analysis 
> > of True \/ True in a non-Prop context, and the extractor wasn't 
> > sufficiently savvy (and as Arnaud points out, it has much more 
> > serious matters to attend to than this), then you would end up with 
> > two branches of a match statement, but have no way to cause the 
> > generated code to take one vs. the other - so one or the other is 
> > dead code, and the compiler just has to choose which it is.  But, it 
> > shouldn't matter, because whichever branch it chooses would be 
> > identical to whatever you could have extracted without analyzing True 
> > \/ True.
> >
> > -- Jonathan