证明道具中的两个居民不相等吗？

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.

[直觉上，我认为不是，因为这将使我们能够在证明之间进行区分”，但是如果不使用A或B进行计算，就不能做到这一点。但是，Coq明确禁止我们检查证明，因为必须在运行时将其删除。因此，（由于擦除）仅Prop应该能够检查Prop，但是检查始终是计算的，因此Prop无法检查Prop。因此，nothing不能检查Prop，并且不能证明上述定理ANeqB。

• 如果我的上述解释不正确，请您向我解释为什么会这样吗？
• 如果定理ANeqB无法得到证明，您能指出这个事实吗？
• 如果定理ANeqB 可以]被证明，您能告诉我我的直觉在哪里失败吗？

编辑：

[让我感到震惊的是，由于我们可以将证明无关紧要当作额外的公理（Axiom proof_irrelevance : forall (P:Prop) (p1 p2:P), p1 = p2.），因此定理ANeqB不能在Coq中证明---如果可以的话，让proof_irrelevance变得不合理作为额外的公理。

这转移了我的问题，然后：

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

是否有一些A，B：道具，这样我们可以提供以下证明：QUESTION部分。答：道具：= 。 B：道具：= 。定理ANeqB：A <> ...

Answer 1

我认为您可能在想其他事情。 Prop本身并非无关紧要。它绝对具有可区分的元素。例如，True <> False。