问题标签 [coqide]

我已经按照此处的说明安装coq并CoqIDE通过了。opam

如说明中所述，每次我必须

导出 OPAMROOT=~/opam-coq.8.9.0

eval `opam 配置环境`

在CoqIDE通过coqide.

否则，它会抱怨

coqide找不到命令。

如何配置我的系统，以便我可以coqide直接通过coqide每次启动？将exportandeval命令添加到~/.bashrcandsource ~/.bashrc对我不起作用。

配置：

• Ubuntu 18.04.2 LTS，64 位
• 奥帕姆 2.0
• coq 8.9.0

我正在使用 coq 中的定义，它需要从定理中产生一些东西，但不能在定义中破坏。

当我尝试破坏 H 时，coq 会发出警告

归纳定义前不允许对排序类型进行案例分析。

我想知道它的原因，以及如何使用定义从“存在”命题中产生一个元素。

我最近从 Windows 切换到 Mac，现在 CoqIde 的行为不像我以前那样。我正在使用 Coq 8.9.1，我不记得我曾经使用的版本，但它最后一次更新是 2018 年秋季。

在我的旧机器上，我可以编译一个文件（例如 file1.v 以获取 file1.vo 和 file1.glob），然后将其导入或导出到同一目录中的另一个文件（例如 writing Require Export file1.），而无需更改加载路径。现在我必须将当前目录显式添加到加载路径，否则会出现“无法找到库...”错误。

这是预期的行为吗？我已经离开 Coq 一段时间了，但我很确定我以前不必这样做。将当前目录添加到加载路径不在我的任何旧工作中。有没有办法让当前目录始终位于加载路径中？

我阅读了这个问题和答案，但那里的建议看起来都归结为将我正在使用的任何目录添加到加载路径（在我正在处理的文件中或其他地方）。

更新：

我能够在文件所在位置从终端打开解决方案（导致当前文件的路径位于 LoadPath 中），但这比我习惯使用 Windows 时更令人头疼。

我不得不在 ~/bin/coqide 中编写一个小 Bash 脚本，它只调用/Applications/CoqIDE_8.8.0/Contents/MacOS/coqide. 在我的主用户的二进制文件目录中添加符号链接找不到它期望与调用符号链接的位置相关的文件。

我无法使用 _CoqProject 文件在 CoqIde 中获得第二个解决方案，最终看到了一些奇怪的行为。使用 coqc 从终端编译有效。

我已将此添加到 Coq GitHub 问题跟踪器（请参阅此处和此处）。

在这个文档链接中有关于除法的有用定理。我尝试Require Import在 CoqIDE 8.9.0 中使用导入它，但是当导入成功时，以下代码失败并出现The reference div_lt_upper_bound was not found in the current environment.

我尝试下载该文件的源代码并通过手动导入它Load，但随后我收到以下消息，没有进一步解释（第一行为红色）：

如何正确加载这些定理？为什么以前的方法不起作用？

我需要在 GitHub 中使用与 Coq 标准库不同的库。但我不知道如何手动设置它以便我可以在 CoqIDE 中使用它。

我需要在 CoqIDE中使用这个库。我已将文件夹下载并保存到我的计算机，但是当我打开 CoqIDE 并编写“需要导入 StringEq”（其中 StringEq 是库中的 Coq 文件的名称）时，我收到错误消息“无法找到库 StringEq”。

有什么方法可以手动设置这个库，以便我可以将它与 CoqIDE 一起使用？（库的 GitHub 页面上的 READme 文件没有说明。）

在 coqide 中构建证明时，我没有找到一种方法

一招一招。因此，像上面的代码那样构建正确的证明变得非常困难。所以我的问题是

• 有没有办法逐步完成上面的代码或
• 你如何像上面的代码那样构造证明？

转发一个命令或转到光标不起作用。

我的问题似乎很常见，但找到的答案都无法解决。我正在关注 Coq 上的软件基础课程，所以我来了命令：

无论我尝试什么，我总是得到以下答案：

“找不到绑定到逻辑路径匹配后缀 <> 和前缀 LF 的物理路径。”

我从 coqIde 编译了 Basics.v，并且正确创建了 Basics.vo 文件。我还从 coqc 命令行编译了它，正如某处建议的那样，我的 _CoqProject 文件存在于与 Basics.v 相同的文件夹中，并指出：-Q . LF _CoqProject 参数设置为“附加到参数”。

当我加载 Basics.v 时，我在 CoqIde 底部看到“从 ..._CoqProject 读取选项”，我将 lf 文件夹放入 coq 的 LoadPath 中的文件夹中。

我还能检查什么？

我的系统是 Windows 10。我运行 CoqIde 8.9.1

谢谢！

以标准方式，我对这样的列表进行归纳

• 审批为lst
• 证明x::lst

但我想要：

• 审批为lst
• 证明lst ++ x::nil

对我来说，x列表中的位置很重要。

我试图写这样的东西，但没有成功。

我有两个相同的子目标，如下所示：

prove_me (x::xs) = true

prove_me (x::xs) = true

证明将是平等的。如何使用第一个目标解决第二个目标？

I am new to Coq. I have a record type and one definition:

I want to proof a trivial lemma:

after unfolding indent subgoal becomes:

How to simplify term?