问题标签 [coq-plugin]

我正在尝试使用 Function 使用度量来定义递归定义，但出现错误：

我在底部发布了整个源代码，但我的功能是

我知道问题出在 foralls 上：如果我用 True 替换它们，它就可以工作。我也知道如果我的右手边使用含义（->），我会得到同样的错误。Fixpoint 适用于 foralls，但不允许我定义度量。

有什么建议吗？

正如所承诺的，我的完整代码是：

我正在测试 AAC 策略库以重写模关联性和交换性。根据Coq 网站，应该：

根据您的安装，修改以下两行，或将它们添加到您的 .coqrc 文件中，替换“。” 带有 aac_tactics 库的路径。

但我不知道如何找到 aac_tactics 库的路径，并使用“。” 没用。

我按照以下方式在 Ubuntu 16.04 LTS 下安装了 Coq：

有谁知道在哪里可以找到图书馆的位置？

我正在测试 Coq 重写策略模关联性和交换性 ( aac_tactics)。以下示例适用于整数 ( Z)，但当整数替换为有理数 ( Q) 时会生成错误。

Require Import ZArith.用etc替换Require Import QArith.的时候报错：

错误：策略失败：未找到模数 AC 的匹配发生。

在aac_rewrite H.

Z和之间也存在类似的不一致问题Q，这与Z/Q范围是否开放有关。

但我不明白为什么 aac rewrite 在这里不起作用。不一致的原因是什么，如何使它对Z和表现相同Q？

我猜 Coq aac_tactics(8.5p1) 应该能够处理 assoc。和交换性。但我不知道如何使用它来证明简单的等式，例如

例如：

产生错误：

错误：策略失败：不是模 A/AC 相等。

将最后一个策略更改为aac_normalise也不能解决它。

如何使用 AAC 证明这些目标？

这个问题是基于我的问题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 策略（目前用 Ltac 编写）移植到 OCaml，以便能够更轻松地扩展该策略（并避免在 Ltac 中模拟一些在 OCaml 中非常标准的数据结构所需的黑客攻击）。

我目前面临以下问题：

1. 我们可以定义一个 OCaml 策略，将 Ltac 表达式k（旨在作为延续）作为参数吗？
2. 我们如何将一个这样的 Ltac 表达式k应用于给定的constr v？
3. 我们如何tac从插件中调用给定的 Ltac 策略？
4. 我们可以从插件代码中将 Ltac 闭包传递给这样一种策略吗？（为了tac ltac:(fun r => ...)在 OCaml 中实现 Ltac 成语）

我对 Coq 资源进行了 grep 搜索TACTIC EXTEND，但没有找到这种方法的一些例子......

running_example作为一个最小的例子，下面是我想在 OCaml 中移植的一个玩具 Ltac 策略，它依赖于现有的 Ltac 策略tac：

到目前为止，我已经获得了以下代码（仅针对点 1）：

非常欢迎任何指示或建议。

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

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

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

我想在 Atom 中开发一些 Coq 代码。我希望能够像往常一样逐行检查我的代码，就像使用 CoqIDE 或 emacs proof general 一样。atom 是否有类似的东西，或者人们如何在 Atom 编辑器中开发 Coq 代码？

一些链接：

https://discuss.atom.io/t/is-there-proof-general-for-coq-in-atom/60862

注意：我主要发现语法高亮。

我正在尝试安装tcoq，但出现以下错误：

有人知道吗：

1. 错误是什么意思？
2. 如何解决？

我在网上看到相关帖子：

https://coq-club.inria.narkive.com/h4i0KOH0/problem-compiling-coq

但这并不是很有帮助。我做了：

正如他们所建议的那样，它似乎工作正常......

我确实这样做make clean了，但这没有帮助。

我刚刚意识到我跳过了安装的第 3 步，但如果它与问题相关或者我想用它做什么，我会知道：

我正在尝试安装游戏手柄，并且需要按照说明进行操作。特别是我运行了以下 3 个命令：

最新错误：

在阅读了那个错误之后，我奇迹般地想到打印两个ocaml和的版本camlp5：

和：

很明显那是错误的，所以也许第一步是修复camlp5工作，4.05.0因为那是我需要的。

我尝试卸载camlp5但它拒绝了！

如何使用插件Paramcoq证明以下自由定理？

如果不可能，那么这个插件的目的是什么？