问题标签 [coqide]

我正在阅读这本书http://www.seas.upenn.edu/~cis500/current/sf/lf-current/这是对 Coq 和自动定理证明的介绍。

我首先完成了 Basics.v 文件，并在同一目录中编译它，生成 Basics.vo。然后我开始研究 Induction.v，并在引用 Basics.v 中的“evenb”函数时出错。完整的错误文本是这样的：

“当前环境中没有找到引用的evenb。”

此外，我正在使用 macOS，它无法识别命令行中的输入“coqide”。我觉得这与我最初的 coq 无法识别“evenb”引用的问题有关。以前，我只通过 IDE 而不是命令行在 Coq 中工作。任何想法如何解决这一问题？

更新

我想安装不同版本的 Coq (8.6)，因为我引用的书是专门为那个版本设计的，我觉得这可能会解决问题。如果有人对执行此操作的最佳方法有建议，请告诉我。

这个问题是基于我的问题https://cs.stackexchange.com/questions/96533/how-to-transform-lambda-function-to-multi-argument-lambda-function-and-how-to-re有该问题中的两个功能和两个术语：

功能：

条款：

我的问题是：如何重写涉及is只有 的术语的术语IS？Coq（或第三方工具）是否有这样的重写功能？Coq 是否有工具来检查重写条款的相等性？

也许这样的重写可以在 Coq 世界之外完成，也许还有其他纯粹的 lambda 演算工具仅具有句法操作？

我刚开始学习coq，我基本上是从教授在课堂上展示的代码中复制了代码（？），但它从来没有在我的笔记本电脑上工作过！我不知道为什么它一直告诉我在当前环境中找不到引用 y。我的 coqIDE 中只有两句话（？）：

我读过一些网页询问类似的问题，但我认为我们没有同样的问题。如果我错了，很抱歉。另外，你能告诉我“Utf8”和“99级”是什么意思吗？

我知道这些都是愚蠢的问题，但我就是不明白。感谢您查看它:)

我想将一些特定的命令和战术着色成不同的颜色，例如我希望“打印”和“定位”命令是灰色的，而“感应”是一些不同于其他战术的特殊颜色。

这在 ProofGeneral 中可能吗？如果它在 ProofGeneral 中不可配置，那么是否可以通过某些 Emacs 机制对其进行配置？

PS：我检查了ProofGeneral 的手册，但找不到任何相关选项。

我正在向库 https://github.com/coq-contribs/zfc添加一些定理

但是有一个不是很好的事情。当我在 CoqIDE 中开发代码时，我必须添加

并重命名所有

至

. 库的所有文件都在

最后一个文件夹的名称很重要。

但是当我想运行“make”命令时，我必须重命名所有内容。

文件“Make”包含文件名和前缀。删除第一行并没有解决问题。

我认为这不是使用 CoqIDE 开发的最佳实践，那我该怎么做呢？

编辑1：

我有“run_coqide.sh”，其中包括

“从 ZFC 需要导入集。”引发错误“找不到物理路径”。

编辑2：

我发现这是一个工作脚本：

这是正常运行还是黑客攻击？

我根据以下内容更改了键绑定：

https://github.com/coq/coq/wiki/Configuration-of-CoqIDE

但现在我无法让它们恢复正常。我如何将它们设置为默认状态？

请注意，Coq 已经更改了文件，我不知道如何撤消我所做的更改。

以防万一网页死在这里是我遵循的说明：

配置备用绑定集 (0) 您需要至少执行一次 CoqIDE 才能使配置文件存在。

(1) 在对这些文件进行任何更改之前，您必须关闭所有正在运行的 CoqIDE 实例。

(2) 需要找到配置文件 coqiderc 和 coqide.keys 的位置：

在 Linux 上，在 ~/.config/coq/ 在 Windows 上，在 %HOME%.config\coq 或 C:\Program Files\Coq\config 在 Mac OS X 上，在 ~/Library/Application\ Support/coq/ (3) 编辑文件 coqiderc 并进行如下更改：

|之前 | 修饰符_for_navigation = "" | |之后 | 修饰符_for_navigation = "" |

(4) 编辑文件 coqide.keys 并在文件底部插入以下行：

(gtk_accel_path "/Navigation/Go to" "F5") (gtk_accel_path "/Navigation/Backward" "F6") (gtk_accel_path "/Navigation/Forward" "F7") (gtk_accel_path "/Navigation/End" "F8") ( gtk_accel_path "/Navigation/Start" "F9") (gtk_accel_path "/Navigation/Interrupt" "F12") (gtk_accel_path "/Navigation/Previous" "") (gtk_accel_path "/Navigation/Next" "") (5) 打开 CoqIDE并测试新绑定是否有效。它们应该出现在导航菜单中。

我正在学习软件基础课程，由于某种原因，我无法获得coqc编译库的命令。

我做了：

但得到错误：

错误：文件 /Users/pinocchio/coq/software_foundations_vol1/Maps.vo 包含库地图而不是库地图

我也尝试使用 coqIDE 进行编译，但出现以下错误：

错误：编译的库 Maps（在文件 /Users/pinocchio/coq/software_foundations_vol1/Maps.vo 中）对库 Coq.Init.Notations 做出不一致的假设

关于我能做什么的任何想法？

如何将 CoqIDE 与超过 2 个窗格一起使用？代码可能会变得非常大，并且很难在一个窗格中跟踪每个定义等。

我用谷歌搜索了这个：

http://web.cecs.pdx.edu/~apt/coq_hints.html

但这并没有太大帮助...

我正在运行 CoqIDE 来阅读教科书系列“软件基础”，我目前正在阅读“逻辑基础”一卷。我刚开始第 2 章（归纳），但是当我尝试运行时

我收到错误声明

The file ...\LF\Basics.vo contains library Basics and not library LF.Basics

我尝试重命名文件所在的目录，并重新编译缓冲区，但这些操作都没有帮助。我应该怎么做才能解决这个问题？

我定义了一个归纳类型，下面是最小的例子。我想使用符号，如 ~ 或 =。语法被识别，但未打印在右上角面板的目标中。

例子：

小组说：

虽然我期望：

我试图重新定义 = 像这样，但没有成功：

或定义一个新符号，但均未成功：

是设置问题吗？我在 Mac 上使用 CoqIde 8.7.2。