问题标签 [ltac]

假设我有一个像这样的策略（取自 HaysTac），它搜索一个参数来专门化一个特定的假设：

但是，我想写一个策略来搜索n参数来专门化一个策略。关键是它需要回溯。例如，如果我有以下假设：

如果我写do 2 (find_specialize_in H)，它可能会选择x2实例化它，然后尝试找到第二个参数失败。所以我需要我的重复循环能够回溯它选择专门化早期参数的参数。

是否有可能做到这一点？我怎样才能创建一个回溯其先前迭代选择的策略循环？

如果有一种方法可以定义一个“本地”Ltac 表达式，我可以用它来证明一个引理但在外面不可见？

假设我有一些编程语言，具有“有类型”关系和“小步”关系。

这里的关键细节是，对于每个术语变体，只有一个可能匹配的 HasType 变体。

假设我想证明一个进度引理，但我也希望能够从中提取一个解释器。

这给出了错误Inversion would require case analysis on sort Set which is not allowed for inductive definition hasType.

我理解它为什么这样做：inversion对 sort 的值执行案例分析Prop，我们不能这样做，因为它在提取的代码中被删除了。

但是，由于术语变体和类型派生规则之间存在一一对应的关系，我们实际上不必在运行时执行任何分析。

理想情况下，我可以应用一堆看起来像这样的引理：

每个案例都有一个这样的引理（或者是这些案例的结合的单个引理）。

我看过Derive Inversion但它似乎没有做我在这里寻找的东西，尽管我可能没有正确理解它。

有没有办法进行这种“只有一个案例的案例分析”？或者为了得到Prop证明所隐含的等式，这样我就只能在我提取的解释器中写出可能的情况？可以使用 Ltac 或 Deriving 机制自动导出这些引理吗？

我正在尝试将 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）：

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

通过CpdtTactics.v：

[...]成功当且仅x在 list 中ls，用左关联嵌套元组表示。

Ltac inList x ls := match ls with | x => idtac | (_, x) => idtac | (?LS, _) => inList x LS end.

这似乎不典型。列表的尾部不是按惯例位于元组的右侧吗？

考虑以下发展， Adam Chlipala 的simplHyp一个孤立部分：

查看内联注释 -G一开始就匹配，最终用于验证最终目标是否保持不变。这是为了排除injection H可能修改目标或添加无关假设的可能性吗？

我正在尝试学习如何做 Coq 证明自动化 à la Chlipala/ crush。为此，我想知道自动分解单例归纳类型的便捷方法是什么，例如在解决以下问题时：

我只想在有意义的时候自动分解这些- 也就是说，只有当我这样做不会丢失任何信息时。那可能吗？

例子：

simple1有效，但simple2失败了

我想使用rewrite_strat/Hint Rewrite的判别树来编写我自己的证明搜索，使用impl关系来模拟apply。但setoid_rewrite只有当我使用而不是impl重述引理时才有效，这很烦人。有没有办法接受类型的引理并使用关系？impl->setoid_rewriteA -> Bimpl

考虑以下发展：

这打印H != n。我发现这非常令人惊讶，因为范围内的唯一假设是n和done n- 并且done n已经由顶级匹配的第一个分支发送。

如何在done n不明确引用的情况下进行匹配n，如第二个匹配的第一个分支？

I believe the title is pretty self explanatory : https://en.wikipedia.org/wiki/Conditional_proof

I would like to have a tactic where I assume a proposition and proceed to find another one, if succeeded, then I have found that the first proposition implies the second one and this is put as an hypothesis in the context.

So for example Ltac cp P Q creates a subgoal Qand puts Pin the context. If I can indeed reach the subgoal Q, then the subgoal is discharged and P->Q is added to the context. How can I achieve this ?

Edit: It is clear that while proving assert (P->Q). intro. does the job, but I cannot combine them into a Ltac tactic, it gives an error of No focused proof (No proof-editing in progress).