3

私の coq 開発では、Adam Chlipala 教授のように、自分の問題領域に合わせた新しい戦術を作成する方法を学んでいます。そのページでは、たとえば と組み合わせrepeatて強力なカスタム戦術を作成する方法について説明していますmatch。

今、私はすでに強力なワンショット戦術を使用していますauto. ヒント データベースから見つかったステップのチェーンをつなぎ合わせます。ヒントデータベースのキュレーションにも力を入れているので、これからも使い続けたいと思います。

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

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

これが理想的でない理由を理解するために、 の 1 つの「ステップ」を直接呼び出す仮想的な方法を考えてみましょう。この方法はauto、変更を加えることができれば (目標を解決した場合のみではなく) 成功し、それ以外の場合は失敗します。このような単一ステップは、一致の繰り返しループでカスタム動作とインターリーブすることができ、検索ツリー内の中間点try contradictionなどを可能にします。try congruence

autoの機能をカスタム戦術に組み込むための優れた設計パターンはありますか?

の行動は、使用できるauto「シングル ステップ」戦術に分解できますか?

4

1 に答える 1

2

代わりに私がすることは、 内に他の戦術を組み込むことautoです。優先度番号 (0 が最高の優先度)、ヒントを使用する必要があるときにフィルターするパターン、そしてもちろん適用したい戦術と追加したいベースを指定するHint Extern num pat => mytactic : mybaseコマンドを使用して、これを行うことができます。へのヒント (デフォルトの を使用しないでください。代わりにカスタム ベースを作成し、それを で呼び出します。検索にベースからの補題を含めたくない場合は、偽のベース:を追加します)。numpatmytacticmybasecoreauto with mybasecorenocoreauto with mybase nocore

autoに非常に依存し始めた場合は、代わりに、ほぼ同等で動作の良い に切り替えtypeclasses eauto with mybaseます。その名前が示唆するものとは反対に、これは型クラスとは何の関係もない汎用的な戦術です (それが機能するヒントベースを明示的に提供する限り)。知っておくべき主な動作の違いの 1 つは、検索の深さがデフォルトで無制限であることです。したがって、無限ループの可能性に注意するか、バリアントで有限制限を修正してくださいtypeclasses eauto num with mybase。

于 2016-12-17T16:25:27.743 に答える