在 Coq 中提供示例，其中 (A B: Prop)，P: Prop -> Type，这样 A <-> B，但不能用 P B 替换 P A

Question

正如标题所问，我希望举个例子：

Section Question:
Definition A: Prop := <whatever you like>.
Definition B:Prop := <whatever you like>.
Definition/Inductive/Fixpoint P: Prop -> Type := <whatever you like>.

Theorem AEquivB: A <-> B.
Proof. <supply proof here>. Qed.

(* Question 1. can we pick a P, A, B to prove this? *)
Theorem PA_not_equals_Pb: P A <> P B.
Proof. <supply proof here>. Qed.

(* Question 1.5. can we pick a P, A, B to prove this? *)
Theorem PA_not_equiv_PB: ~(P A <-> P B)
Proof. <supply proof here>. Qed.

总的来说，我有兴趣了解 "proof equivalence" 是否是 "good enough" 在某种意义上被用作 "equality"，或者是否存在我们可以 P A，和 A <-> B，但不是 P B。

Answer 1

forall A B : Prop, (A <-> B) -> A = B与Coq一致。（也就是说，你可以把它作为公理加上去，理论就不会崩溃。）这个公理叫做propositional extensionality。由于 A = B 很快给出 forall P : Prop -> Prop, P A <-> P B，因此没有项 P、A、B 使得 (A <-> B) /\ ~(P A <-> P B)，因为这与公理相矛盾，但我们知道它是一致的。同样，我们也很快得到P A = P B，这意味着我们不能同时得到P A <> P B。请注意，即使不存在违反命题外延性的P、A、B，我们仍然无法证明命题外延性。 Coq 根本没有力量像那样谈论自己（这很好，因为这意味着你可以自定义它），这就是为什么如果你想要的话，需要将命题外延性作为公理添加。

在 Coq 中提供示例，其中 (A B: Prop)，P: Prop -> Type，这样 A <-> B，但不能用 P B 替换 P A

Provide example in Coq where (A B: Prop), P: Prop -> Type, such that A <-> B, but one cannot replace P A with P B

formal-verification

proof

coq