如何证明 Coq 中命题外延性的证明不相关性？

Question

这是《逻辑基础》第ProofObjects章中的一道题。

我想证明命题外延性，

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

意味着证明不相关，

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

输入：

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

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

我非正式地理解这一论点，对于

H2

，

pf1

和

pf2

都是

True

类型。类型

True

的唯一构造函数是

I

，因此是

pf1 = pf2 = I

。但我如何在 Coq 中证明这一点？

Answer 1

问题在于您正在一个地方重写 pf1，而不是另一个地方。要将所有内容放在同一个位置，您可以使用恢复。如果我有代码：

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.

那么我的证明状态正是你所拥有的：

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

如果我随后运行

clear H1; revert pf1 pf2.

行，我会得到以下证明状态：

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

现在我可以重写了！

rewrite H2.

引导我：

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

这很容易解决。

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

为了您的方便，以下是完整代码：

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.

Answer 2

一种方法是对

pf1

和

pf2

再次进行抽象，从而能够对

H2

进行重写，然后对

pf1

和

pf2

进行案例分析。

Answer 3

我在前面的章节中使用了

specialize

/

remember

策略来介绍假设

HTP : True = P

。然后我只需通过

I

假设

destruct

即可获得构造函数

HTP

。

假设你已经证明了

pe_implies_true_eq

，这是我的解决方案：

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

Theorem pe_implies_true_eq :
  propositional_extensionality ->
  forall (P : Prop), P -> True = P.
Proof. Admitted.

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

Theorem pe_implies_pi:
  propositional_extensionality -> proof_irrelevance.
Proof.
  intros PE.
  intros P PF1 PF2.
  specialize (pe_implies_true_eq PE) with P as H.
  specialize (H PF1) as HTP. (* or [remember (H PF1) as HTP.] *)
  destruct HTP. destruct PF1. destruct PF2.
  reflexivity.
Qed.