Prove proof irrelevance in Coq?

Question

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.

Answer 1

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.