<p>Proof irrelevance in general is not implied by the theory behind Coq. Even proof irrelevance for equality is not implied; it is equivalent to <a href="https://github.com/coq/coq/wiki/The-Logic-of-Coq#what-is-streichers-axiom-k" rel="noreferrer">Streicher's axiom K</a>. Both <a href="https://github.com/coq/coq/wiki/The-Logic-of-Coq#axioms" rel="noreferrer">can be added as axioms</a>.</p>

<p>There are developments where it's useful to reason about proof objects, and proof irrelevance makes this nigh-impossible. Arguably these developments should have all the objects whose structure matters recast in <code>Set</code>, but with the basic Coq theory the possibility is there.</p>

<p>There is an important subcase of proof irrelevance that always holds. Streicher's axiom K always holds on decidable domains, i.e. equality proofs on decidable sets are unique. The general proof is in the <a href="http://coq.inria.fr/library/Coq.Logic.Eqdep_dec.html" rel="noreferrer"><code>Eqdep_dec</code></a> module in the Coq standard library. Here's your theorem as a corollary (my proof here is not necessarily the most elegant):</p>

<pre><code>Require Bool.
Require Eqdep_dec.
Theorem bool_pirrel : forall (b : bool) (p1 p2 : b = true), p1 = p2.
Proof.
  intros; apply Eqdep_dec.eq_proofs_unicity; intros.
  destruct (Bool.bool_dec x y); tauto.
Qed.
</code></pre>

<p>For this special case, here's a direct proof (inspired by the general proof in <code>Eqdep_dec.v</code>). First, define we define a canonical proof of <code>true=b</code> (as usual in Coq, it's easier to have the constant first). Then we show that any proof of <code>true=b</code> has to be <code>refl_equal true</code>.</p>

<pre><code>Let nu b (p:true = b) : true = b :=
  match Bool.bool_dec true b with
    | left eqxy =&gt; eqxy
    | right neqxy =&gt; False_ind _ (neqxy p)
  end.
Lemma bool_pcanonical : forall (b : bool) (p : true = b), p = nu b p.
Proof.
  intros. case p. destruct b.
  unfold nu; simpl. reflexivity.
  discriminate p.
Qed.
</code></pre>

<p>If you add classical logic to Coq, you get proof irrelevance. Intuitively speaking, classical logic gives you a decision oracle for propositions, and that's good enough for axiom K. There is a proof in the Coq standard library module <a href="http://coq.inria.fr/library/Coq.Logic.Classical_Prop.html" rel="noreferrer"><code>Classical_Prop</code></a>.</p>

CC BY-SA 4.0
2011-02-26T14:25:27.847Z
2019-08-26T15:40:06.067Z
2019-08-26T15:40:06.067Z
Gilles 'SO- stop being evil'
<p>Is there a way to prove the following theorem in Coq?</p>

<p><code>Theorem bool_pirrel : forall (b : bool) (p1 p2 : b = true), p1 = p2.</code></p>

<p><strong>EDIT</strong>: An attempt to give a brief explanation for "what proof irrelevance is" (correct me someone if I am wrong or inaccurate)</p>

<p>The basic idea is that in the proposition world (or the <code>Prop</code> sort in Coq), what you (and you should) really care about is the <em>provability</em> of a proposition, <em>not</em> the proofs of it, there may be many (or none). In case you have multiple proofs, from the provability point of view, they are equal in the sense that <em>they prove the same proposition</em>. So their distinction is just irrelevant. This differs from the computational point of view where you really care about the distinction of two terms, e.g., basically, you don't want the two inhabitants of the <code>bool</code> type (or <code>Set</code> in Coq's words), namely <code>true</code> and <code>false</code> to be equal. But if you put them in <code>Prop</code>, they are treated equal.</p>

CC BY-SA 4.0
2021-11-09T14:22:03.633Z
try the bool of Forall(0) and Exists(1) for illumination. #P=#Q for all formulas P. +daniel GREs2380
daniel pehoushek
CC BY-SA 2.5
2011-02-26T12:06:47.643Z
Intriguing. I'm sure you'd get an answer within minutes on the Coq mailing list. (Be sure to post the response here, if you do.)
Dave Clarke
CC BY-SA 2.5
2011-02-28T04:31:13.037Z
For those of us who are curious what your question is about, but not familiar with Coq, can you maybe add a sentence or two explaining what that theorem means in English? (And maybe what "proof irrelevance" is about?)
Joshua Grochow
CC BY-SA 2.5
2011-02-28T20:57:00.100Z
@Joshua, I am not adequate to explain it in detail, because it is also new to me, that is also why it puzzled me for quite some time. But anyway, here is my attempt (see in the question part).
day
CC BY-SA 2.5
2011-02-28T21:56:18.053Z
@Joshua, IIRC, in constructive mathematics, a proof of an implication like $A \rightarrow B$ is a function/process/algorithm/construction that converts a *proof* of $A$ to a *proof* of $B$, and the construction is *proof irrelevant* if the resulting proof of $B$ is not dependent on which proof is given for $A$.
Kaveh
<lo.logic><type-theory><proof-assistants><coq>
Prove proof irrelevance in Coq?
day
# Prove proof irrelevance in Coq?

(Asked by: username_0 on 2011-02-26)

Is there a way to prove the following theorem in Coq?

`Theorem bool_pirrel : forall (b : bool) (p1 p2 : b = true), p1 = p2.`

**EDIT**: An attempt to give a brief explanation for "what proof irrelevance is" (correct me someone if I am wrong or inaccurate)

The basic idea is that in the proposition world (or the `Prop` sort in Coq), what you (and you should) really care about is the *provability* of a proposition, *not* the proofs of it, there may be many (or none). In case you have multiple proofs, from the provability point of view, they are equal in the sense that *they prove the same proposition*. So their distinction is just irrelevant. This differs from the computational point of view where you really care about the distinction of two terms, e.g., basically, you don't want the two inhabitants of the `bool` type (or `Set` in Coq's words), namely `true` and `false` to be equal. But if you put them in `Prop`, they are treated equal.

**Tags:** lo.logic, type-theory, proof-assistants, coq
> **Comments:**
> **username_2**: Intriguing. I'm sure you'd get an answer within minutes on the Coq mailing list. (Be sure to post the response here, if you do.)  
> **username_3**: For those of us who are curious what your question is about, but not familiar with Coq, can you maybe add a sentence or two explaining what that theorem means in English? (And maybe what "proof irrelevance" is about?)  
> **username_0**: @Joshua, I am not adequate to explain it in detail, because it is also new to me, that is also why it puzzled me for quite some time. But anyway, here is my attempt (see in the question part).  
> **username_4**: @Joshua, IIRC, in constructive mathematics, a proof of an implication like $A \rightarrow B$ is a function/process/algorithm/construction that converts a *proof* of $A$ to a *proof* of $B$, and the construction is *proof irrelevant* if the resulting proof of $B$ is not dependent on which proof is given for $A$.  
> **username_1**: try the bool of Forall(0) and Exists(1) for illumination. #P=#Q for all formulas P. +daniel GREs2380  

---

## 1 answers

### Answer by username_5 on 2011-02-26. Score: 31 | Accepted answer

Proof irrelevance in general is not implied by the theory behind Coq. Even proof irrelevance for equality is not implied; it is equivalent to Streicher's axiom K. Both can be added as axioms.
There are developments where it's useful to reason about proof objects, and proof irrelevance makes this nigh-impossible. Arguably these developments should have all the objects whose structure matters recast in Set, but with the basic Coq theory the possibility is there.
There is an important subcase of proof irrelevance that always holds. Streicher's axiom K always holds on decidable domains, i.e. equality proofs on decidable sets are unique. The general proof is in the Eqdep_dec module in the Coq standard library. Here's your theorem as a corollary (my proof here is not necessarily the most elegant):
Require Bool.
Require Eqdep_dec.
Theorem bool_pirrel : forall (b : bool) (p1 p2 : b = true), p1 = p2.
Proof.
  intros; apply Eqdep_dec.eq_proofs_unicity; intros.
  destruct (Bool.bool_dec x y); tauto.
Qed.

For this special case, here's a direct proof (inspired by the general proof in Eqdep_dec.v). First, define we define a canonical proof of true=b (as usual in Coq, it's easier to have the constant first). Then we show that any proof of true=b has to be refl_equal true.
Let nu b (p:true = b) : true = b :=
  match Bool.bool_dec true b with
    | left eqxy => eqxy
    | right neqxy => False_ind _ (neqxy p)
  end.
Lemma bool_pcanonical : forall (b : bool) (p : true = b), p = nu b p.
Proof.
  intros. case p. destruct b.
  unfold nu; simpl. reflexivity.
  discriminate p.
Qed.

If you add classical logic to Coq, you get proof irrelevance. Intuitively speaking, classical logic gives you a decision oracle for propositions, and that's good enough for axiom K. There is a proof in the Coq standard library module Classical_Prop.


---

