問題タブ [coq]

免責事項：これは宿題用です

私はcoq初心者なので、これが繰り返しの質問ではないことを願っています。私はこの質問を/持っています/見ましたが、私の質問はまだ答えられていないようです。

私は次の前提を持っています：

私は証明する必要があります：

これまでの私のcoqコード：

行を実行しようとすると、次のエラーが発生しますGoal P.。

エラー：現在の環境で参照Pが見つかりませんでした。

これらは私が思いついた解決策です：

1. に置き換えVariables Q : Prop.ますVariables P Q : Prop.。これに伴う問題はP、前提として想定されることですが、そうではありません
2. Variables P.目標宣言の前に追加します。これにより、構文エラーが発生します。

私は何かが足りないのですか？私はこれを理解できないようです。

依存型を持つプログラミング言語として coq を使用しようとしています。次の小さなプログラムを作成しました。

空でないリストの型を定義し、空でないという証拠があれば、そのようなリストの最初の要素を取得する関数を作成します。先頭項目が 2 つの項目からなる場合はうまく処理できますが、空リストの不可能な場合は処理できません。coqでこれを行うにはどうすればよいですか?

この時点で、 coqとタグ付けされた 81 の質問のすべてではないにしても、ほとんどを読んだと思います。coq に非常に慣れていないので、この非常に単純な質問に対する答えを見つけることができませんでした (SO は非常に基本的なものであるため、SO で質問されていないことは確かです)。

私は宿題に取り組んでいます。そのためには、coq を使用して次のことを証明する必要があります。

• 与えられた: P/Q. ~Q
• 証明: P

これは、私が紙の上で行うのに十分簡単な証明ですが、coq にこれを実行させることはできないようです。

私の戦略は、 と のそれぞれを仮定してP、Qを示し、したがってが成り立つ必要がPあると結論付けることです。P

1. P/Q [前提]

2. ~Q [前提]

   1. P [仮定]

   2. P [前の行をコピー]

      ---

   3. 問【仮定】

   4. ~Q [前の行をコピー]
   5. [矛盾]
   6. P【矛盾解消】
3. P [ の消去\/]

これが紙の上で証明する方法だとすれば、coq で証明する次の coq コードを思い付くことができました。P悲しいことに、 、Q、または~P実現しないと仮定する私の努力:

次の行の試行と、それらが生成するエラーを次に示します。

この時点で考えられることはすべて使い果たしたので、これについて何か助けていただければ幸いです。

私はいくつかの規則を持っていますが、それは基本的に、いくつかの命題 P が決して真ではないということを伴います。Coq を使用して、P が偽であることを証明する必要があります。紙の上でそうするために、私は P が成り立つと仮定し、それから矛盾に到達し、それによって P が成り立たないことを証明します。

P がこの証明に適していると仮定する方法がよくわかりません。これが私が助けを求めていることです。私の現在のコード:

誰かが私がこれを正しい方法で行っているかどうかを確認してもらえますか (そうでなければ、どうすればよいですか?)?

[intros]、[apply]、[assump]、[destruct]、[left]、[right]、[split] というタクティクスでこの補題を証明しようとしましたが、失敗しました。誰か証明の仕方教えてくれませんか?

そして、一般的に、false->P、P/~P などの簡単な命題をどのように証明するのでしょうか?

私は COQ を学んでいて、本の演習の 1 つに行き詰まっています。この本には解決策が書かれていないので、どうすればよいかわかりません。最初はやったけど。これらのステートメントを述語ロジックに変換する必要があります。

コード：

.

助けていただけますか？どうもありがとう！

この問題をできるだけ切り分けるために、次のように Coq セッションを開始するとします。

ここからは、常に truef : A -> Bである一意の関数として関数を定義したいと思います。P a (f a)

これどうやってするの？これはできますか？明らかに、私は次のようなものから始めるべきです

...しかし、これらの仮説に関して実際に関数をどのように記述すればよいでしょうか?

私はこれを証明しなければなりません:

これまでのところ、私はやった：

次に、False を証明する必要があります。どうすればいいのかわかりません。これは証明不可能でしょうか？私を正しい方向に向けることができますか？それとも、ここで何か不足していますか?

編集: Ptival さん、大変お世話になりました...質問の間違いに気付き、質問を編集しようとしたときに、誤って削除ボタンを押してしまい、パニックになり、バックスペースを押してしまいました。:(

forall m n : Z, m < n -> m -n < OCoq でどのように証明しますか? どうもありがとう！

次の定義を前提としています (最初の 2 つはhttp://www.cis.upenn.edu/~bcpierce/sf/Basics.htmlから取得したものです)。

次のことを証明したいと思います。

私が到達できた最も遠いところは、 とblt_nat_flip仮定して証明することblt_nat_flip0です。私は多くの時間を費やし、ほとんどそこにいますが、全体的には必要以上に複雑に見えます. 2つの補題を証明する方法について、より良いアイデアを持っている人はいますか?

これまでの私の試みは次のとおりです。