coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Proof Irrelevance

From: Robbert Krebbers <mailinglists AT robbertkrebbers.nl>
To: Ilmārs Cīrulis <ilmars.cirulis AT gmail.com>
Cc: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Proof Irrelevance
Date: Wed, 23 Oct 2013 09:19:08 +0200

On 10/23/2013 01:09 AM, Ilmārs Cīrulis wrote:

If it's true, is there any general way how to make such proofs?

Given any decidable proposition [P] with decider [P_dec : {P} + {~P}], you can easily make a logical equivalent proof irrelevant proposition:

Definition P' := if P_dec then True else False.

It is easy to prove that [P <-> P'], and [forall p q : P', p = q].

[Coq-Club] Proof Irrelevance, Ilmārs Cīrulis, 10/23/2013
- Re: [Coq-Club] Proof Irrelevance, Jason Gross, 10/23/2013
  - Re: [Coq-Club] Proof Irrelevance, Ilmārs Cīrulis, 10/23/2013
    - Re: [Coq-Club] Proof Irrelevance, AUGER Cédric, 10/23/2013
- Re: [Coq-Club] Proof Irrelevance, Robbert Krebbers, 10/23/2013