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

Question

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

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

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

我想我确实使用以下方式理解“正常”类型Set：

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

诸如这样的事情O就是返回一个类型的对象，nat并S O接受一个类型的对象nat并返回另一个同一类型的不同对象nat。通过不同的对象，我想我的意思是它们具有不同的价值。

我困惑的是归纳道具的构造函数与归纳类型的区别Set。因为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？

对于那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中是如何工作的吗？

---

请注意，我并不真正了解Setvs 的区别，Type但我认为这本身就是另外一则文章。

---

其他一些评论：

我还在玩这个，做了：

Check ev_SS

令我惊讶的是：

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

我认为这是意外的，因为我没想到类型的类型ev_SS（除非我误解了Check应该做的事情）是函数本身的定义。我以为ev_SS是构造函数，所以在我看来，在这种情况下可以进行映射，nat -> Prop因此这就是我期望的类型。

Answer 1

因此，首先，对此感到困惑是很正常的，但它可能比您想的要简单！

您会混淆两个截然不同的概念，因此让我们一次来考虑一个。首先，您提到这ev 0是一个命题，想知道是什么使它成为现实。你会在某个时候得知，命题和类型是相同的东西，之间的区别Prop，并Set与Type不说那些东西是本质上的不同。

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

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

因此，您可以通过在其中创建价值的方法来使该建议成为现实。您也可以通过不使用构造函数或使用永远无法调用的构造函数来定义错误的命题：

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命题分配给命题没有任何意义，除了它是一个命题，如果有一种方法可以用type构造一个值ev n，则可能为true；如果没有方法可以用type构造一个值，则可能为false ev n。

但是，请注意，ev n经过精心设计，它们恰好适合n偶数的s 居住，而恰好适合n奇数的s 居住。从这个意义上讲，它ev抓住了一个命题。如果您收到type的值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，您可以在其中创建归纳类型的所有Universe，但是它们具有某些限制。PropType

Prop实现代码生成的优化。本质上，这是程序员（一种您将某种类型标记为仅用于验证目的，而从未用于计算目的）的一种方式。结果，类型检查器将迫使您从不对PropUniverse中的证明进行计算，并且代码生成将知道它可以丢弃这些证明，因为它们不参与计算行为。

Set只是Prop避免与宇宙层次打交道的限制。直到以后的学习过程中，您才真正需要了解这一点。

您应该真正尝试不要认为与Prop魔幻魔法有所不同Set。

以下内容可能对您有帮助：我们可以以完全等效的方式将natand 的定义重写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，也就是说，我们期望输入一个type a，并返回一个type的输出b。

我们之所以写forall (n : nat)，ev_SS是因为我们必须为第一个参数命名，因为第二个参数的类型将取决于它（第二个参数具有type ev n）。