在我的 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 失败版本的实际问题可能仍然很有趣。