問題タブ [coq-tactic]

機能が重複している Coq タクティックをたくさん見てきました。

たとえば、仮説に正確な結論がある場合はassumption、apply、exact、trivial、およびおそらく他のものを使用できます。他の例にはdestruct、induction非誘導型 (??) の と が含まれます。

私の質問は：

自然数の関数に関するCoq証明可能な定理を証明するためにこのセットを使用できるという意味で、完全な基本的な戦術の最小セット( などを除く)はありますか?auto

この最小限の完全なセットの戦術は、それぞれが 1 つ (または 2 つ) の機能のみを実行し、その機能を簡単に理解できるように、理想的には基本的なものです。

オンラインコースから、中間を除外した次の単純な定理を証明しようとしましたが、反駁できませんでしたが、ステップ1でほとんど行き詰まりました。

今私は得る：

Iapply Hの場合、目標は になりますがP \/ ~P、これは途中で除外され、建設的に証明することはできません。しかし、 以外ではapply、仮説について何ができるかわかりませんP \/ (P -> False) -> False。含意->は原始的であり、それを分解する方法も分解する方法もわかりませんdestruct。そして、これが唯一の仮説です。

私の質問は、原始的な戦術のみを使用してこれをどのように証明できるかです (ここで特徴付けられているように、つまり、神秘的なautos はありません)。

ありがとう。

Coq タクティックを使用するapply ... with場合、私が見た例はすべて、インスタンス化する変数の名前を明示的に指定することを含みます。たとえば、等式の推移性に関する定理があるとします。

それにapply：

最後の行で、インスタンス化する変数の名前はorまたはその他の名前ではなく、 でapply trans_eq with (m := 1).あることを覚えておく必要があります。mony

私にとって、定理の元のステートメントで使用されているかどうm n oかx y zは問題ではありません。それらはダミー変数または関数の仮パラメーターのようなものだからです。また、定理を定義するときに、私が使用した特定の名前や、他の誰かが別のファイルに書き留めた特定の名前を思い出せないことがあります。

たとえば、変数をその位置で参照して、次のようなものを使用できる方法はありますか?

上記の例では？

ちなみに、私は試しました：apply trans_eq with (1 := 1).そして得ましたError: No such binder.

ありがとう。

Coq で用語を並べ替える方法について一般的な質問があります。たとえば、用語がある場合m + p + n + p、人間は用語を次のようにすばやく再配置できますm + n + p + p(暗黙的に plus_comm と plus_assoc を使用します)。Coqでこれを効率的に行うにはどうすればよいでしょうか?

（ばかげた）例として、

今、私たちは持っています

私の質問は：

m + n + p + pLHS を効果的に書き換えるにはどうすればよいですか?

を使用しようとしましrewrite plus_comm at 2たが、エラーが発生します。Nothing to rewrite.単純に rewrite を使用plus_commすると、LHS が に変更されp + m + n + pます。

効果的な書き直しに関する提案も歓迎します。

ありがとう。

destructはCoq でand、orを分割するために使用できます。しかし、それは暗示的にも使用できるようですか？たとえば、私は証明したい~~(~~P -> P)

正常にdestruct pff.動作するのですが、理由がわかりません。誰かが私のためにそれを説明できますか?

Coqで定理の証明中にまったく新しい変数を導入する方法があるかどうか疑問に思っていましたか?

完全な例として、リストの長さの均一性に関する次のプロパティをここから検討してください。

ここで、任意のリストが偶数の場合、次lのことが成り立つことを証明したいと思います。lengthev_list l

与える：

nここで、新しい自由変数と仮説を「定義」したいと思いますn = length l。手書きの数学では、これができると思いますn。しかし、Coqで同じことをする方法はありますか?

ノート。私が尋ねる理由は次のとおりです。

1. 前にリンクされたページで行われているように、これを定理自体のステートメントに人為的に導入したくありませんがn、これは不自然です。

2. しようとしましたinduction H.が、うまくいかないようです。length lCoq は'sネスのケース分析を行うことができずev、帰納仮説 (IH) は生成されませんでした。

ありがとう。

項がリテラル ゼロかどうかをチェックする次の戦術があるとします。

ここで、戦術にもう少し受け入れてもらいたいと想像してみてください。おそらく、ゼロで変換可能な任意の項。これが目標に基づいて行動する戦術である場合、私はそうします

しかし、これは項を生成するタクティックでは失敗します:

戦術生成用語の変換可能性を確認するにはどうすればよいですか? この特定の例では、それを減らすxか計算する (let xx := eval compute in x

PS: 参考までに、簡略化されていない問題は、 へのFMap一連の呼び出しによって構築された値におそらく一致するキーを効率的に検索しようとしているということですadd。戦術は次のようになります。

この実装ではvalue、マップの代わりに、変換可能でvalueあるが構文的に等しくない用語が含まれている場合、タクティックは誤って を返しNoneます。

証明中に、現在のゴール/サブゴールが同じ定理の後の段階で役立つことが判明した状況に遭遇しました。

assert現在の目標がedであるかのように、現在の目標を補題として「保存」する戦術はありますか?

もちろん、 assertゴールに明示的にコピー&ペーストすることも、現在の定理の前に別の Lemma を書くこともできます。しかし、ショートカットが存在するかどうかは興味があります。

ありがとう。

私が理解していることから、Coq の関数呼び出しは不透明です。場合によっては、unfoldそれを適用してからfold、関数定義/本体をその名前に戻す必要があります。これはしばしば面倒です。私の質問は、関数呼び出しの特定のインスタンスを適用させる簡単な方法はありますか?

最小限の例として、リストのl場合、右追加[]が変更されないことを証明するにはl:

これは次のとおりです。

++ここで、 (ie )の定義を一度適用する必要があります(適用/拡張したくない目標にapp他の定義があるふりをします)。++現在、この 1 回限りのアプリケーションを実装する唯一の方法は、最初に展開++してから折りたたむことです。

与える:

しかし、 で使用する用語の形を理解しなければならないので、これは不便foldです。Coqではなく、私が計算しました。私の質問は次のとおりです。

このワンタイム関数アプリケーションを同じ効果に実装する簡単な方法はありますか?