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是一个type/theorem陈述，而test是该定理的那个type/proof的值。

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

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

来查看这一点

Curry Howard correspondence in Coq