Coq 中的 Curry Howard 对应关系

Posted 2023-05-08

【中文标题】Coq 中的 Curry Howard 对应关系

【英文标题】：Curry Howard correspondence in Coq

【发布时间】：2020-12-21 18:45:15

【问题描述】：

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

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

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

test
     : 0 <= 0

但是当我检查“ nat -> Prop。这意味着（0

【参考方案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 来查看这一点。

【讨论】：

'0

它们都是类型，但是它们之间的关系是“有类型”，而不是子类型。它们看起来非常相似（我们使用看起来相似的符号），但它们的行为不同。

如果我是正确的，has-type 关系需要 LHS 上的类型和 RHS 上的类型的值，如 (n: nat)。上面 (0

您是对的，某些类型如0 <= 0、True、False、p \/ q 或x = y 具有Prop 类型，但并非所有类型都具有Prop 类型，从Prop 本身开始，它的类型为Prop : Type，还有nat : Set（Set 是Type 特定情况的别名）。