Coq中的归纳命题如何工作？ [英] How do inductive proposition work in Coq?

问题描述

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

I was going through IndProp in software foundations and Adam Chlipala's chapter 4 book and I was having difficulties understanding inductive propositions.

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

For the sake of a running example, lets use:

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

我想我确实理解了使用 Set 像：

I think I do understand "normal" types using Set like:

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

诸如 O 之类的东西只是返回单个 nat 和 SO 类型的对象正在使用 nat 并返回另一个不同类型相同的 nat 。通过不同的对象，我想我的意思是它们具有不同的价值。

and things like O just return the single object of type nat and S O is taking an object of type nat and returning another different one of the same type nat. By different object I guess I mean they have different values.

我感到困惑的是归纳道具的构造函数与归纳类型 Set 有何不同。对于 Set ，它们似乎只是作为函数运行，该函数接受值并返回该类型的更多值。但是对于归纳命题，我很难弄清楚它们的作用。

What I am confused is on how exactly the constructors for inductive props differ from inductive types Set. For Set it seems they just behave as function, a function that take values and return more values of that type. But for Inductive Propositions I am having a hard time figuring out what they do.

例如，将 ev_0 作为简单的例子。我假设这是命题对象（值） ev 0 的名称。由于它本身是 ev 0 ，因此必须是 Prop 命题。但是到底是什么使它成为现实呢？如果这是一个命题，那我可能是错误的。我想这个归纳使我感到困惑。 ev 是返回某种类型的对象（命题）的函数，因此ev 0只是一个命题，但我们没有说什么 ev 0 应该表示（与我对自然数的定义不同，基本情况很清楚其作用）。在python中，我希望看到

For example take ev_0 as a simple example. I assume that is the name for the propositional object (value) ev 0. Since it's by itself ev 0 must be a Prop a proposition. But what exactly makes it true? If its a proposition it could be false I assume. I guess the induction is confusing me. ev is the "function that returns objects of some type (proposition)", so ev 0 is just a proposition, but we have not said what ev 0 should mean (unlike in my definition of natural number the base case is clear what its doing). In python I would expect to see

n == 0：返回True

或其他基本情况。但是在这种情况下，它看起来像是在指向自身，而不是指向 True 之类的圆形对象。我知道我有一个基本的误解，但我不知道我到底不明白什么。

or something for the base case. But in this case it seems circular pointing to itself and not to something like True. I know there is a foundational misconception I have but I don't know what exactly what I am not understanding.

同样的名字让我感到困惑。在 nat 中，名称 O 对于构建/构造对象至关重要。但是在归纳定义中， ev_0 似乎更像是实际值 ev 0 的标签/指针。所以我假设 ev_SS == ev_0-？ EV 2 并没有什么意义，但我不知道为什么。这里的标签与使用 set 的归纳类型的标签有何不同？

Also whats confusing me is the naming. In the nat the name O was crucial for building/constructing objects. But in the inductive definition ev_0 seems to be more like a label/pointer to the real value ev 0. So I'd assume ev_SS == ev_0 -? ev 2 doesn't really make sense but I don't know why. How are the labels here acting differently from the labels in the inductive types using set?

对于 ev_SS 那更加令人困惑。因为我不知道标签在做什么，这当然使我感到困惑，但请看这是怎么回事：

For ev_SS thats even more confusing. Since I don't know what labels are doing of course thats confusing me but look how this is pointing:

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））。

so given a natural number n I assume it returns the proposition ev n -> ev (S (S n)) (I am assuming forall n : nat is not part of the proposition object and its just there to indicate when the constructer that returns propositions works). So forall n : nat, ev n -> ev (S (S n)) isn't really a proposition but ev n -> ev (S (S n)).

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

Can someone help me clarify how inductive proposition type really work in Coq?

请注意，我并没有真正理解 Set 与 Type 之间的区别，但是我相信

Note I don't truly understand the difference between Set vs Type but I believe that would be a whole other post by itself.

更多评论：

我还在玩这个游戏，并且做了：

I was playing around with this some more and did:

Check ev_SS

，令我惊讶的是：

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

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

I think this is unexpected because I didn't expect that the type of ev_SS (unless I am misunderstanding what Check is suppose to do) would be the definition of the function itself. I thought that ev_SS was a constructor so in my mind I thought that would do a mapping in this case nat -> Prop so of course thats the type I expected.

推荐答案

因此，首先，对于您可能会对此感到困惑，但它可能比您想的要简单！

So, first, it is normal for you to be confused by this, but it might be simpler than what you think!

您会混淆两个不同的概念，所以让我们一次来看一个。首先，您提到 ev 0 是一个命题，并且想知道是什么使它成立。您将在某个时候了解到命题和类型是相同的东西，并且 Prop 和 Set 和 Type 并不是这些事物本质上是不同的。

There are two distinct concepts you are confused about, so let's take them one at a time. First, you mention that ev 0 is a proposition, and wonder what makes it true. You will learn at some point that propositions and types are the same things, and the distinction between Prop and Set and Type is not that those things are different inherently.

因此，当您定义类型（或命题）时， nat ，您正在创建一个新类型，并描述其中存在哪些值。您声明值 O ，即 nat 。并且您声明在传递 S ，即 nat > nat 。

So, when you define the type (or proposition) nat, you are creating a new type, and describing what values exist within it. You declare that there is a value O, that is a nat. And you declare that there is a parameterized value S, that is a nat, when passed a nat.

以同样的方式，在定义类型（或命题）时， ev ，您正在创建一个新类型（嗯，它实际上是由 nat 类型的值索引的一类类型），并描述这些<$ c中存在的值$ c> ev 类型。您声明值 ev_0 ，即 ev 0 。并声明存在一个参数化值 ev_SS ，即 ev（S（S n））传递了 n：nat 和 ev n 。

In the same way, when you define the type (or proposition) ev, you are creating a new type (well, it's actually a family of types indexed by values of type nat), and describing what values exist within those ev types. You declare that there is a value ev_0, that is an ev 0. And you declare that there is a parameterized value ev_SS, that is an ev (S (S n)), when passed a n : nat and an ev n.

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

So you made the proposition be true by having ways of creating values within it. You can also define a false proposition by having no constructors, or having constructors that can never be called:

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

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

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

I have declared two now types (or proposition), but there's no way to witness them because they either have no constructors, or no way to ever call those constructors.

现在有关事物的命名， ev_0 ， ev_SS ， O 和 S 都是相同的实体：构造函数。我不确定您为什么认为 ev_0 是指向值 ev 0 的指针。

Now regarding the naming of things, ev_0, ev_SS, O, and S are all the same kind of entity: a constructor. I'm not sure why you think that ev_0 is a pointer to a value ev 0.

没有任何意义将命题分配给 ev n 作为命题，除非这是一个命题，如果有办法的话构造类型为 ev n 的值，如果没有办法构造类型为 ev n 。

There is no meaning to assign to ev n as a proposition, other than it's a proposition that may be true if there is a way to construct a value with type ev n, and may be false if there is no way to construct a value with type ev n.

但是，请注意， ev n 精心设计为适合<$ c只是偶数的$ c> n s，对于奇数的 n s来说是无人居住的。从这个意义上说， ev 抓住了一个命题。如果收到类型为 ev n 的值，它实际上会断言 n 是偶数，因为类型 ev n 仅包含偶数值的居民：

However, note that ev n has been carefully crafted to be inhabited for exactly those ns that are even, and to be uninhabited for exactly those ns that are odd. It's in this sense that ev captures a proposition. If you receive a value of type ev n, it essentially asserts that n is an even number, because the type ev n only contains inhabitants for even values:

• 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））


• 等。

• ev 0 contains 1 inhabitant (ev_0)
• ev 1 contains 0 inhabitant
• ev 2 contains 1 inhabitant (ev_SS 0 ev_0)
• ev 3 contains 0 inhabitant
• ev 4 contains 1 inhabitant (ev_SS 2 (ev_SS 0 ev_0))
• etc.

最后，对于 Set 之间的差异， Prop 和 Type ，这些都是您可以在其中创建归纳类型的Universe，但是它们具有某些限制

Finally, for the difference between Set, Prop, and Type, these are all universes within which you can create inductive types, but they come with certain restrictions.

Prop 可以优化代码生成。从本质上讲，这是程序员（一种类型）将某种类型标记为仅用于验证目的，而从未用于计算目的的一种方式。结果，类型检查器将迫使您从不计算 Prop 范围内的证明，并且代码生成将知道它可以丢弃那些证明，而不会

Prop enables an optimization for code generation. It's essentially a way for you, the programmer, to mark some type as being only used for verification purposes, never used for computation purposes. As a result, the type-checker will force you to never compute on proofs within the Prop universe, and the code generation will know that it can throw away those proofs as they don't participate in computational behavior.

Set 仅仅是对 Prop 的限制

您应该真正尝试不要想到 Prop 是与 Set 不同的神奇事物。

You should really try to not think of Prop as being a magical thing different than Set.

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

The following might help you: we could rewrite the definitions of nat and ev, in a completely equivalent way, as:

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 的输出。

Any time you see a type looking like a -> b, it's really a short-hand for forall (_ : a), b, that is, we expect an input of type a, and return an output of type b.

原因我们在 ev_SS 中写 forall（n：nat）的原因是我们必须第一个参数的名称，因为第二个参数的类型将取决于它（第二个参数的类型为 ev n ）。

The reason why we write forall (n : nat) in ev_SS is that we have to give a name to the first argument, because the type of the second argument will depend on it (the second argument has type ev n).

这篇关于Coq中的归纳命题如何工作？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！