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

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的情况。

标签： coqproofformal-verification

Answer 1

这与 Coq 一致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 根本没有能力像那样谈论它自己（这很好，因为这意味着你可以自定义它），这就是为什么如果你想要它需要添加命题外延性作为公理。