归纳命题在 Coq 中如何运作？

我正在阅读软件基础中的 IndProp 和 Adam Chlipala 的第 4 章书，但我在理解归纳命题时遇到了困难。

为了运行示例，让我们使用：

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

我想我确实理解“正常”类型使用Set like:

Inductive nat : Set :=
  | O : nat
  | S : nat -> nat.

和类似的事情O只返回类型的单个对象nat and S O正在获取类型的对象nat并返回另一个不同的同一类型之一nat。我想我所说的不同对象是指它们具有不同的值。

我感到困惑的是归纳道具的构造函数与归纳类型到底有何不同Set. For Set看起来它们只是充当函数，一个接受值并返回更多该类型值的函数。但对于归纳命题，我很难弄清楚它们的作用。

例如采取ev_0举一个简单的例子。我假设这是命题对象（值）的名称ev 0。既然是它自己ev 0必须是一个Prop一个提议。但究竟是什么让它成为事实呢？如果这是一个提议，我认为它可能是错误的。我想归纳法让我感到困惑。ev是“返回某种类型的对象的函数（命题）”，所以 ev 0 只是一个命题，但我们还没有说什么ev 0应该意味着（与我对自然数的定义不同，基本情况很清楚它在做什么）。在 python 中我希望看到

n == 0: return True

或基本情况的东西。但在这种情况下，它似乎循环指向自身而不是类似的东西True。我知道我有一个根本性的误解，但我不知道我到底不理解什么。

另外让我困惑的是命名。在里面nat名字O对于建造/构造物体至关重要。但在归纳定义中ev_0似乎更像是一个标签/指向真实值的指针ev 0。所以我假设ev_SS == ev_0 -? ev 2确实没有意义，但我不知道为什么。这里的标签与使用感应类型的标签有何不同？set?

For ev_SS这更令人困惑。因为我不知道标签在做什么，这当然让我感到困惑，但看看它是如何指向的：

forall n : nat, ev n -> ev (S (S n))

所以给定一个自然数n我认为它返回了命题ev n -> ev (S (S n))（我假设forall n : nat不是命题对象的一部分，它只是用来指示返回命题的构造函数何时起作用）。所以forall n : nat, ev n -> ev (S (S n))这并不是一个真正的提议，但是ev n -> ev (S (S n)).

有人可以帮我澄清归纳命题类型在 Coq 中是如何真正工作的吗？

注意我并不真正理解之间的区别Set vs Type但我相信这本身就是另一篇文章了。

更多评论：

我又玩了一下这个，然后做了：

Check ev_SS

令我惊讶的是：

ev_SS
     : forall n : nat, ev n -> ev (S (S n))

我认为这是出乎意料的，因为我没想到这种类型ev_SS（除非我误解了什么Check应该做的）将是函数本身的定义。我以为ev_SS是一个构造函数，所以在我看来，我认为在这种情况下会进行映射nat -> Prop所以这当然是我所期望的类型。

所以，首先，你对此感到困惑是正常的，但它可能比你想象的要简单！

您对两个不同的概念感到困惑，所以让我们逐一讨论它们。首先，你提到ev 0是一个命题，并想知道是什么让它成为现实。在某些时候你会了解到命题和类型是相同的东西，并且它们之间的区别Prop and Set and Type并不是说这些东西本质上是不同的。

因此，当您定义类型（或命题）时nat，您正在创建一个新类型，并描述其中存在哪些值。你声明有一个值O， 这是一个nat。并且你声明有一个参数化值S， 这是一个nat，当通过一个nat.

同样，当你定义类型（或命题）时ev，您正在创建一个新类型（嗯，它实际上是一个由类型值索引的类型系列nat），并描述其中存在哪些值ev类型。你声明有一个值ev_0，这是一个ev 0。并且你声明有一个参数化值ev_SS，这是一个ev (S (S n))，当通过一个n : nat and an ev n.

So you通过在其中创造价值的方式使该主张成为现实。您还可以通过没有构造函数或具有永远无法调用的构造函数来定义伪命题：

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

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

我已经声明了两个 now 类型（或命题），但无法见证它们，因为它们要么没有构造函数，要么无法调用这些构造函数。

现在关于事物的命名，ev_0, ev_SS, O, and S都是同一种实体：构造函数。我不知道你为什么这么想ev_0是一个指向值的指针ev 0.

没有赋予任何意义ev n作为一个命题，除非有一种方法可以构造具有类型的值，否则它可能是正确的命题ev n，如果无法构造具有类型的值，则可能为 falseev n.

但请注意ev n经过精心设计，正是为了满足这些需求ns 是均匀的，并且正是那些无人居住的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))
• etc.

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

Prop实现代码生成的优化。从本质上讲，它是程序员将某种类型标记为仅用于验证目的而不用于计算目的的一种方法。因此，类型检查器将迫使您永远不要在以下范围内计算证明：Prop宇宙，代码生成将知道它可以丢弃这些证明，因为它们不参与计算行为。

Set只是一个限制Prop以避免处理宇宙层面。直到稍后的学习过程中，您才真正需要理解这一点。

你真的应该试着不去想Prop作为一种神奇的东西不同于Set.

以下内容可能对您有帮助：我们可以重写以下定义nat and 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) in ev_SS是我们have为第一个参数命名，因为第二个参数的类型将取决于它（第二个参数的类型为ev n).