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.

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, Feb 26 '11 at 12:06
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, Feb 28 '11 at 04:31
@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, Feb 28 '11 at 20:57
@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, Feb 28 '11 at 21:56
try the bool of Forall(0) and Exists(1) for illumination. #P=#Q for all formulas P. +daniel GREs2380 — daniel pehoushek, Nov 09 '21 at 14:22

score 31 · Accepted Answer · edited Aug 26 '19 at 15:40

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.

Prove proof irrelevance in Coq?

1 Answers1