问题标签 [proof-general]

我在 Ubuntu 中使用 Coq 8.11 和 Proof-general。我写的：

Ltac 示例 1 := 失败。

并成功。假设我想使用 unicode 符号：

Proof-General -> Display -> Quick Options -> Unicode Tokens

然后我再次写：

Ltac 示例 2 ≔ 失败。

并因错误而失败：

错误：语法错误：词法分析器：未定义的标记

所以我去一些编辑器并编写序列“：=”并在编写时复制粘贴它：

Ltac 示例 3 := 失败。

很高兴我又成功了。

上面出现了许多您可以想到的符号 |-、/\、/ 等。

我该如何解决？

当我尝试复制粘贴验证代码时，有时会出现 [...]（即使我没有复制任何此类内容）并且我无法删除它。我必须撤消副本才能摆脱它。这是什么意思？

谢谢。

我正在尝试运行带有一般证明的 emacs 来打开 Coq 文件。但是，当我打开 emacs 时，我收到以下错误消息：

我的emacs文件如下：

关于如何使我的 emacs 与 coqtop 一起工作的任何建议？

有人可以解释如何完成这个证明吗？（请不要给出实际答案，只是一些指导:)

该练习来自 SF 第 1 卷，如标题所述，内容如下：

现在，我试图在介绍完所有术语后解决这个injection问题。H0在injection重写之后H2，我最终达到了以下目标，我不知道如何前进。

很明显，如果我设法添加:: l到等式的两边，那么我可以完成reflexivity，但是什么策略可以让我添加:: l到两边？

此致

从软件基础第 1 卷的逻辑一章中，我们看到了列表反转的尾递归定义。它是这样的：

然后，我们被要求证明它们的等价性tr_rev，rev很明显它们是相同的。不过，我很难完成归纳。如果社区提供有关如何处理此案例的任何提示，将不胜感激。

据我所知，这是：

至此，我有了这一套假设和目标：

现在，[] ++ [x]显然与它相同[x]但simpl无法简化它，我无法想出一个Lemma可以帮助我的方法。我确实证明了app_nil_l（即forall (X : Type) (x : X) (l : list X), [] ++ [x] = [x].），但是当我尝试用它重写时，app_nil_l它会重写等式的两边。

我可以将其定义为公理，但我觉得那是作弊:-p

谢谢

我正在使用 proof-general 来编写 Coq 证明。

当我C-c C-n在证明中使用时，我的光标移动到下一行，但当前行没有格式化。例如，如果我输入：

我的光标移动到下一行，但intros n.仍然不缩进。所以我必须返回一行，走到行尾并点击<RET>自动缩进 coq 语句。此时，proof-general认为该语句已更改，我必须重新运行它。

理想情况下，我会C-c C-n自动缩进它正在运行的行，而不是转到下一行。

我怎样才能做到这一点？

每次我尝试使用 CoqIDE 编译器 (v8.13.2) 编译在此链接上找到的 CoQ 描述时，都会显示以下错误消息

我遇到了CoQ 问题日志中描述的战术失败的潜在解决方案。但是，我不知道如何正确应用它。

此外，我不确定与错误项目符号相关的问题是否是上述问题的结果。

作为我自己的练习，我试图在二叉树上定义和证明一些属性。

这是我的 btree 定义：

我想证明的第一个属性是 btree 的高度至少log2(n+1)是n节点数。所以我简单地定义countNodes了：

并且heightTree：

现在，这是我的（不完整的）定理。任何人都可以向我提供有关如何完成此归纳的提示吗？看来我应该有 2 个基本案例（Leaf和Node _ Leaf Leaf），我该怎么做？

剩余目标：

PS：当我试图证明任何节点的度数只能是 0、1 或 2 时，我遇到了类似的问题。在归纳步骤上也有问题。