问题标签 [coqide]

使用 CoqIde，有没有办法查看simpl已采取的步骤？我发现我不明白它是如何经常取得结果的。

例子：

我完成了一个有点冗长的证明，但每当我尝试时，Qed我都会收到错误消息Error: This proof is focused, but cannot be unfocused this way。有没有其他方法可以使证明失去焦点？即使我的证明是严格的，我应该只使用承认吗？作为参考，我使用的是 CoqIDE 8.6

我在上下文中有两个假设，但是当我尝试apply一个到另一个时，我得到了错误unable to unify。我应该能够统一它们。这两个假设如下

IHl : forallb func l = true -> All (fun x : X => func x = true) l H1 : All (fun x : X => func x = true) l

我的目标是通过将 IHl 应用于 H1 从 IHl 中获得前提。

我是 Coq 的新手，目前正在阅读 Software Foundations 系列教程。

然而，我一直发现自己Require Export在第一次尝试时很难让零件工作，每个文件似乎都需要一个新的策略才能工作。然而，这一次，我完全被困住了。

在一个文件（Lists.v）中，我可以简单地编写 From LF Require Export Induction.，并且让它工作得很好。

在下一个（Poly.v）中，我根本无法加载 Lists 模块，

除非我先将加载路径添加到当前文件夹：

但是，在下一章中，似乎没有任何效果。

这是我尝试过的：

可以肯定地说：我在这里不知所措，我不知道我在做什么或为什么它不起作用。它以前有效，我在网上找不到任何东西似乎可以给出任何好的答案。

我的 _CoqProject 文件包含-Q . LF

我在 Windows 和 Mac 上都遇到了这个问题。

我正在使用最新版本的 CoqIDE。

我在 CoqIDE 4.5 中收到错误“Basics.vo 包含库 Basics 而不是库 Metalib.Basics”。我正在关注软件基础并将基础知识导入为“需要导出基础知识。”。我还使用相同的 CoqIDE 编译了 Basics。过去我使用的是 CoqIDE 4.2，这在 CoqIDE 4.2 中运行良好。现在我切换到 CoqIDE 4.5，删除了之前编译的 Basics.vo 并再次编译。有人可以帮我吗？

我已经尝试删除之前编译的 Basics.v。还尝试多次重新启动 CoqIDE。

我有一个已经被证明的证明。

其次，我有加法交换性证明的修正。

但是，我不明白 Equal_trans （第 8 行）的用法。如果我理解， Equal_Trans 需要 3 个参数： yxz ？但是为什么在 Add_com lemma 中只有 1 个参数使用 Equal_Trans 呢？

预先感谢您的帮助。

我正在尝试检查 Coq 中两个整数之间的相等性，但我收到此错误：“术语“first = second”的类型为“Prop”，它不是（共）归纳类型。”。Coq 中有没有提供相等检查的库？这是我的代码：

所以我刚刚开始学习coq（到目前为止它已经超出了我的想象）并且我正在尝试做一个基本的证明并且我很迷茫，到目前为止找到了一些帮助但是我认为我应该做 coq 会引发错误。所以在我的编辑部分我有：

在打样框中我有：

在错误框中我有：

当前环境下找不到是什么意思？

如果我定义这样的乘法 ( drugi_c)，我如何证明 eg X*0=0？（如何通过定义证明某事？）

每当我使用“简单”时。在证明而不是 0 = 0 中，我得到了结果的定义。

最后一个简化后的结果。

在那之后写什么simpl.来完成证明？

我正在阅读逻辑基础并下载了它附带的 coq 脚本。

我正在使用 coq v8.8.1，通过 opam 安装。

我在标题中遇到了两个错误，我不确定应该如何调试它们。

第二个错误的完整错误消息是

COQDEP VFILES

*** 警告：在文件 Auto.v 中，库 LF.Maps 是必需的，但在加载路径中没有找到！

我的目标是编译和运行该Induction.v文件。在出现这些错误之前，我使用 coqide 的选项首先“make makefile”然后“make”。