Coq上での命題論理 (PropLogic.v)

このファイルは、命題論理の体系を定義している部分と、そのあとの演習問題から構成される。(それらの間に Exercises というコメントが書いてある。) 体系の定義部分は一切変更しないでほしい。演習部分に直接証明を書きこんで、Coqシステムのチェックを通るまで何度でも試してほしい。
証明のしかた
何はともあれ、Theorem ex01 という行にカーソルを進めてほしい。そこまでいってから、C-c C-return と打つと、Coqシステムがその行までの定義や証明を処理してくれる。処理済みの部分は色が変わる。
そして、 Theorem ex01...という行まで色が変わったら、 emacsのウィンドウが2つになり、PropLogic.v というファイルを見ている部分と、*goals* という名称のバッファとになる。この*goals* には「現在、まだ証明されていない(あなたが証明すべき)もの」が列挙されている。最初の時点では、証明すべきものは、1つだけであり、それを意味する「1 subgoals」という表示がでているはずである。
```
1 subgoals, subgoal 1 (ID 85)

  ============================
   [P] |- P
```
ここで === の下が、証明すべきもので、この場合、講義資料の P |- P を意味している。(|-の左辺は列なので、実装の都合上、リストをあらわす [...]で囲うことにした。)
つまり、現在は、P |- P を証明すべきだということである。
そこで、証明を構成する。証明は「下から上へ」作っていく。この証明は assume 命令を使えば一発で解けてしまうので、 PropLogic.v の Theorem ex01... Proof. のあとに assume. と入力する。 (というか、これは既に入力してある。) そこで、この assume. の行を実行するため、C-c C-n とタイプする。一回タイプすると、Proof. の行が実行され、もう一回タイプすると、 assume. が実行される。その瞬間に、*goals*バッファに変化がおこり、上記のゴールが消えて、
```
No more subgoals.

(dependent evars:)
```
という表示に変更される。(バッファ名も *response* になるが、その辺は気にしなくてよい。) これで、証明は終わりである。
ただし、若干面倒くさいのだが、証明が終わったことを意味する。 Qed.という命令も実行しないといけない。そこで、C-c C-n をもう一回タイプする。今度は、
```
ex01 is defined
```
という表示になり、定理ex01が証明されたことがわかる。(証明が終了したのに defined と表示されるとは一体どういうことだ、と思う人がいるかもしれないが、ここでは、こんなものだとおもってほしい。)
あとは同様に証明していけばよいのだが、証明が書いてあるのは ex03 までで、ex04以降は、証明のところが Admitted となっている。これは、「証明せずにとりあえず認めてくれ」という意味であり、つまり、証明できていないことを意味する。この Admitted.という部分を消して、きちんとした証明に置きかえる、というのが、演習問題である。
PropLogic.v では、論理式等を以下のように、ASCII文字で表現する。日本語(全角)文字は一切使わないことに注意せよ。
- False ...「矛盾」を意味する論理式
- P,Q,Rなど ...原子命題(基本命題)
- A /\ B ... 「かつ」 (/\ の部分は2文字であることに注意。全角文字の「∧」ではない。)
- A \/ B ...「または」 (\/ の部分は2文字であることに注意。全角文字の「∨」ではない。)
- A -> B ...「ならば」 (-> の部分は2文字であることに注意。全角文字の「→」や「⊃」ではない。)
- ~A ...「でない」 (全角文字の「￢」ではない。)
- A,B,C |- D ...判断をあらわす (|- の部分は2文字であることに注意。全角文字の「├」ではない。)
具体的な方の証明の詳細は演習初回に説明するとして、ここでは、証明を作るにあたって、使える規則を列挙しておく。これらは、すべて、命題論理の規則(講義資料にあるもの)に対応している。
- assume.
- impI. ⊃I規則(->I規則)のこと
- impE (A). ⊃E規則(->E規則)のこと、ただし、A->B のAの部分は一意的に決まらないので、ユーザが指定しないといけない。
- andI. /\I規則のこと
- andEL (B). /\EL規則のこと、A/\B のBの部分は一意的に決まらないので、ユーザが指定しないといけない。
- andER (A). /\ER規則のこと、A/\B のA の部分は一意的に決まらないので、ユーザが指定しないといけない。
- orIL. \/IL規則のこと
- orIR. \/IR規則のこと
- orE (A) (B). \/E規則のこと、A\/B のAとB の部分は一意的に決まらないので、ユーザが指定しないといけない。
- notI. ￢I規則のこと
- notE (A). ￢E規則のこと、￢A の A の部分は一意的に決まらないので、ユーザが指定しないといけない。
- falseE. ⊥E規則のこと
- notnotE. ￢￢E規則のこと
impEなど、いくつかの規則は (A) などの形の引数を1つか2つ取ることに注意せよ。この場合、実装上の理由により、 impE (A) というように、論理式の一番外に括弧を書く必要があることに注意せよ。 (もし impE A と書いてしまうと、不思議なエラーメッセージが出る。) また、orE (A) (B) を orE (A,B) などと書いてもいけない。

Yukiyoshi Kameyama