库克的咖喱霍华德对应

问题描述

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

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

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

test
     : 0 <= 0

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

解决方法

test : 0 <= 0和0 <= 0 : Prop，如您所说。在Curry-Howard对应关系的术语中，0 <= 0是类型/定理陈述，test是该类型/定理的证明。

此示例中不涉及任何子类型。子类型化是两种类型之间的关系。如果Cat <: Animal（猫是动物的子类型），则意味着猫类型的所有对象也都是动物类型的：x : Cat表示x : Animal。 >

Coq在类型Universe之间具有一种相对简单的子类型形式。最简单的示例是Prop是Type的子类型。您可以使用Check来确认0 <= 0 : Prop以及0 <= 0 : Type来查看此内容。