問題タブ [coq-tactic]

Coq 8.4pl3 を使用すると、リファレンス マニュアルの誘導に記載されていないeqn:バリアントの誘導でエラーが発生します。

最後のステップを単純な「誘導 H」に置き換えると、エラーは発生しませんが、上記の eqn: 引数を使用すると、次のエラーが発生します。

エラー: 結論に a が使用されています。

(以前は、定理ステートメントに欠落している条件があり、同じエラーで代わりに識別子dがリストされていました。)

参照マニュアルには、 assertの使用によるエラーとして「結論で使用されます」がリストされています。舞台裏でeqn:がアサーションを生成している可能性があることはある程度理にかなっていますが、コンテキスト内に識別子a が表示されていないため、Coq が自動的にそれを使用して何をしようとしているのかわかりません。

証明の冒頭を

帰納法を試みると、 a の代わりにHを使用するだけで、以前と同じエラーが発生します。(定理に追加の条件がない場合、Coq はまた、仮説Hと同じようにコンテキストにdを明示的に追加しました。)

ここはどうすれば前に進めますか？コンテキストから情報が失われないようにしています。

私は定義を持っていますmy_def1：

以下のような別の定義を書き、常に を返す公理を追加my_def2したいと思います。my_def1proj_bytes vlSome bl

私の質問は、関連する情報をどのように完成させmy_def2て書くことができますか?axiomproj_bytes vl

list memvalまたは、タイプから list byte[ decode_intaccepts list byte]にキャストするにはどうすればよいですか?

の定義は次のmemvalとおりです。

私が抱えている問題を示すために、このサンプルタイプを作成しました。

明らかfoo_1 0 <> foo_2 0になりましたが、これを証明することはできません:

これはエラーを返します

差別可能な平等ではありません。

inversion Hコンテキストをまったく変更しません。奇妙なことに、 をfooからPropに変更するとType証明は通りますが、他の場所で問題が発生するため、実際のコードでこれを行うことはできません。

どうすればこの証明を通過させることができますか? そして、そもそもなぜこれが問題なのですか？

証明が不完全な次のレンマがあります。

この証明は失敗します

これeq_Sを証明する方法のようですが、適用できません（:n + 1として認識されません）。も試しましたが、関係が見つかりません。を使用すると、同じ最終目標になります。S nError: Unable to find an instance for the variable y.ringrewrite

どうすればこの証明を完成させることができますか?

標準ライブラリのセットの定義のように、多くの Coq コードで、この種の表記を見てきました。

|-*(バー-ハイフン-スター) とはどういう意味ですか?

検索しても出てこなかったのですが、句読点の検索が難しいので、重複していたらすみません！

証明では(同様に) に単純化(negb (negb true))したいと思います。truefalse

Coq の手順は知っていますが、私の教科書では紹介されていないので、 ornegb_involutiveのみを使用して何とかその機能を模倣する必要があると思います。rewriteapply

私の coq 開発では、Adam Chlipala 教授のように、自分の問題領域に合わせた新しい戦術を作成する方法を学んでいます。

そのページでは、さまざまな興味深い条件に対応する をラップrepeatすることで強力な戦術を作成する方法について説明しています。matchその後repeat、反復して、広範囲にわたる推論を可能にします。

の使用にrepeatは警告があります（強調は私のものです）：

ここrepeatで使用する は、戦術的、または戦術コンビネータと呼ばれます。の動作は、 running 、生成されたすべてのサブゴールでの実行、生成されたサブゴールでの実行などrepeat tをループします。この検索ツリーの任意の時点で失敗すると、その特定のサブゴールは後の戦術によって処理されます。したがって、常に成功する戦術では決して使用しないことが重要です。ttttrepeat

今、私はすでに強力な戦術を使用していますauto. 同様に一連のステップをつなぎ合わせますが、今回はヒント データベースから見つけました。のページからauto:

autoゴールを完全に解決するか、そのままにしておくかのいずれかです。autoそしてtrivial決して失敗しない。

ブー！私はすでに のヒント データベースのキュレーションにいくらかの労力を費やしてきましたが、それらを使用して戦術(つまり、興味深い戦術) にauto使用することは禁じられているようです。repeat

auto失敗する可能性がある、またはループで正しく使用される可能性のあるバリエーションはありますか?

たとえば、このバリアントは「[ゴール] をそのままにしておく」場合に失敗する可能性があります。

EDIT :autoループに組み込むことは、とにかくそれを行う「正しい」方法ではありません (これを参照してください)。

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

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

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

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

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

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

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

Coq 8.5pl1 を使用しています。

人為的ではあるが実例となる例を作るために、

ここで、引数を double に単純化するだけで、それ以外の部分は単純化しません。（たとえば、残りはすでに慎重に正しい形に入れられているためです。）

これにより、外側の (2 + ...) が (S (S ...)) に変換され、ダブル展開が行われました。

次のようにして、それらの1つに一致させることができます。

それらすべてを単純化したいというのはどうすればよいでしょうか。つまり、手に入れたい

double への呼び出しごとに個別のパターンを配置する必要はありません。

double 自体を除いて単純化できます