coq中的“Some”是啥意思？

Posted 2023-05-08

【中文标题】coq中的“Some”是啥意思？

【英文标题】：What does "Some" mean in coq?coq中的“Some”是什么意思？

【发布时间】：2015-07-17 13:11:38

【问题描述】：

coq 中的关键字/命令“Some”是什么意思？

此外，我如何查看它的定义？考虑到some 这个词的流行度，使用coq some 并没有太大帮助。

【问题讨论】：

强相关：quora.com/What-does-the-Some-command-in-Coq-do

【参考方案1】：

Some 是option 类型的类型构造函数。您可以通过Checking 或Printing 获取有关此类构造函数的一些信息，以获取它们的类型或完整实现。

编辑：option 类型是什么。

它是 Coq 前奏中定义的类型（同样，使用 Check 或 Print 获取有关此类型的信息）。该类型用于陈述关于可选存在类型的事实：对于任何类型A，None : option A 表示没有值，Some A: option A 表示存在值（类型为A）。

这是一个自然数前身的例子：

Definition myPred (n:nat) : option nat := match n with
  | S p => Some p
  | O => None
end.

在本例中，如果您尝试计算O 的前任，您将得到None（没有这样的自然数）。否则，你会得到Some p 这样S p = n。

【讨论】：

那么option是什么类型？

@JRR 尝试打印和检查option

我已经阅读了 option 的描述，但你怎么知道它有那种语义？究竟是什么让你得出这样的结论？

我很困惑，它实际上并没有返回前任，它返回Some 2 sya for Some 3 这似乎与您的描述不符...您能澄清一下吗？

前驱不是自然数上的全函数，因为0没有前驱。所以在这里我选择使用option 类型来使函数总计：对于0，我返回None。对于任何S n，我返回Some n。由pred 的用户来检查哪种情况是返回与pred 0 本身的交易。