coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Provability of (proj_sig1 x) = (proj_sig1 y) -> x = y

From: Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>
To: Floyd Lee <undecidable AT secureroot.com>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] Provability of (proj_sig1 x) = (proj_sig1 y) -> x = y
Date: Mon, 03 Jun 2013 15:01:26 +0200

On 02/06/2013 23:45, Floyd Lee wrote:
> Is this deceptively simple theorem provable in Coq's logic?

Your lemma implies in particular proof-irrelevance (take A to be unit
and the predicate to be any proposition), so no.

PMP

Attachment: signature.asc
Description: OpenPGP digital signature

[Coq-Club] Provability of (proj_sig1 x) = (proj_sig1 y) -> x = y, Floyd Lee, 06/03/2013
- Re: [Coq-Club] Provability of (proj_sig1 x) = (proj_sig1 y) -> x = y, Adam Chlipala, 06/03/2013
- Re: [Coq-Club] Provability of (proj_sig1 x) = (proj_sig1 y) -> x = y, Pierre-Marie Pédrot, 06/03/2013
  - Re: [Coq-Club] Provability of (proj_sig1 x) = (proj_sig1 y) -> x = y, Pierre-Marie Pédrot, 06/03/2013
- Re: [Coq-Club] Provability of (proj_sig1 x) = (proj_sig1 y) -> x = y, Christian Doczkal, 06/03/2013
- <Possible follow-up(s)>
- Re: [Coq-Club] Provability of (proj_sig1 x) = (proj_sig1 y) -> x = y, Floyd Lee, 06/03/2013