问题标签 [coqide]

我是使用 coq/coqIDE 的新手，而且我也不精通计算机，所以我不知道出了什么问题，也不知道该说什么。我试图通过软件基础这本书，但 coqIDE 工作不正常。我正在使用最新的 windows 10 和 coqIDE 8.10.2

第一个问题是当我转到 中的选项卡compile -> compile buffer时Basics.v，coqIDE 不会创建 .vo 文件或 .glob。其他按钮也没有工作。以管理员身份运行 coqIDE 也无法正常工作，但我发现我可以通过手动将 Basics.v 拖到 coqc 应用程序文件中来解决这个问题。

在第一课中我对 coq 的工作没有任何问题，但是在下一课中，当我运行他们所说的时，我们打算将定义从Basics.vinto导入Induction.v

The file C:\Users\...\Coq Files\Tutorial\lf\Basics.vo contains library Basics and not library LF.Basics即使 _CoqProject 文件应包含“-Q . LF”，我也会收到错误消息。

我也可以通过编写“Require Export Basics”来解决这个错误。正确加载，直到我真正尝试从 Basics 调用定义

跑步

工作直到我到达evenb，然后给出错误 The reference evenb was not found in the current environment.，即使它在Basics.v

如果我得到更多的肛门并尝试

我得到错误

最后，如果我尝试

正确加载。

所以我想知道我应该如何修复加载路径，以便项目在不将垃圾放入每个文件中的情况下工作，以及如何使编译选项卡工作。

有一些人在谈论“在顶层打 make”，但我不知道那是什么意思。无论如何，我尝试了它并将 Makefile 作为 .bat 运行，即使我已经正确下载了它，所以不应该有任何需要，但 Makefile 并没有改变任何东西。

我不认为我忘记了什么，提前谢谢。

在 Isabelle 证明助手中，可以单击 Ctrl+单击一个术语，IDE 会将他重定向到相关定义。

这可以用 CoqIde 完成吗？与证明一般？

我想在两种情况下破坏我的列表类型对象，例如：

我对 nat 数字有两个条件：

如何区分目标？< 是否存在任何策略？

我正在尝试在软件基础的 plf 文件夹中的 coq 中编译文件 hw5.v。我想解决绑定，因此我使用命令：

coqc -Q.PLF hw5.v

但它不会编译并给出错误为 coqc: -Q.PLF: no such file or directory。这是以前从未发生过的。如果我执行 man coqc 或 coqc -v，它会给我正确的输出。但它不适用于 -Q 或 -R。有什么办法解决这个问题吗？我的 coq 版本是：8.9.1

我在某种程度上是 Coq 的新手，使用 CoqIDE 8.11，并且看不出我在这里做错了什么。我检查了文档，但没有找到解决问题的方法。

和

我收到一条Syntax error: illegal begin of vernac.消息。知道插入之前定义如下：

而且我已经在引理部分使用它并且没有遇到任何问题。非常感谢任何帮助或提示。

所以，我正在尝试使用“计算逻辑导论”脚本来学习 Coq，并且我得到了一个练习。它是为了证明以下内容：“forall ab, a + S b = S (a + b)”。我得到了“nat_ind”的定义：

我对此进行了尝试，并使用此方法解决了该问题，并且有效：

现在问题来了，我必须解决同样的问题，但我需要立即应用归纳引理，并且在我这样做之前不能使用介绍或归纳策略。我该怎么做？

我试图从我的第一次尝试中删除第一行，但它会引发错误：“在当前环境中找不到引用 b。”

更新：我已经到了某个地方。这是我当前的代码：

最后一个子目标只是 nat，我根本不知道该怎么做。

我试图证明上述问题。我得到了归纳的定义：

这是我的尝试，但不知道如何完成

我请求您的帮助是因为我想知道是否可以允许在 Coq 中定义潜在的无限固定点，以检查当前定义是否最终产生输出。

我已经尝试过新Unset Guard Checking命令，我想精确禁用的是递减参数检查（因为我实际上有错误cannot guess decreasing argument of fix.

我知道在 Coq 中禁用此功能有点可惜，但这只是为了获得一个小的实用程序函数来检查当前定义是否正确，以确保提供递减的参数将在进一步的开发中起作用.

我试图证明eqb_neq：

这是我目前的证明状态：

在证明过程中，我到达了最后一步，我只需要证明附加辅助定理：

我尝试了多种策略，但现在我什至不确定是否可以证明这个辅助定理。

我不确定如何使用归纳法证明基本情况：

我还能尝试什么？任何提示eqb_neq或辅助定理？

谢谢