こんな日記にもたまにブックマークを付けてくださる方がいらっしゃて有り難い事です。しかし自分が理解した順番に書いてるだけなので、話題が前に後ろに飛びまくって読みづらくて申し訳ない。いつかそのうちちゃんと分かりやすい順番にまとめたいと思っていますので、生暖かく見守り下さい。
さて、今回自分で定理を作ってみます。今回作る定理は「又」です。「True [又] False」のように使います。いわゆる or の事です。今回の目的は、forall と Implicit Arguments の性質に慣れる事です。Implicit Arguments は便利ですが、慣れないと凶悪に難しいです。逆に、これに慣れて forall が単なる関数型と同じように見えてくると断然心が軽くなります。
あと余談ですが、日本語でプログラムを書くのって意外と良いですね。漢字、ひらがな、アルファベットと文字が混ざるとアクセントになって読みやすいです。
Coq < Axiom 又 : Prop -> Prop -> Prop. 又 is assumed
まず「又」という関数を定義します。Axiom や Parameter は新しい名前を宣言する時に使います。宣言とは、このように、型だけがあって実装が無いもので、普通の言語でコンストラクタと言うのと同じです。「又」はふたつの Prop をうけとり Prop を返すので、「又 True False」のように使います。
Coq < Notation "A [又] B" := (又 A B) (at level 85).
かっこよく書けるように「又」を中値演算子にします。中値演算子にするには、一つ以上の記号を含めないと行けないので、[又] にしてみました。
Coq < Axiom 又の左 : (forall A B : Prop, A -> A [又] B). 又の左 is assumed Coq < Axiom 又の右 : (forall A B : Prop, B -> A [又] B). 又の右 is assumed
二つの定理を宣言しました。「又の左」の型は、「A が真ならば A [又] B も真である。」という意味になります。forall 文は「すべての何とかは〜」を表現するのに使う文ですが、同時に関数型でもあります。例えば、以下の三つは同じ意味です。
- A -> B -> C
- forall (a:A) (b:B), C
- forall a:A, forall b:B, C
forall 形式を使うと、二つ目の引数の型を最初の引数で指定するような事が出来ます。上の例 (又の左 : forall A B : Prop, A -> A [又] B) は Haskell 風の表記をすると Prop -> Prop -> A -> A [又] B という三引数の関数型で、引き数と返り値と意味は次のようになります。
- 引数1: 左側の仮定(A)
- 引数2: 右側の仮定(B)
- 引数3: Aの証明(実装)
- 返り値: A [又] B の証明
こんな風に使います。三番目の引き数は、左側の仮定の証明になるような名前ですが、例えば True なら I という証明が最初から宣言されているので、次のようにして True [又] False を証明出来ます。
Coq < Check 又の左 True False I (* 引き数として、「True, False, True の証明」を与える。*).
又の左 True False I
: True[又]False準備はこのへんで、今度は証明モードで (False [又] True) [又] False を証明してみましょう。
Coq < Theorem T : ((False [又] True) [又] False).
1 subgoal
============================
(False[又]True)[又]False
T < apply 又の左 (* 左側が証明出来そうなので「又の左」を apply します。*).
1 subgoal
============================
False[又]True
T < apply 又の右 (* どう見ても右側が証明出来るので「又の右」を apply します。*).
1 subgoal
============================
True
T < apply I (* True に組み込みの証明 I を使います。*).
Proof completed.
T < Qed.
apply 又の左.
apply 又の右.
apply I.
T is defined
Coq < Print T.
T = 又の左 (False[又]True) False (又の右 False True I)
: (False[又]True)[又]False最後に Print で出した「又の左 (False[又]True) False (又の右 False True I)」が、Coq 語で言う「証明」です。きっと慣れたら読めるようになるのだと思います。多分。。。
さて、話は少し戻りますが、「又の左 True False I」をよく見ると、最初の引き数は省略出来る事が分かります。なぜなら、I の型は True なので、最初の引き数は True 以外あり得ないからです。こういう時ジョーカー _ を使って引き数を省略すると、Coq が勝手に推論してくれます。
Coq < Check 又の左 _ False I.
又の左 True False I
: True[又]Falseまた、このような時、Implicit Arguments を使うと、そもそも最初の引き数は書かなくて良くなります。
Coq < Implicit Arguments 又の左 [A].
Coq < Check 又の左 False I.
又の左 False I
: True[又]False自分で Implicit Arguments を言うのさえ面倒な時は、Set Implicit Arguments モードにすると、宣言時に勝手に省略してくれます。Unset Implicit Arguments で元のモードに戻ります。
Coq < Set Implicit Arguments. Coq < Axiom 又の左' : (forall A B : Prop, A -> A [又] B). 又の左' is assumed Coq < Print 又の左'. *** [ 又の左' : forall A B : Prop, A -> A[又]B ] Argument A is implicit Argument scopes are [type_scope type_scope _]
さて、ここで本物の \/ の定義を見てみます。Unset Printing Notations で構文糖を無効にすると我々の「又」と比べやすいと思います。
Coq < Locate "\/".
Notation Scope
"A \/ B" := or A B : type_scope
(default interpretation)
Coq < Print or.
Inductive or (A : Prop) (B : Prop) : Prop :=
or_introl : A -> or A B | or_intror : B -> or A B
For or_introl: Argument A is implicit
For or_intror: Argument B is implicit
For or: Argument scopes are [type_scope type_scope]
For or_introl: Argument scopes are [type_scope type_scope _]
For or_intror: Argument scopes are [type_scope type_scope _]本物の \/ も大体似たような定義ですが、Inductive というのを使っている所が違います。この Inductive について勉強して行きたいと思います。
おまけ: apply の復習とうんちく
上の証明モードの最初の apply のステップを復習します。
- ゴールが (False[又]True)[又]False の時
- 又の左 : (forall A B : Prop, A -> A [又] B) を apply
- (False[又]True)[又]False が A [又] B にマッチ
- False[又]True が A にマッチ
- False が B にマッチ
- ゴールが False[又]True になる。
のように、apply コマンドは現在のゴールを -> の右辺にマッチさせて左辺と置き換えるという事をします。「X ならば Y」ではなく、「Y の為には X が必要」という考え方をするのです。これは普通の考え方と逆なのでうざいです。
だいたい証明なんて矢印を繋ぐだけなので前からでも後ろからでも良さそうなのですが、なぜそうなってるのかを自分なりに考えて、これは関数表記に引っ張られているのでは無いかと思いました。関数では、f:A->B, g:B->C のような関数の合成は g.f : A->C のように逆に書きます。後ろから証明すると証明の手順と結果出来た関数の対応が付けやすいのです。単なる思いつきなので、間違ってたらまた訂正します。
