How can I prove Proof Irrelevance from Propositional Extensionality in Coq?

This is a question from "Logical Foundation" in Chapter ProofObjects.

I want to prove that Propositional Extensionality,

forall (P Q : Prop), (P <-> Q) -> P = Q

implies Proof Irrelevance,

forall (P : Prop) (pf1 pf2 : P), pf1 = pf2

Input:

Theorem pe_implies_pi :
(forall (P Q : Prop), (P <-> Q) -> P = Q) -> (forall (P : Prop) (pf1 pf2 : P), pf1 = pf2).
Proof. intros. assert (H1 := H P True).
assert (H2 : P <-> True).
{ split. intros. apply I. intros. apply pf1. }
apply H1 in H2.
Fail rewrite H2 in pf1.

Output:

H: ∀ P Q : ℙ, P ↔ Q → P = Q
P: ℙ
pf1,pf2: P
H1: P ↔ True → P = True
H2: P = True
===========================
pf1 = pf2

The command has indeed failed with message:
Cannot change pf1, it is used in conclusion.

I understand the line of argument informally in that, with H2, both pf1 and pf2 are of type True. The only constructor for type True is I, hence pf1 = pf2 = I. But how do I prove this in Coq?

Solution

The problem is that you are rewriting pf1 in one place, but not another. To get everything in the same place, you can use revert. If I have the code:

Definition PropEx : Prop := forall (P Q : Prop), (P <-> Q) -> P = Q.

Definition ProofIrr : Prop := forall (P : Prop) (pf1 pf2 : P),  pf1 = pf2.

Theorem PropExImpliesProofIrr : PropEx -> ProofIrr.
Proof.
  intros PE P pf1 pf2.
  assert (H1 := PE P True).
  assert (H2 : P <-> True). { split; intro H2; auto. }
  apply H1 in H2.

then my proof state is exactly what you had:

1 goal (ID 19)
  
  PE : PropEx
  P : Prop
  pf1, pf2 : P
  H1 : P <-> True -> P = True
  H2 : P = True
  ============================
  pf1 = pf2

If I then run the line clear H1; revert pf1 pf2., I get the following proof state:

  PE : PropEx
  P : Prop
  H2 : P = True
  ============================
  forall pf1 pf2 : P, pf1 = pf2

Now I can rewrite! rewrite H2. leads me to:

1 goal (ID 23)
  
  PE : PropEx
  P : Prop
  H2 : P = True
  ============================
  forall pf1 pf2 : True, pf1 = pf2

Which is easily solved.

  intro pf1; destruct pf1.
  intro pf2; destruct pf2.
  reflexivity.
Qed.

For your convenience, here is the entire code:

Definition PropEx : Prop := forall (P Q : Prop), (P <-> Q) -> P = Q.

Definition ProofIrr : Prop := forall (P : Prop) (pf1 pf2 : P),  pf1 = pf2.

Theorem PropExImpliesProofIrr : PropEx -> ProofIrr.
Proof.
  intros PE P pf1 pf2.
  assert (H1 := PE P True).
  assert (H2 : P <-> True). { split; intro H2; auto. }
  apply H1 in H2.
  clear H1; revert pf1 pf2.
  rewrite H2.
  intro pf1; destruct pf1.
  intro pf2; destruct pf2.
  reflexivity.
Qed.