问题标签 [coq]

我是 Coq 的新手。我无法使用单位、产品和总和来定义列表、地图和树。我在标题中收到错误消息。评论上面的代码工作正常，下面的代码没有。

编辑 4：事实证明，这实际上只是一般 TTY 输入的限制；导致问题的 OCaml、Coq 或 Emacs 没有任何具体内容。

我正在使用 Emacs 中的 Proof General 开发 Coq 程序，但我发现了一个输入太长的错误。如果要通过 Proof General 提交的区域coqtop包含超过 1023 个字符，Proof General（虽然不是 Emacs）在等待响应时会挂起，并且*coq*缓冲区包含一个额外^G字符，用于超过 1023 个字符。例如，如果一个 1025 个字符区域被发送到coqtop，那么*coq*缓冲区将以两个额外的字符结束^G^G。我无法继续文件中的这一点，我必须终止coqtop进程（使用终端C-c C-x或kill/killall从终端）。

关于这种限制的某些东西来自coqtop其本身。如果生成一个 1024 字符或更长的字符串并将其通过管道输入，例如通过运行

然后一切正常。（同样，coqc也可以正常工作。） 但是，如果我coqtop在终端中运行，我不能在一行上输入超过 1024 个字符，包括结束返回字符。因此，输入 1023 个字符的行然后按回车即可；但是在输入 1024 个字符后，按任何键，包括返回（但不包括删除等），只会发出哔哔声。事实证明ocaml（OCaml 顶层）具有相同的行为：

ocaml工作正常，但如果从终端运行，我不能在一行上输入超过 1024 个字符。由于我的理解是coqtop依赖于 OCaml 顶层（在运行时更明显coqtop -byte），我想这是一个相关的限制。

相关软件版本为：

• 来自Homebrew的OCaml 3.12.1 ；
• 来自Homebrew的Coq 8.3pl3（和 8.3pl2）；
• 证明总则4.1；
• 从Emacs 为 Mac OS X构建GNU Emacs 24.1.1 ；和
• Mac OS X 10.6.7。

我的问题是：

• 怎么样ocaml并且coqtop正在执行这个字符限制？为什么只用于来自终端或 Emacs 的输入，而不是来自管道或文件的输入？
• 为什么Proof General（明显）不知道这个限制会导致挂起错误和神秘^G的s？
• 我该如何解决这个限制？我的最终目标是在 Proof General/Emacs 中使用 Coq，因此可以避开潜在问题的解决方法。

编辑 3：在发现 Ocaml 顶层也存在 1024 个字符的输入限制（我想这是相关的）后，我添加了该信息并删除了原始问题描述，因为它已被完全掩盖和取代。（如有必要，请参阅编辑历史）。

所以我在子目标中有一个错误的假设。这是不同构造函数之间的相等性。如何完成子目标？

我想证明字符串的“自反性”属性。请如果你能帮助我如何进行证明。这是我的代码：

我有一个定理 T，它的证明，以及用于证明它的无数个引理。

我想隐藏引理，只提供定理——主要是因为我不想为引理想出好的全局名称。

我可以将定理、它的证明和引理放在一个模块中，受模块类型的限制，并且只使定理可用吗？

就像是：

如果是这样，有人可以发帖或指出一个简单的例子吗？

是否有任何函数/命令可以使用 Coq 获取/检查一个自由变量，比如 n:U，是否存在于术语/表达式 e 中？请分享。

例如，我想在 Coq 中声明这个“n 不会出现在 e 的自由名称中”。

谢谢，

维拉亚特

Coq 的文档一般告诫不要依赖内置的命名机制，而是选择自己的名称，以免命名机制的更改导致过去的证明无效。

在考虑表单的表达式时remember Expr as v，我们将变量设置v为表达式Expr。但是假设的名称是自动选择的，类似于Heqv，所以我们有：

Heqv: v = Expr

我怎样才能选择我自己的名字而不是Heqv？我总是可以使用该rename命令将其重命名为我喜欢的任何名称，但这并不能让我的证明独立于 Coq 中内置命名机制的假设未来变化。

我想知道是否有人可以告诉我Z3和coq之间的区别？在我看来，coq 是一个证明助手，因为它要求用户填写证明步骤，而 Z3 没有这个要求。但似乎 coq 也有类似于 Z3 的自动战术？又或者 coq 的证明搜索能力没有 Z3 强大？

我正在尝试从 coq 命题（或类似的东西......）中提取证人。

我有类似的东西

（后来证明，有一个明确的类型atom：

我如何提取这样的x？ 文档说

从这样的（exist xp）中，我们可以反过来提取它的见证 x:A（使用消除构造，例如 match）

但我不明白这是如何工作的......

它还说

给定 A:Type 和 P:A->Prop，构造 {x:A | P x} 是一个类型

但是如果我尝试类似的东西Parameter C : {x : atom | x \notin xs}，它会给

假设我有两个函数f，g并且我知道f = g. 是否有一种向前推理的“功能应用”策略，可以让我为他们共同领域f a = g a中的一些人添加上下文？a在这个人为的示例中，我可以使用assert (f a = g a)后跟f_equal. 但我想在更复杂的情况下做这样的事情；例如，