问归纳命题在Coq中是如何工作的？

EN

因此，首先，这是正常的，你会对此感到困惑，但它可能比你想的更简单！

有两个不同的概念，你很困惑，所以让我们一次一个。首先，您提到ev 0是一个命题，并想知道是什么使其成为现实。您将在某一时刻了解到命题和类型是相同的，Prop和Set与Type之间的区别并不是这些事物本质上是不同的。

因此，当您定义类型(或命题) nat时，您将创建一个新类型，并描述其中存在的值。您可以声明有一个值O，即nat。并声明在传递一个S时，存在一个参数化值nat，即nat。

同样，当您定义类型(或命题) ev时，您将创建一个新类型(实际上，它是由nat类型的值索引的类型系列)，并描述这些ev类型中存在的值。您可以声明有一个值ev_0，即ev 0。并声明在传递一个ev_SS和一个ev n时，存在一个参数化的值n : nat，即ev (S (S n))。

因此，you通过在其中创建价值的方法使这一命题成为现实。还可以通过没有构造函数或具有永远无法调用的构造函数来定义错误命题：

Inductive MyFalse1 := . (* no constructor! *)

Inductive MyFalse2 :=
| TryToConstructMe : False ->  MyFalse2
| ThisWontWorkEither : 0 = 1 -> MyFalse2
.

我现在已经声明了两种类型(或命题)，但是没有办法证明它们，因为它们要么没有构造函数，要么就无法调用这些构造函数。

现在，关于事物的命名，ev_0、ev_SS、O和S都是相同类型的实体:构造函数。我不知道为什么您认为ev_0是指向值ev 0的指针。

将ev n作为一个命题分配没有任何意义，但如果有一种使用ev n类型构造值的方法，则它可能是正确的；如果无法用ev n类型构造值，则可能是假的。

但是，请注意，ev n是精心构建的，为那些偶数的n而设，而对于那些奇怪的n，则是无人居住的。正是在这个意义上，ev捕捉到了一个命题。如果收到ev n类型的值，它实质上断言n是偶数，因为类型ev n仅包含偶数的居民：

• ev 0包含1个居民(ev_0)
• ev 1包含0位居民
• ev 2包含1个居民(ev_SS 0 ev_0)
• ev 3包含0位居民
• ev 4包含1个居民(ev_SS 2 (ev_SS 0 ev_0))
• 等。

最后，对于Set、Prop和Type之间的区别，这些都是您可以在其中创建归纳类型的宇宙，但它们都有一定的限制。

Prop支持代码生成的优化。对于程序员来说，这基本上是一种将某些类型标记为仅用于验证目的，而不是用于计算目的的方法。结果，类型检查器将迫使您永远不计算Prop宇宙中的证明，代码生成将知道它可以丢弃这些证明，因为它们不参与计算行为。

Set只是Prop的一个限制，以避免处理宇宙级别。在以后的学习过程中，你不需要真正理解这一点。

你真的应该尽量不要把Prop看作是一个与Set不同的神奇事物。

以下内容可能对您有所帮助:我们可以以完全相同的方式重写nat和ev的定义，如下所示：

Inductive nat1 : Set :=
| O : nat1
| S : nat1 -> nat1
.
(* is the same as *)
Inductive nat1 : Set :=
| O : nat1
| S : forall (n : nat1), nat1
.

(* and *)
Inductive ev : nat -> Prop :=
| ev_0 : ev 0
| ev_SS : forall (n : nat), ev n -> ev (S (S n))
.
(* is the same as *)
Inductive ev : nat -> Prop :=
| ev_0 : ev 0
| ev_SS : forall (n : nat) (e : ev n), ev (S (S n))
.

当您看到一个类似a -> b的类型时，它实际上是forall (_ : a), b的一个简短操作，也就是说，我们期望输入a类型，并返回一个b类型的输出。

我们用forall (n : nat)编写ev_SS的原因是我们有为第一个参数命名，因为第二个参数的类型将取决于它(第二个参数具有ev n类型)。

如果您用Prop替换为Set，那么您就会说您理解这个定义：

Inductive ev' : nat -> Set :=
| ev_0' : ev' 0
| ev_SS' : forall n : nat, ev' n -> ev' (S (S n)).

对于每一个n : nat，我们都认为ev' n是一种有一些元素的类型，或者没有。因为这是一个归纳定义，我们可以知道ev' 0的元素是什么:惟一的元素是ev_0' (或者更准确地说，ev' 0类型的每一个封闭项都计算到ev_0;)。ev_0 1没有任何元素，但是有一个ev 2'元素，即ev_SS' 0 ev_0'。事实上，有一点思考表明，ev n要么是空的，要么是单例的，这取决于n是偶数还是奇数。

当我们从Set切换到Prop时，情况完全一样，只是读取方式不同：Set是(大型)类型，Prop也是类型(它们是宇宙)。Prop的每个元素都是一个类型(但我们更喜欢称之为“命题”)，它有一些元素(但我们更愿意称它们为“证明”)。因此，请考虑一下：

Inductive ev : nat -> Prop :=
| ev_0 : ev 0
| ev_SS : forall n : nat, ev n -> ev (S (S n)).

对于每一个n : nat，我们都认为ev n是一个语句，即n拥有属性ev，不管该属性是什么。对于任何给定的n，可能都有ev n的证明，在这种情况下，n具有属性ev，或者没有这样的证明，在这种情况下，n没有属性ev。因为这是一个归纳定义，我们可以知道ev_0的证明是什么:它们都计算到ev_0'。没有ev_0 1的证明，但有ev 2的证明，即ev_SS 0 ev_0。事实上，一点点思考表明，ev n有一个证明当且仅当n是偶数的。我们现在了解到，ev是“偶数”的属性。

这就是所谓的“作为类型的命题”。

我们观察到ev' 0只包含一个元素ev_0'。类型unit也只包含一个元素tt。这是否意味着ev' 0和unit是相等的？不，但它们是等价的，因为我们可以提供函数ev' 0 -> unit和unit -> ev' 0，它们是相互逆的。

对于ev 0，我们可以问同样的问题:它是否等于True？不，但它们是等价的，因为我们可以证明ev 0 -> True和True -> ev' 0的含义。

人们开始怀疑Prop和Set之间有什么区别。对于一个类型的P : Prop，它的所有元素都被认为是相等的，也就是说，Coq不允许我们区分它们。(这是一个教学上的谎言，因为在现实中，Coq对于P中的所有元素是否都被认为是平等的是不可知的，但也许最好现在就不要讨论这个问题。)