私の coq 開発では、Adam Chlipala 教授のように、自分の問題領域に合わせた新しい戦術を作成する方法を学んでいます。
そのページでは、さまざまな興味深い条件に対応する をラップrepeatすることで強力な戦術を作成する方法について説明しています。matchその後repeat、反復して、広範囲にわたる推論を可能にします。
の使用にrepeatは警告があります（強調は私のものです）：
ここ
repeatで使用する は、戦術的、または戦術コンビネータと呼ばれます。の動作は、 running 、生成されたすべてのサブゴールでの実行、生成されたサブゴールでの実行などrepeat tをループします。この検索ツリーの任意の時点で失敗すると、その特定のサブゴールは後の戦術によって処理されます。したがって、常に成功する戦術では決して使用しないことが重要です。ttttrepeat
今、私はすでに強力な戦術を使用していますauto. 同様に一連のステップをつなぎ合わせますが、今回はヒント データベースから見つけました。のページからauto:
autoゴールを完全に解決するか、そのままにしておくかのいずれかです。autoそしてtrivial決して失敗しない。
ブー！私はすでに のヒント データベースのキュレーションにいくらかの労力を費やしてきましたが、それらを使用して戦術(つまり、興味深い戦術) にauto使用することは禁じられているようです。repeat
auto失敗する可能性がある、またはループで正しく使用される可能性のあるバリエーションはありますか?
たとえば、このバリアントは「[ゴール] をそのままにしておく」場合に失敗する可能性があります。
EDIT :autoループに組み込むことは、とにかくそれを行う「正しい」方法ではありません (これを参照してください)。