問題タブ [coq-tactic]

例を使って説明します。

サブゴール:

私の質問は、どのように抽出するかです (P->Q)。私はすでに R を持っていますが、「H0 に H を適用」すると、すべてが評価され、Q が返されます。

私は Coq の初心者で、行き止まりに遭遇しました。おおよそ次のような帰納的な定義があります (前に帰納的に受け入れを定義しました)。

私が証明する必要があるのはこれです：

もちろん、私が得る証明を開始するとき

私は長い間戦術について読んで、h を fn2 などにプラグインできる方法を見つけようとしましたが、それを行う方法を見つけることができません。誰かが私をここに案内して、アイデアを教えてもらえますか?? また、楽しい A を A に単純化するために何かをしようとしましたが、そこでも成功しませんでした。ご助力ありがとうございます！

次の定理を証明したい.

私はすでに次の証拠を手に入れました：

でも今はどうしたらいいのかわからない状況です。以下のものは私の処分です：

そして、次のサブゴールを証明したいと思います。

指定された前提で forall 量指定子を削除するにはどうすればよいですか

つまり、具体的な x : A をどのようにプラグインして、 px を推測できるようにできますか?

タクティカルを使用した有効な Coq 証明が与えられた場合、;それを有効な等価証明に変換するための一般式はあり.ます;か?

多くの Coq 証明では、タクティック;シーケンス タクティカルまたはタクティック シーケンスが使用されます。初心者として、個々のステップが実行されるのを見たいので、 を代用.したいのです;が、驚いたことに、これは証明を破る可能性があることがわかりました。

のドキュメント;はまばらで、明示的な議論は.どこにも見つかりませんでした。の非公式な意味はt1; t2

現在の証明コンテキストでt2の実行によって生成されたすべてのサブゴールに適用されます。t1

そして.、現在のサブゴールでのみ動作し、それが異なる動作を説明するのだろうか? しかし、特に代用による破損を修復するための一般的な解決策があるかどうかを知り.たい;.

次の 3 つの引数を持つ and の否定の定義が与えられれば、さまざまなケースを簡単に証明できますが、この証明を 1 つの forall ステートメントで何とか Coq を使用して書きたいと思います。Forall b1 b2 b3 : bool そのうちの 1 つが false の場合は true が返され、3 つすべてが true の場合は false が返されます。この前提を Coq でどのように記述すれば、split などの戦術を使用して接続詞を分割することができますか?

私は次の証明状態を持っています:

だから私はしたいです

そして、それを証明するために証拠の無関連性を使用します。残念ながら、pF = pG型が同じであることはわかっていますが、型が異なるため有効ではありませんH。rewrite Horrewrite H in pFが一致の失敗につながると言ってin pFいるのは、型ではなく値を参照しているためだと思います。

rewritefor タイプに相当するものはありますか？

これが私が完成させようとしている定理です（必要なすべての定義を含む）。

多くの場合、Coq では次のことを行っていることに気付きます。たとえば、証明の目標があります。

a = bとにかく、他のすべてが同じであるため、証明する必要があるだけなので、次のようにします。

次に、そのサブゴールを証明します。

証明を終了します。

しかし、私の証明の一番下にぶら下がっているそれらを持っているのは、不必要な混乱のようです.

Coqには、コンストラクターの等価性を取り、それをコンストラクターパラメーターの等価性に分割するための一般的な戦略がありますsplitか?

私は何度もこの問題に直面してきました: Coq には、同じ等式の両側の一致を含む証明状態があります。

複数の一致を 1 つに書き換える標準的な方法はありますか?

例えば。

で破壊するexpresion_evaling_to_Zと、同じゴールが 2 つ得られます。目標の1つだけを取得する方法を見つけたいと思います。