问题标签 [coq-tactic]

使用 Coq 8.4pl3，我在使用eqn:归纳时遇到错误：参考手册中归纳下未列出的变体。

如果我只用简单的“归纳 H”代替最后一步，我不会收到任何错误，但是使用上面的 eqn: 参数，我会收到错误：

错误：a 用于结论。

（以前在定理语句中缺少一个条件，并且相同的错误列出了标识符d。）

参考手册将“在结论中使用”列为使用assert的错误。从某种意义上说，在幕后，eqn:可能正在生成断言，但我在上下文中没有可见的标识符a，而且我看不到 Coq 试图自动使用它做什么。

尝试将证明的开头替换为

现在进行归纳的尝试给出了与以前相同的错误，只是使用H而不是a。（当定理缺少附加条件时，Coq 还明确地在上下文中添加了一个d，与假设H相同。）

我怎样才能在这里前进？我试图避免从上下文中丢失信息。

我有定义my_def1：

我想写另一个my_def2类似于下面的定义并添加一个总是返回my_def1的公理，所以：proj_bytes vlSome bl

我的问题是我怎样才能完成my_def2和写相axiom​​关的proj_bytes vl？

或者问题是如何从类型list memval转换为 list byte[decode_int接受list byte]？

这是 的定义memval：

我创建了这个示例类型来演示我遇到的问题：

现在很清楚foo_1 0 <> foo_2 0，但我无法证明这一点：

这将返回错误

不是可区分的平等。

inversion H根本不会改变上下文。奇怪的是，如果我改变foo了Prop，Type那么证明就会通过，但我不能在我的实际代码中这样做，因为它会在其他地方引起问题。

我怎样才能让这个证明通过？为什么这首先会出现问题？

我有以下引理，但证明不完整：

这个证明失败了

这似乎eq_S是证明这一点的方法，但我不能应用它（它不能识别n + 1为S n: Error: Unable to find an instance for the variable y.）。我也试过ring了，但找不到关系。当我使用rewrite时，它只是减少到相同的最终目标。

我怎样才能完成这个证明？

在很多 Coq 代码中，比如在标准库中的集合定义中，我看到过这种表示法：

|-*(bar-hyphen-star) 是什么意思？

我的搜索没有出现任何结果，但是标点符号很难搜索，所以如果这是重复的，请见谅！

在证明中，我想简化(negb (negb true))为true（同样使用false）。

我知道 Coq 的negb_involutive程序，但由于我的教科书没有介绍它，我认为我应该设法仅使用rewriteor来模仿它的功能apply。

在我的 coq 开发过程中，我正在学习如何创建针对我的问题领域的新策略，就像 Adam Chlipala 教授一样。

在该页面上，他描述了如何通过环绕响应各种有趣条件repeat的 a来创建强大的策略。then 迭代，允许进行深远的推断match。repeat

使用repeat有一个警告（强调我的）：

我们在这里使用的repeat被称为tactical或 tactic 组合器。的行为repeat t是循环运行t，t在所有生成的子目标上运行t，在它们生成的子目标上运行，等等。当t此搜索树中的任何一点失败时，该特定子目标将留给以后的策略处理。因此，重要的是永远不要使用repeat总是成功的策略。

现在，我已经有一个强大的战术在使用，auto. 它同样将步骤链串在一起，这一次是从提示数据库中找到的。从auto的页面：

auto要么完全解决目标，要么保持原样。auto并且trivial永远不会失败。

嘘！我已经在策划auto的提示数据库上投入了一些精力，但似乎我被禁止将它们用于战术使用repeat（即有趣的战术）。

是否有一些变体auto可能会失败，或者在循环中正确使用？

例如，当这个变体“使[目标]完好无损”时，它可能会失败。

编辑：auto无论如何，将其合并到循环中并不是“正确”的方法（请参阅this），但是 auto 失败版本的实际问题可能仍然很有趣。

在我的 coq 开发过程中，我正在学习如何创建针对我的问题领域的新策略，就像 Adam Chlipala 教授一样。在该页面上，他描述了如何通过结合来创建强大的自定义repeat策略match。

现在，我已经有一个强大的单发战术在使用，auto. 它将从提示数据库中找到的步骤链串在一起。我已经投入了一些精力来管理这些提示数据库，所以我也想继续使用它。

然而，这提出了一个问题。 目前尚不清楚将auto's 的功能合并到定制策略中的“正确”方式是什么。

例如，由于（按其页面）auto总是要么解决目标要么什么都不做，将它放在循环中并不比在循环后调用它一次更强大。

要了解为什么这不理想，请考虑一种直接调用 的单个“步骤”的假设方法，auto如果可以进行更改（而不是仅在解决目标时），则该步骤成功，否则失败。这样的单步可以与匹配重复循环中的自定义行为交错，允许我们在搜索树中的例如try contradiction或try congruence中间点。

是否有很好的设计模式可以将auto's 的功能整合到自定义策略中？

的行为是否可以auto分解为我们可以使用的“单步”策略？

我正在使用 Coq 8.5pl1。

举一个人为但说明性的例子，

现在，我只想将参数简化为加倍，而不是除此之外的任何部分。（例如，因为其余的已经仔细地放入正确的形式。）

这将外部 (2 + ...) 转换为 (S (S ...)) 以及展开双倍。

我可以通过以下方式匹配其中之一：

我怎么说我想简化所有这些？也就是说，我想得到

无需为每次调用加倍设置单独的模式。

我可以简化，除了 double 本身

我目前正在寻找一种从一些依赖类型语言（可能是 Coq）中的归纳定义生成 LaTeX 推理规则（水平线样式）的方法。

我找到了这个包，但它看起来很脆弱，没有很多最近的更新，并且每当它遇到 unicode 时都会默默地失败。

我想知道的是，我可以滥用 Coq 在 OCaml 中编写 Tactics 来检查Inductive定义并将其格式化为 LaTeX 的能力吗？显然我会自己编写格式化代码，但我想知道如何获得 AST 表示

这里和这里有一些插件介绍教程，但它们只提供基础知识，而且我还没有找到插件 API 的真正文档，所以我不确定如何获得归纳类型的 OCaml 表示，例如，类型的名称，或该类型的目标。

这已经完成了吗？是否有现有的工具可以做到这一点，或者类似的东西，我可以用作例子吗？