Prove proof irrelevance in Coq?

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.

Solved by user43935 (103 )
Feb 26, 2011 at 14:25