オートの検索とヒントデータベースをカスタム戦略でどのように活用するのですか？

Question

私のcoqの開発では、私の問題ドメインに合った新しい戦術、a la Prof. Adam Chlipalaを作成する方法を学んでいます。そのページで、彼は強力なカスタム戦術を作成する方法を説明します。 repeatとmatchを組み合わせる。

今、私はすでに強力なワンショット戦術を使用しています。auto。これは、ヒントデータベースから見つかった一連のステップをまとめます。私はそれらのヒントデータベースをキュレーションすることに多少の努力をしてきましたので、私もそれを使い続けたいと思います。

ただし、これは問題を示します。 autoの機能をカスタマイズされた戦術に組み込むことが「正しい」方法であるかどうかは不明です。

たとえば、（ページごとに）autoは常に目標を解決するか何もしないので、ループ内に置くことはループの後で一度呼び出すよりも強力ではありません。

これが理想的ではない理由を知りたい場合は、autoという1つの「ステップ」を直接呼び出す仮説的な方法を検討してください（ゴールを解決したときだけではなく） 。このような単一ステップは、マッチリピートループにおいてカスタム動作でインターリーブされ、例えば、 try contradictionまたはtry congruenceである。

カスタム戦略にautoの機能を組み込むための良いデザインパターンはありますか？

autoの動作を「シングルステップ」の戦術に分解できますか？

Answer 1

私が代わりに行うことは、autoに他の戦術を組み込むことです。 Hint Extern num pat => mytactic : mybase.コマンドを使用すると、numが優先番号（0が最高優先順位です）、patヒントが使用されるべきときにフィルタリングするパターン、mytacticおよびmybaseはもちろん適用する方法です。 baseをcoreにしないでください。代わりにカスタムベースを構築してauto with mybaseと呼びます; coreベースの補題を検索に含めたくない場合は、偽ベースnocoreを追加してください：auto with mybase nocore）。

autoに非常に頼りがちなのであれば、私はほとんど同じだが、より良い振る舞いのtypeclasses eauto with mybaseに切り替えるだろう。その名前が示唆しているのとは反対に、それは型クラスとは関係のない一般的な手法です（あなたが明示的にそれが動作するはずのヒントベースを提供している限り）。知るべき主な動作の違いの1つは、検索の深さがデフォルトで無制限であることです。無限ループが発生する可能性があることに注意するか、バリアントtypeclasses eauto num with mybaseで有限限を修正してください。詳細はthe manualをご覧ください。