为什么Coq在归纳命题类型中使用未命名的参数？ [英] Why does Coq use unnamed parameters in Inductive Types of Propositions?

问题描述

我正在查看 IndProp ，我看到了：

 失败归纳错误_ev（n：nat）：道具：= 
 |错误的错误_0：错误的错误0 
 | rong_ev_ss：∀n，错误_evn→错误_ev（S（S n））。 
（* ===>错误：归纳类型n的参数不允许
用作其构造函数的类型
中的绑定变量。*）
  

除了它的行为似乎就像在接受参数一样，但是似乎抛出错误。为什么会这样？

文字提供了一些解释，但我不明白：

我不知道不太明白。我不理解的部分是它说的部分：

允许在类型中采用不同的值

为什么说在类型中？类型不是输入，值是输入。为什么这么说呢？似乎非常令人困惑。我（非常模糊地）知道存在依赖类型之类的东西，但是它也指的是什么？不应该是争论吗？构造函数不取值或东西并返回某种类型的对象吗？

为什么似乎归纳类型的签名（实际上我只是查看它作为构建事物的函数是返回某种类型的对象）缺少自变量？

---

从似乎似乎可以解释的文本中获得更多上下文：不是类型，而是从nat到Prop的函数-即数字的属性。请注意，我们已经看到了其他归纳定义，这些归纳定义会产生一些函数，例如list，其类型为Type→Type。此处的新功能是，由于ev的nat参数未命名，在冒号的右侧，因此可以在不同构造函数的类型中采用不同的值：ev_0和S（S n）的类型为0。 ev_SS的类型。
相反，列表的定义在冒号的左侧全局命名X参数，强制nil和cons的结果相同（列表X）。如果我们尝试在定义ev时将nat移到左侧，我们将会看到一个错误...我们可以认为ev的定义是定义Coq属性ev：nat→Prop以及原始定理ev_0：ev 0和ev_SS：∀n，ev n→ev（S（S n））。
这样的构造定理与已证明的定理具有相同的地位。

解决方案

为什么说在类型中？类型不是输入，值是

您需要阅读整个表达式：在不同构造函数的类型中。
而且，实际上，这两个构造函数的返回类型的自然数是不同的：

• 对于 ev_0


• 对于 S（S n） > ev_SS

I was looking at IndProp and I saw:

Fail Inductive wrong_ev (n : nat) : Prop :=
| wrong_ev_0 : wrong_ev 0
| wrong_ev_SS : ∀ n, wrong_ev n → wrong_ev (S (S n)).
(* ===> Error: A parameter of an inductive type n is not
        allowed to be used as a bound variable in the type
        of its constructor. *)

except that it seems to behave exactly as if it was taking an argument but it seems to throw an error. Why is this?

The text provides some explanation but I don't understand it:

what I don't understand specifically it. The part I don't understand is the part it says:

it is allowed to take different values in the types

why is it saying "in the types"? Types are NOT the input, values are. Why is it saying this? It seems extremely confusing. I know (extremely vaguely) that there is such a thing as "dependent types" but is that what it's referring too? Shouldn't it be arguments? Don't constructors take value or "stuff" and return an object of some type?

Why does it seem that the signature of the Inductive type (which really I just view it as a function that builds things are returns objects of some type) missing the arguments?

---

More context from text where explanation seems to appear:

This definition is different in one crucial respect from previous uses of Inductive: its result is not a Type, but rather a function from nat to Prop — that is, a property of numbers. Note that we've already seen other inductive definitions that result in functions, such as list, whose type is Type → Type. What is new here is that, because the nat argument of ev appears unnamed, to the right of the colon, it is allowed to take different values in the types of different constructors: 0 in the type of ev_0 and S (S n) in the type of ev_SS. In contrast, the definition of list names the X parameter globally, to the left of the colon, forcing the result of nil and cons to be the same (list X). Had we tried to bring nat to the left in defining ev, we would have seen an error ... We can think of the definition of ev as defining a Coq property ev : nat → Prop, together with primitive theorems ev_0 : ev 0 and ev_SS : ∀n, ev n → ev (S (S n)). Such "constructor theorems" have the same status as proven theorems.

解决方案

why is it saying "in the types"? Types are NOT the input, values are

You need to read the whole expression: "in the types of different constructors". And, indeed, the natural number is different in the return type of the two constructors:

• It is 0 for ev_0
• And it is S (S n) for ev_SS

这篇关于为什么Coq在归纳命题类型中使用未命名的参数？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！