coq - 证明 Prop 中的两个居民不相等？

Question

是否有可能有一些A, B : Prop这样我们可以提供证明：

Section QUESTION.
A: Prop := <whatever you want> .
B : Prop := <whatever you want> .
Theorem ANeqB: A <> B.
Proof.
<a proof of this fact>
Qed.

直觉上，我认为不会，因为这可以让我们“区分”证明，但是如果不计算Aor ，就不能做到这一点B。然而，Coq 明确禁止我们检查证明，因为它们必须在运行时被擦除。所以，只Prop应该能够检查Prop（由于擦除），但检查总是计算的，因此Prop不能检查Prop。因此，没有任何东西可以检验Prop，上述定理ANeqB也不能被证明。

• 如果我的上述解释不正确，您能否向我解释为什么会这样？
• 如果这个定理ANeqB不能被证明，你能给我一个证明这个事实的证据吗？
• ANeqB 如果可以证明这个定理，你能告诉我我的直觉在哪里失败吗？

编辑：

令我震惊的是，由于我们可以将证明无关性作为一个额外的公理 ( Axiom proof_irrelevance : forall (P:Prop) (p1 p2:P), p1 = p2.)，因此无法在 Coq 中证明该定理ANeqB—— 如果可以的话，将其proof_irrelevance作为一个额外的公理是不合理的。

这改变了我的问题，然后：

• ANeqB是否有可能证明一些居民A和B？（proof_irrelevance更强：它表明我们无法证明[实际上，我们可以证明A <> B的更强有力的陈述] 对所有人）A = B A, B
• 如果没有，有人可以提供在 Coq 的基于公理系统中ANeqB 无法证明的证明吗？

标签： coqproofformal-verification

Answer 1

我想你可能在想别的东西。Prop本身并不是不相关的证明。它肯定有可区分的元素。例如，True <> False。

Section QUESTION.
Definition A: Prop := True.
Definition B : Prop := False.

Theorem ANeqB: A <> B.
Proof.
  unfold A, B.
  intro p.
  destruct p.
  exact I.
Qed.

End QUESTION.

相反，它的元素可能Prop是无关紧要的。在公理中

Axiom proof_irrelevance: forall (P: Prop) (p q: P), p = q.

p并且q它们本身不是 的元素Prop，而是 的某个元素的元素Prop。