coq - Coq 中的 Curry Howard 对应关系

Question

通过 Curry Howard 对应，所有定理和引理都是类型，证明对象是值。举个例子：

Theorem test:  0 <= 0.
Proof.
  omega. Qed.

当我这样做时，检查测试。Coq 的输出是：

test
     : 0 <= 0

但是当我检查“<=”的类型时，它是nat -> nat -> Prop。这意味着（0 <= 0）是Prop类型。这是否意味着'test'类型是Prop的子类型？一般来说，定理和引理标识符是 Prop 的子类型吗？

Answer 1

test : 0 <= 0并且0 <= 0 : Prop，正如你所说。在 Curry-Howard 对应的术语中，0 <= 0是类型/定理陈述，并且test是该类型的值/该定理的证明。

此示例中不涉及任何子类型。子类型是两种类型之间的关系；当Cat <: Animal（猫是动物的子类型）时，这意味着所有猫类型的对象也是动物类型：x : Cat暗示x : Animal。

Coq 在类型宇宙之间有一种相对简单的子类型化形式。最简单的例子Prop是Type. 您可以通过使用Check来确认0 <= 0 : Prop和来查看这一点0 <= 0 : Type。