如何使用自动重复自定义策略？

Question

在我的coq开发中，我正在学习如何为我的问题域创建新的策略，la Prof. Adam Chlipala。

在该页面上，他描述了如何通过围绕match包装repeat来创建强大的策略，以响应各种有趣的条件。 repeat然后迭代，允许深远的推论。

使用的repeat有一个警告（重点煤矿）：

，我们在这里使用的repeat被称为战术，或战术组合子。 repeat t的行为是循环运行t，在所有生成的子目标上运行t，在上运行t，它们的生成的子目标等等。当t在这个搜索树中的任何一点都失败时，那个特定的子目标会被稍后的策略处理。 因此，重要的是永远不要使用repeat，这种策略总是成功的。

现在，我已经有了一个强大的战术使用，auto。它类似地串联在一起的步骤链，这次从提示数据库中找到。从auto的页面：

auto要么完全解决目标，要么保持完好无损。 auto和trivial永远不会失败。

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

是否存在的auto一些变化可能出现故障，或否则可以在循环中正确使用？

例如，也许这个变体在“完成目标”时失败。

编辑：结合auto成环是不是“正确”的方式做到这一点呢（见this），但汽车的一个失败的版本实际的问题仍然是可能有趣。

Answer 1

正如@安顿特鲁诺夫所说，如果目标没有改变，你总是可以使用progress战术来使战术失败。在auto的情况下，因为它应该解决目标或保持不变，您还可以将其包装在solve [ auto ]中，这将具有相同的效果，因为如果auto完全不能完全解决目标（here is the doc for solve），它将会失败。