如何在Coq中从命题外延性证明证明无关性？

问题背景 #

需要证明命题外延性（Propositional Extensionality）蕴含证明无关性（Proof Irrelevance）：

• 命题外延性：forall (P Q : Prop), (P <-> Q) -> P = Q
• 证明无关性：forall (P : Prop) (pf1 pf2 : P), pf1 = pf2

现有代码与报错 #

编写的部分Coq代码：

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.

执行后上下文与报错：

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

报错信息：Cannot change pf1, it is used in conclusion.

非形式化思路：通过H2可知pf1和pf2的类型均为True，而True唯一的构造子是I，因此pf1 = pf2 = I，但不知如何在Coq中实现。

解决方法 #

直接改写pf1会因为它出现在结论中被禁止，我们可以通过替换类型等式的方式，将pf1和pf2的类型转换为True，再利用True的证明唯一性完成证明。

简洁版完整证明

Theorem pe_implies_pi :
(forall (P Q : Prop), (P <-> Q) -> P = Q) -> (forall (P : Prop) (pf1 pf2 : P), pf1 = pf2).
Proof.
  intros pe P pf1 pf2.
  (* 利用命题外延性得到 P = True *)
  assert (P_eq_True : P = True) by (apply pe; split; [intros _; apply I | intros _; apply pf1]).
  subst P. (* 将上下文中所有的 P 替换为 True *)
  (* 此时 pf1、pf2 类型均为 True，直接匹配构造子证明相等 *)
  destruct pf1 as []; destruct pf2 as []; reflexivity.
Qed.

步骤解释

1. subst P会把上下文中所有的P（包括pf1和pf2的类型）替换为True，规避直接改写pf1的限制。
2. destruct pf1 as []和destruct pf2 as []是对True的证明进行模式匹配——因为True只有唯一构造子I，匹配后两个变量都会被替换为I。
3. reflexivity直接证明I = I，完成整个推导。

内容的提问来源于stack exchange，提问作者Farhan