问题标签 [proof-general]

• 我喜欢使用 Emacs 来运行 ProofGeneral/Coq-mode，因为用于证明的交互式工具很棒。
• 我喜欢使用 Emacs 来运行 Org-mode，因为它是一种非常简单的方式来编写演示文稿，我可以在编写演示文稿的同时编辑文本。

我可以在同一个缓冲区同时拥有这两种东西吗？

我这样做的建议是有一个很好的方法来演示 Coq，我可以在其中隐藏/折叠项目符号并执行 Coq 代码。我所说的“执行 Coq 代码”是指使用交互式工具来检查证明。

我认为这将是介绍 Coq 的好方法。但是，如果您认为这不是一个好主意，我愿意接受介绍 Coq 的好方法。

现在，问题是怎么做！我对所有与之相关的工具都很陌生，甚至不知道是否可能。

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

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

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

我正在做软件基础练习，并且combine_split在尝试证明辅助引理时遇到了困难。

reflexivity在证明过程中应用时，尽管等式显然是正确assert的，但它只是挂在那里。(x, y) = (x, y)

这是实现

为什么会这样？

试图证明以下引理：

我已经尝试在目标中展开 nth_error 和 nth，但我无法找到一种方法来告诉 Coq 打破这两个函数的 Fixpoint 定义。我也尝试对 n 和列表进行归纳，但由于列表中的项目彼此无关，因此它们都无法解决问题。但这显然是一个正确的引理，现在我觉得它是不可证明的，任何人都可以帮我解决这个问题吗？非常感激！

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

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

我打开 emacs，然后打开一个 .v 文件，以便触发 Proof General。但是，这样做的 IDE 非常慢，并且需要很长时间才能上下滚动证明。关于为什么会发生这种情况的任何想法？

配置文件：

如果我做类似的事情 -From mathcomp Require Import ssreflect.它会给我以下错误。

但如果我这样做 -Require Import ssreflect.它编译得很好。这可能是因为我安装了 ssreflect 但不完全是我想要的方式。

但问题是我想要第一种工作方式，因为我有很多这样编写的程序，而且每一个都改变行似乎不合逻辑。

这就是我的 .emacs 文件中的内容 - （我想也许我需要添加任何东西，比如 mathcomp/ssreflect 的路径。我不知道）

如果有人可以帮助我开始From mathcomp Require Import ssreflect.工作，那对我真的很有帮助。

在 DeepSpec 2018 的第 6 讲中，讲师检查了

获得：

然后他继续查看 + 的定义，但在此之前，他在 CoqIde 中禁用了符号的打印。这样 sumbool 就被打印出来了。可以检查最后一个符号。

我怎样才能用 Proof General 做同样的事情？

我正在使用《Certified Programming with Dependent Types》一书，但每次我都发现不同的错误。在我看来，错误来自 Proof General 的编译过程与本书来源的 makefile 之间的不匹配。

1. 如果我使用 make 编译源代码并尝试在 Proof-General 中运行例如 Subset.v，我会得到：

错误：文件 /home/usuario/Desktop/Coq/cpdt/src/CpdtTactics.vo 有错误的幻数 81100（预期为 8600）。它已损坏或使用其他版本的 Coq 编译。

2. 如果我用 make clean 清理 makefile 编译文件并尝试继续使用选项 Coq -> Auto Compilation -> Compile before require 那么它是以下行：

需要提取。

那失败了。最初它因错误而失败：

错误：无法找到库提取。

但是使用上面的选项启用它会给出类似的东西：

回声“需要提取。” > /tmp/ProofGeneral-coqQPJTf0.v coqdep -Q /home/usuario/Desktop/Coq/cpdt/src/ -R /home/usuario/Desktop/Coq/cpdt/src Cpdt /tmp/ProofGeneral-coqQPJTf0.v * 警告: 在文件/tmp/ProofGeneral-coqQPJTf0.v 中，库提取是必需的，并且在加载路径中没有找到！*警告：在文件 /tmp/ProofGeneral-coqQPJTf0.v 中，库提取是必需的，并且在加载路径中没有找到！/tmp/ProofGeneral-coqQPJTf0.vo /tmp/ProofGeneral-coqQPJTf0.glob /tmp/ProofGeneral-coqQPJTf0.v.beautified：/tmp/ProofGeneral-coqQPJTf0.v /tmp/ProofGeneral-coqQPJTf0.vio：/tmp/ProofGeneral-coqQPJTf0 .v

我该如何解决这个问题？

我有一些代码只能在 Coq 8.09.0 中编译 coq 代码。我通常使用的版本是现在最新的版本，即 Coq 8.11.0。我能够使用 opam 开关创建一个新环境并在那里安装 Coq 8.09.0。我用这个版本成功编译了所有文件；但是，我不能在 emacs 中使用一般证明，因为它仍在使用 Coq 8.11.0。我想知道如何使用 Emacs 中的 opam 开关使 Proof General 使用不同的 opam 实例。我尝试在 eshell 中执行以下操作

其中 vst 是opam switch在我的终端的输出中看到的开关的名称：

但是，该eval $(opam env)行的输出如下：

这没有任何意义，因为它理解 opam 的含义，因为它能够很好地执行第一个命令。是否有正确的方法来进行 opam 切换以更改 emacs 使用的内容？有没有办法明确告诉 Proof General 它应该使用哪个 Coq 实例？pacman我应该卸载 Coq 8.11.0 并直接使用（我正在使用 manjaro）安装 Coq 8.09.0吗？