2

とタグ付けされた 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実現しないと仮定する私の努力:

Section Q5.

Variables P Q : Prop.
Hypothesis premise1 : P \/ Q.
Hypothesis premise2 : ~Q.

Goal P.

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

+-----------------+---------------------------------------------------------------------+
|      Code       |                                Error                                |
+-----------------+---------------------------------------------------------------------+
| assumption.     | Error: No such assumption.                                          |
| exact P.        | The term "P" has type "Prop" while it is expected to have type "P". |
| apply premise1. | Error: Impossible to unify "P \/ Q" with "P".                       |
| apply P.        | Error: Impossible to unify "Prop" with "P".                         |
+-----------------+---------------------------------------------------------------------+

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

4

1 に答える 1

3

あなたの戦略をよく理解しているかどうかはわかりませんが、正しいようです。

あなたがしたいことは、基本的にP \/ Q分離の2つのケースを考えることです。destruct premise1.これは、2 つの目標 (1 つは whichp: Pで、もう 1 つは which で) を生成するタクティックを介して行うことができますq: Q。この 2 つは簡単に証明できるはずです。

あなたの戦術が失敗した理由:

P : Prop
Q : Prop
premise1 : P \/ Q
premise2 : ~ Q
______________________________________(1/1)
P

  1. assumption.タイプが現在の目標である用語の仮説を調べるだけなので、機能しません。ここにはタイプの用語はありませんP。

  2. exact P.の場合、戦術exact <term>.は目標を解決することになっているため、失敗します。あなたの目標はそうではありませんよね？:)<type><term> : <type>Prop

  3. apply premise1.ゴールにのみ適用されるため、失敗しP \/ Qます。

  4. apply P.基本的には当時のままexact P.です。

全体として、用語と型を区別して考える (一般的な) 問題を抱えているようです。目標は型であり、項を構築することによって証明しようとすることを忘れないでください。仮説はすべて の形式であるため、 or<term> : <type>を使用するときはいつでも、コロンの左側にある名前ではなく、コロンの右側にあるものが目標に一致するためです。exact <term>.apply <term>.<term>

于 2012-09-23T06:12:17.507 に答える