coq - 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类型的对象。通过不同的对象，我想我的意思是它们具有不同的值(value)。

我感到困惑的是归纳 Prop 的构造函数与归纳类型 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中是如何工作的吗？

请注意，我并没有真正理解 Set和 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。并且您声明在传递S时存在一个参数化值nat，即nat。

以同样的方式，当您定义类型(或命题)ev时，您正在创建一个新类型(实际上，它是由nat类型的值索引的一系列类型)，并描述了这些ev类型中存在哪些值。您声明存在一个值ev_0，即ev 0。并且您声明在传递ev_SS和ev (S (S n))时存在一个参数化值n : nat，即ev 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分配为一个命题没有任何意义，除了它是一个命题，如果有一种方法可以构造类型为 ev n的值，则可能为true；如果没有方法可以构造类型为 ev n的值，则可能为false 。

但是，请注意，精心制作了 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之间的差异，它们都是可以在其中创建归纳类型的Universe，但是它们具有某些限制。
Prop启用代码生成的优化。本质上，这是程序员(一种您将某种类型标记为仅用于验证目的，而从未用于计算目的)的一种方式。结果，类型检查器将迫使您从不对 Prop范围内的证明进行计算，并且代码生成将知道，由于这些证明不参与计算行为，因此可以丢弃这些证明。
Set只是对 Prop的一种限制，以避免处理Universe级别。直到以后的学习过程中，您才真正需要了解这一点。

您应该真正尝试不要将 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)。