2

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

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

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

P \/ Q
~Q

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

P

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

Section Q5.

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

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

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

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

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

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

4

1 に答える 1

4

適切な解決策は1であり、あなたが期待している問題は間違っています。

あなたが書くとき：

Variable P: Prop.

あなたは、Pが住んでいる（または「Pが保持している」）とは想定していませんが、ここでは有効性が考慮されていない「ステートメント」であるPという名前の命題が存在することだけを想定しています。

これは書くこととは大きく異なります。

Variable p: P.

これは、タイプ「P」が生息しているという証明「p」があることを前提としています（PがタイプPropを持っている場合、pは命題Pの証明です）。したがって、Pは真であると想定します。

また、その理由：

Variables P.

構文エラーが発生すると、導入された変数ごとに型を指定する必要があります（型推論エンジンを導く情報がない場合、Coqはそれを魔法のように理解できません）。

したがって、スクリプトを次のように開始することはまったく問題ありません。

Section Q5.
Variables P Q : Prop.
Hypothesis premise1 : P \/ Q.
Hypothesis premise2 : ~Q.
Goal P.
于 2012-09-22T03:26:12.550 に答える