Theoretical Computer Science
lo.logic type-theory proof-assistants coq
Updated Fri, 10 Jun 2022 11:03:19 GMT

# Prove proof irrelevance in Coq?

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.

## Solution

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`.