在Coq中提供示例，其中(A B：Prop)，P：Prop ->类型，使得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.  

一般来说，我有兴趣了解"证明等价"在某种意义上是否"足够好"，可以用作"相等"，或者是否存在可以有P A和A <-> B，但不能P B的情况。

Answer 1

forall A B : Prop, (A <-> B) -> A = B。(也就是说，你可以把它作为一个公理，理论就不会崩溃。(这个公理被称为命题可拓性。由于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根本没有能力这样谈论自己(这很好，因为这意味着你可以自定义它(，这就是为什么如果你想要的话，命题可扩展性需要被添加为公理