型付きλ式から証明

命題ｓ

まずは簡単な命題

1. 　　　　　 s : (A -> (B -> C)) -> (A -> B) -> (A -> C)

をCoqで証明し、（言い換えると、 型が (A -> (B -> C)) -> (A -> B) -> (A -> C) であるλ式 s を作るということです） その証明をPrint命令で表示しましょう。Coqを起動して、 以下を打ち込んでください。（打ち込む代わりに以下をクリップボードに コピーして、Coqの窓の一番上のバーを右クリックして編集-> 貼り付けを選択してもできます。）

Section ML.
Variables A B C:Prop.
Theorem s : (A -> (B -> C)) -> (A -> B) -> (A -> C).
Proof.
intros H Hab Ha.
apply H.
assumption.
apply Hab.
assumption.
Qed.
Print s.

まだSectionを閉じてはいませんが、目的は型付のλ式から証明を読み取ること なので、 s の 内容さえ把握できれば Coqは終了して結構です。（終了の仕方は、Window右上の×印をクリック してもいいですし、Quit.命令でも終了できます。）

さて、最後のPrint s.命令で、上記のように表示されていたと思います。 そのうち、λ式ｓは

2. 　　　　　 fun (H : A -> B -> C) (Hab : A -> B) (Ha : A) => H Ha (Hab Ha)

の部分で、 (A -> B -> C) -> (A -> B) -> A -> C はその型です。では、λ式Ｈ，Ｋからλ式Ｌが作られることを

のような表であらわすことにし、λ式に型もつけて上記のｓを作る様子を 表にすると、次のようになります。

ここで、Ｈ，Ｈａ，Ｈａｂは型を持った変数です。さて、 型の部分だけ取り出すと、

あるいは、変数名Ｈ，Ｈａ，Ｈａｂをラベルのようにあつかって、

のように表記することにも慣れておいてください。

いずれにしても、これは命題 s : (A -> (B -> C)) -> (A -> B) -> (A -> C) の証明になっていることがわかります。

また、λ式 Ｍ（その型は Ｂ）から、 ｆｕｎ　（ｘ：Ａ）　＝＞　Ｍ を 作ることは、推論で言うと、論理式 Ｂ から論理式 Ａ→Ｂ を作り、 仮定から論理式 Ａ を取り去る作業に対応していることがわかります。

型は命題、式は証明

ここまでくると、型の新しい解釈が理解できるようになります。すぐ上のところで「変数名Ｈ，Ｈａ，Ｈａｂをラベルのようにあつかって、」とあるように、「H : A -> B -> C」に関して、「Hは論理式A -> B -> Cの名前」程度にしか触れませんでしたが、「Hは論理式A -> B -> Cの証明」と解釈する見方があるのです。それは上記の「s : (A -> (B -> C)) -> (A -> B) -> (A -> C)」を考えればわかると思います。実際、上記のCoqにおけるPrint s.の出力を見ればわかるように、「s = fun (H : A -> B -> C) (Hab : A -> B) (Ha : A) => H Ha (Hab Ha)」は論理式「(A -> B -> C) -> (A -> B) -> A -> C」の証明と解釈することができます。

定理OrtoAnd

では、「ちょっと証明を」の定理OrtoAndを Print命令で表示したλ式 から、どのように証明を読み取るか説明しましょう。 まず、定理OrtoAndをPrint命令で表示したλ式は、 A,B,C を型がPropである 変数として、
（見やすいように、 fun (a : A) (_ : B) => H (or_introl B a) を X とおいて）

でした。ではまず、 λ式 X がどのように 構成されるか見ましょう。（以下において、 変数 a,H のみ、 その横に型を記しておきます。色が黒いのはご愛嬌。）

3. 　　　　　

   	or_introl	B
   	or_introl B		a : A
   H : A \/ B -> C	or_introl B a
   H (or_introl B a)
   fun (_ : B) => H (or_introl B a)
   fun (a : A) (_ : B) => H (or_introl B a)

さて、上記の X の 構成では、色々と説明しなくてはならないことがあります。 「λ式の構成」と 「型の付き方」を思い出しながら、 λ式 X を構成する ことを考えると、まずわからないの は or_introl だ と思います。ではこれを説明しましょう。

とは言うものの、このサイトの製作者（以下、私）もよくわかっていません。 実は、 「λ式の構成」と 「型の付き方」の方法 では、Coqにおけるλ式の定義としては足りないようなのです。 では、今までのλ式の構成に、どういった手続きを加えればいいかということですが、 よくわかりもしないのに変な説明をしていたのでは、かえって話をわかりにくく してしまいますので、いっそのこと何も説明しないことにします。 それで or_introl に ついては、「今までの方法に追加された、ある方法で作られたλ式」だと、思って ください。

では何も情報がないかというと、そういうことではありません。Print命令で、 この or_introl の 定義を見てみましょう。命令はPrint or_introl.です。

Inductiveなる命令 で or なるλ式が 定義されているようです。その定義の中 に or_introl が 現われているようです。そういう言い方をする と、or_introl の 定義は別にあるんじゃないかと思うかもしれませんが、そうではありませ ん。なぜなら、そもそもPrint or_introl.なる命令で表示されたのですから。 つまり、or_introl は、 or や or_intror と 同時に定義されているのです。

Coqの出力の1行目 Inductive or (A : Prop) (B : Prop) : Prop := を見てみましょう。最後のところに 「 := 」があります。と言うことは、 「 := 」以前のものを、 「 := 」以降のもので定義しているというわけです。 つまり、 or (A : Prop) (B : Prop) : Prop を or_introl : A -> A \/ B | or_intror : B -> A \/ B で定義しているわけです。

では、 or (A : Prop) (B : Prop) : Prop から見ていくことにしましょう。ここから読み取れるの は、or の 型です。それは、 「or なるλ式 は、引数として(A : Prop)と(B : Prop)の2つをとった上で、結果として型がPropに なる」ということです。 つまり、or の 型は ΠA:Prop.ΠB:Prop.Prop です。 「型付きλ式」での略記に 従えば Prop -> Prop -> Prop です。 （実は、or の 型を知りたいだけなら、Check or.命令だけで知ることができます。）

次に、 or_introl : A -> A \/ B | or_intror : B -> A \/ B を見ましょう。実はこれは、 | で区切られた 2つの文 or_introl : A -> A \/ B と or_intror : B -> A \/ B です。とは言っても、これで なぜ or を定義 したことになるのか全くわからないと思います。 原因の1つはnotation（表記法）です。 そこで、以前「まずはいじってみる」でも実行した 命令のUnset Printing Notations.を実行した上で、もう一度Print or_introl. を実行してみましょう。

上記2つのPrint or_introl.の後のCoqの出力を比べてみてください。実は、 「 A \/ B 」は 「 or A B 」のことなのです。Coqは表記の仕方を自由に変える ことができます。（Notation命令を使うとできるのですが、説明はいずれ。）

さて、Inductive命令で書かれた上記の定義は or (A : Prop) (B : Prop) : Prop を or_introl : A -> (or A B) と or_intror : B -> (or A B) で定義するということですが、ここで注意があります。それは 「 := 以前で書かれた引数は、 := 以降も引き継ぐ 」というものです。つまり、今回の例で言うと、 or (A : Prop) (B : Prop) : Prop における (A : Prop) (B : Prop) の部分は、 or_introl と or_intror の 方にも引き継がれるということです。それも明示して上記定義を もう一度書くと、

4. 　　　　　 or (A : Prop) (B : Prop) : Prop を
5. 　　　　　 or_introl (A : Prop) (B : Prop) : A -> (or A B) と
6. 　　　　　 or_intror (A : Prop) (B : Prop) : B -> (or A B) で定義する。

定義はさておき、上記５．から or_introl の 型を読み取りましょう。 「or_introl なるλ式 は、引数として (A : Prop) と (B : Prop) の 2つをとった上で、結果として 型が A -> (or A B) に なる」ということです。 つまり、or_introl の 型は

7. 　　　　　ΠA:Prop.ΠB:Prop.A -> (or A B)

8. 　　　　　forall A B:Prop, A -> A \/ B

9. 　　　　　forall A B:Prop, forall a:A, A \/ B

（ 「型がPropになる 変数A」なんて 言い方はまどろっこしいので、簡単に A (:Prop) と表記することにします。 ）

さて、上記７．８．９．のどれを見てもいいですが、型を見る限り、 or_introl は、 A (:Prop)、 B (:Prop)、 a (:A)の 3つを引数にとって型が A \/ B になるλ式です。例えば or_introl A B a( :A \/ B)です。 ところが、上記３． の X の構成の 図を見ると、（図の3行目に） or_introl B a と いうのがあって、明らかに型が Prop の変数 が1つ足りません （a の型は Prop では ありません）。

ここで、Print or_introl.の出力に戻って みましょう。 Print or_introl.命令の後の3行目に For or_introl: Argument A is implicit と出力されています。これは 引数 A を省略 する、という意味なのです。 or_introl A B a なる λ式においては、 or_introl の 定義からして、第3引数の a の型が 必ず第1引数 A と一致します。 よって、第1引数は第3引数から推測できるので、省略することにしよう、という わけです。そして、省略することに決めてしまった場合は、通常は省略しないと いけません。ですから実は、上記３． の X の構成の 図は不正確です。例えば次のようにしなければ なりません。（今回も、変数 a,H のみ、その横に型を記しておきます。）

10. 　　　　　

    	or_introl	A	B	a : A
    H : A \/ B -> C	or_introl B a
    H (or_introl B a)
    fun (_ : B) => H (or_introl B a)
    fun (a : A) (_ : B) => H (or_introl B a)

上記１０．の図の全てのλ式に型も表示すると、

11. 　　　　　

    	or_introl:forall A B:Prop, A -> A \/ B	A:Prop	B:Prop	a : A
    H : A \/ B -> C	or_introl B a:A \/ B
    H (or_introl B a):C
    fun (_ : B) => H (or_introl B a):B -> C
    fun (a : A) (_ : B) => H (or_introl B a):A -> B -> C

これで X の型も わかりました。 X:A -> B -> C です。

ついでにCoqの表記について。 「fun (_ : B) =>」 の「_」 （アンダーバー）が気になると思います。そこは 「fun (b : B) =>」 と書いても 「fun (y : B) =>」 と書いてもλ式としては同じ（同値）になります。つまり、 「_」 （アンダーバー）に入る文字は、それ以外の場所には現れないわけです。こういうとき は、（使用する文字の節約でしょうか）Coqでは 「_」 （アンダーバー）を表示することになっています。

それはそうと、 λ式 X は何を 証明しているのでしょうか。上記１１．の図から、型だけを取り出しましょう。 （但し、 A,B が 命題変数（Prop） であることの宣言の部分はカットします。また、 a と H は ラベルの意味を持たせて表示することにします。）

12. 　　　　　

    	A -> A \/ B	a : A
    H : A \/ B -> C	A \/ B
    C
    B -> C			_(:B)を仮定から除く
    A -> B -> C			a(:A)を仮定から除く

A -> A \/ B は 公理であり、 A は 仮定から除かれているので、上記１２．から示されているのは結局、

13. 　　　　　

    H : A \/ B -> C

    X : A -> B -> C

なる推論が成立するということです。

後は同様にして、定理OrtoAndの証明を OrtoAnd の式 から読み取ることができます。以下概略です。

まず、Print and_ind.命令。

これで、λ式 and_ind の 型は forall A B P : Prop, (A -> B -> P) -> A /\ B -> P であり、そのうち A,B,P が 引数から省略（implicit）されることがわかります。

ではOrtoAnd の λ式を構成する手順の図を作りましょう。 λ式 X の部分は 上記１３．を使用します。また、図が横に長くなって しまうので、and_ind の 型は省略します。

14. 　　　　　

    				H : A \/ B -> C
    and_ind	A:Prop	B:Prop	C:Prop	X : A -> B -> C
    and_ind X : A /\ B -> C					H0 : A /\ B
    and_ind X H0 : C
    fun (H0 : A /\ B) => and_ind X H0 : A /\ B -> C
    fun (H : A \/ B -> C) (H0 : A /\ B) => and_ind X H0 : (A \/ B -> C) -> A /\ B -> C

上記から型の部分だけを取り出しましょう。 （また、 A,B,C が 命題変数（Prop） であることの宣言の部分はカットします。さらに、ラベルにできる変数は、 図の中に残します。）

15. 　　　　　

    	H : A \/ B -> C
    (A -> B -> C) -> A /\ B -> C	A -> B -> C
    A /\ B -> C		H0 : A /\ B
    C
    A /\ B -> C			H0を仮定から除く
    (A \/ B -> C) -> A /\ B -> C			Hを仮定から除く

もし、(A -> B -> C) -> A /\ B -> C を公理として採用するなら、これで 定理OrtoAndの証明を読み取ることができました。 ただ上記の１５．は、証明に明らかな無駄があります。一度 A /\ B -> C が 証明されているのに、それをばらしてもう一度証明しています。その無駄を除くと 次のようになります。

16. 　　　　　

    	H : A \/ B -> C
    (A -> B -> C) -> A /\ B -> C	A -> B -> C
    A /\ B -> C
    (A \/ B -> C) -> A /\ B -> C		Hを仮定から除く

もどる