Proof-editing mode であそぼう

プログラミング Coq、2章に突入です。楽しみにしてもらえていたでしょうか?

前回予告した通り、今回は proof-editing mode を使って証明をしてみます。新しい概念が登場して覚えることも多くなりますが、一つずつ確認しながら進んで行けば大丈夫です。

今回もまだプログラムは仮想的に定義されているとして、そのプログラムの性質の証明、つまり、基本的な論理学の命題の証明をします。少し数学よりですが、基本は大事ですので、頑張って証明していきましょう。なお、次回はリストを扱います。

proof-editing mode での証明

1章の最後でこんな型を考えましたね。

forall (P Q : Prop), (forall P : Prop, ((P -> Q) -> Q)) -> ((P -> Q) -> P) -> P

これをみたす関数を作るのはちょっと面倒、という話でした。本格的にプログラムの性質を証明していくとなると、型がこれよりもっと複雑な形になり、自分の頭で関数を考えていくのは現実的ではありません。そこで proof-editing mode の登場です。

証明してみる(1)

それでは、簡単のため1章で出した命題0を proof-editing mode を用いてもう一度証明してみましょう。命題0は、型で表すとこうでしたね。

forall (A : Prop), A -> A

早速 proof-editing mode に入ってみましょう。proof-editing mode に入るには、CoqIDE に次のようなプログラムを書いてください。

Definition prop0 : forall (A : Prop), A -> A.

前回使ったファイルの続きに書く場合は名前が衝突してしまうので prop0 を別の適当な名前に置き換えてください。

前回の prop0 の定義と比較してみましょう。前回はこのように書きました。

Definition prop0 : forall (A : Prop), A -> A :=
  fun A x => x.

書いたプログラムについて説明します。関数名の後に型が来ていますが、前回の prop0 のときと違うのは型の後に ":=" でなく、すぐ "." が来ているところですね。

このように、型のあとに定義を書かずに "." を書くことによって proof-editing mode に入ることができます。

それでは今書いたプログラムを CoqIDE に読み込ませてください。これまで何も表示されていなかった右上の枠に変化が見られます。このように表示されたでしょうか。

1 subgoal                                          (サブゴールが1つある)

______________________________________(1/1)        (サブゴールが1つあるうちの1つ目を表示)
forall A : Prop, A -> A                            (サブゴール(現在の結論))

proof-editing mode に入ることができました。このチュートリアルではこの図を「証明図」と呼ぶことにします。ではまず証明図の見方を説明します。

"___________(1/1)" の下に命題1の型が書かれていますね。"___________(1/1)" の下はサブゴール(subgoal)と呼ばれ、証明における現在の結論(示したいこと)を表示します。1行目の "1 subgoal" は「サブゴールが1つある」という意味で、"___________(1/1)" の "1/1" は「サブゴールが1個あるうちの1個目を表示している」ということを意味します。示したいことが2つ出てくると "1/2" と表示されます。

証明を始めてみましょう。まず、"Definition 〜 ." と書いた次の行に

Proof.

と書いて読み込ませてください。これだけでは何も変わりませんが、Proof は証明を始めることを明示的にします。面倒だと思えば、書かなくても何も問題ありません。

proof-editing mode に入ると、新しくタクティク(tactic) と呼ばれるコマンドが使用できるようになります。タクティクを使うと、小さい証明をつなげて最終的に示したかったことの証明が作れます。そこで、まず "intros" というタクティクを使ってみます。

次の行に

intros.

と書き、同じように読み込ませてください。このような変化が見られましたね。

1 subgoal
A : Prop
H : A
______________________________________(1/1)
A

"___________(1/1)" の上に新しい文字列が並び、サブゴールが A だけになりました。"___________(1/1)" の下は結論を表示すると前述しましたが、逆に "___________(1/1)" の上は仮定(分かっていること)を表示します。

"A : Prop" は A の型が Prop であること、"H : A" は H の型が A であることを表します。

H という新しい変数が現れましたが、では intros は一体どのようなはたらきをしたのでしょうか。

Coq からは離れて「任意の命題 A に対して A ならば A」はどのように証明すればよいのか考えてみます。まず「任意の命題 A に対して」なので、任意に命題を取ってきてそれを A とします。名前は A でなくても構いません。

次に「A ならば A」ですが、これはどうでしょう。一般に「P ならば Q」を証明したいときには、P が成り立つことを仮定したとき Q が成り立つことを示します。具体的に、自然数 n があるとき P を「n が偶数」、Q を「n + n は偶数」とすれば、「P ならば Q」は「n が偶数ならば n + n は偶数」となります。これを証明したいのなら、n が偶数であることを仮定して n + n も偶数であることを示せば良いですね。

そして「A ならば A」の証明は、同じように A が成り立つことを仮定して A を証明すれば良いです。ここで、今分かっていること(仮定)を確認すると、

• A は命題である
• A が成り立つ

の二つです。CoqIDE の画面に戻って "___________(1/1)" の上にある仮定をみてみると、今確認した仮定と似ていることが分かります。"A : Prop" は「A は命題である」に対応し、"H : A" は「A が成り立つ」に対応します。H は何かというと、「A が成り立つ」という仮定に Coq が適当につけた名前です。

1 subgoal
A : Prop                                        (A は命題である)
H : A                                           (A が成り立つ)
______________________________________(1/1)
A

こう考えると、intros のはたらきが分かってきたでしょうか。intros は現在のサブゴールに対して、サブゴールが "forall A, B" なら仮定に A を入れてサブゴールを B に、サブゴールが "A -> B" なら仮定に "H : A" を入れてサブゴールを B に変えるはたらきをします。

証明が 1 ステップ進みました。次はどうするのかというと、H (A が成り立つ)ということが分かっていて、示したいこともまた「A が成り立つ」ということなのですから、H をそのままサブゴールに適用してやればそれで証明終了です。

H をサブゴールに適用するには "apply" というタクティクを使います。intros. の下の行に

apply H.

と書いて CoqIDE に読み込ませてください。すると、証明図のあったところに

Proof completed.

と表示されました。これで証明終了です。最後に証明終了のしるしとして "Qed." と書いて読み込ませましょう。右下の枠に

intros.
apply H.

prop0 is defined

と表示されたら、prop0 が問題なく定義された証です。「定義された」ということは前回書いたように「証明された」ということと同じです。proof-editing mode を使っての証明が見事できました。

"Qed." を読み込むと、proof-editing mode を抜け、Coq はそれまで使われたタクティクを見て prop0 という関数を自動で定義します。既にある関数の定義を見るためには、Command Pane を開いて、中にある左のテキストボックスに

Print

、右のテキストボックスに

prop0 (* 定義を見たい関数の名前 *)

と書いて Ok ボタンを選択してください。このような結果になりましたか?

Result for command Print prop0.:
prop0 = fun (A : Prop)(H : A) => H
   :forall A : Prop, A -> A

"prop0 = " の後は関数 prop0 の定義です。次の行の ":forall A : Prop, A -> A" は prop0 の型が "forall A : Prop, A -> A" であることを表しています。前回定義した prop0 と同じですね。

Definition 以外のコマンド

"Definition"(定義)の代わりに以下のようなコマンドでも同じように使って proof-editing mode に入って証明できます。

沢山ありますが、私は重要な命題には Theorem、他の命題を証明するために使う補助的な定理には Lemma、と使い分けています。Definition、Remark、Fact、Corollary、Proposition は私はあまり使っていません。

Theorem や Lemma などは以下のように使います。

Theorem prop0 : forall (A : Prop), A -> A.
Lemma prop0 : forall (A : Prop), A -> A.

Theorem や Lemma などは proof-editing mode に入って証明を始めるためのコマンドで、 関数を定義する形、つまり "Theorem func : T := X." のようには書けません。関数定義にも使える Definition 以外のコマンドに、Example があります。Example は Definition と同じように、次の二通りの使い方ができます。

Example prop0 : forall (A : Prop), A -> A.
Example prop0 : forall (A : Prop), A -> A := fun A x => x.

また、名前を付けるまでもない命題を証明したいときのために Goal というコマンドがあります。Goal は次のように使います。

Goal forall (A : Prop), A -> A.

Goal の後には関数名を書かず、すぐ型が続いていますが、これでも proof-editing mode に入って証明ができるようになります。

証明してみる(2)

それでは、1 章の最後に挙げた

forall (P Q : Prop), (forall P : Prop, (P -> Q) -> Q) -> ((P -> Q) -> P) ->  P

を proof-editing mode の中で証明してみましょう。今度は Goal を使って、

Goal forall (P Q : Prop), (forall P : Prop, (P -> Q) -> Q) -> ((P -> Q) -> P) -> P.

と書いて読み込ませます。証明図

1 subgoal

______________________________________(1/1)
forall P Q : Prop, (forall P0 : Prop, (P0 -> Q) -> Q) -> ((P -> Q) -> P) -> P

のように変わりましたね。先程のように intros タクティクを使いましょう。

intros.

1 subgoal
P : Prop
Q : Prop
H : forall P : Prop, (P -> Q) -> Q
H0 : (P -> Q) -> P
______________________________________(1/1)
P

仮定が沢山増えました。一度に増えて何が起きたのか分からない、というときは "intros" ではなく "intro" を使うと 1 ステップずつ変形をすることができます。intro を使ってみるために一旦戻ってみましょう。プログラムを読み込ませるのに使った下向きの矢印の右にある、上向きの矢印を選択すると、読み込んだプログラムを読み込む前の状態に戻すことができます。

上向きの矢印を選択してみてください。"intros." の背景色が緑から元に戻り、証明図も最初の状態に戻りました。

"intros." の直前の行に

intro.

と書いて読み込ませてください。

1 subgoal
P : Prop
______________________________________(1/1)
forall Q : Prop, (forall P0 : Prop, (P0 -> Q) -> Q) -> ((P -> Q) -> P) -> P

1 ステップだけ変形できました。まず P だけ仮定に移動しましたね。このように intro はサブゴールが "forall P : 〜" の形なら P を仮定に移します。また、サブゴールが "A -> B" のときは A を仮定に移します。何度も "intro." を書いて読み込ませると少しずつ仮定とサブゴールが変化していくのが分かります。

では、"intro." を複数回か "intros." を使ってサブゴールを

1 subgoal
P : Prop
Q : Prop
H : forall P : Prop, (P -> Q) -> Q
H0 : (P -> Q) -> P
______________________________________(1/1)
P

に戻してください。この後はどうすれば証明ができるでしょうか?

ここで、H0 に注目してください。H0 の型は

(P -> Q) -> P

で、"->" の最後に続く型は P で、サブゴールと同じです。prop0 のとき apply というタクティクを使いましたが、今回も apply が使えます。実際に

apply H0.

を書いて読み込ませてください。

1 subgoal
P : Prop
Q : Prop
H : forall P : Prop, (P -> Q) -> Q
H0 : (P -> Q) -> P
______________________________________(1/1)
P -> Q

サブゴールが "P -> Q" に変わりました。この "P -> Q" は、H0 の "(P -> Q) -> P" の最後の " -> P" が取れて出てきたものです。

一般に、仮定に "X : A -> B" があり、サブゴールが B のとき、"apply X." はサブゴールを "A" にするはたらきを持ちます。

証明の間でなぜこんな操作をして良いのでしょうか。それは「命題は型」「証明はプログラム」という対応を思い出せば簡単です。「"A -> B" という型を持った関数 X」があるときに型 B のプログラム(値)を作りたいなら、型 A のプログラムがありさえすればそれを X に渡せば型 B のプログラムができますね。このように現在の仮定から A が導ければすぐに B も導けます。そのため A をサブゴールに持ってくるために apply を使うのです。

apply X は関数 X に何かを適用している訳ではなく、X に適用できる値の型をサブゴールに持って行くことに注意してください。紙の上の通常の証明では A が成り立つから B も成り立つ、B が成り立つから C も成り立つ、と分かっていることを順に繋げて証明を進めていきますが、Coq では普通 C が成り立つためには B が必要で、B が成り立つためには A が必要だから A を示す、と通常の証明とは逆向きに進んで行きます。

この逆向きに証明していく感覚は、初めは慣れないかもしれませんがすぐ慣れてきます。

では次に何をすれば良いでしょう。サブゴールが "P -> Q" のように -> が入った形になっているので、intro もしくは intros が使えます。もともと1 ステップしかないので、どちらでも良いので書いて読み込ませましょう。

intro.

1 subgoal
P : Prop
Q : Prop
H : forall P : Prop, (P -> Q) -> Q
H0 : (P -> Q) -> P
H1 : P
______________________________________(1/1)
Q

仮定に "H1 : P" が増え、サブゴールが Q になりました。すると今度は、H を apply できますね。しかし、この状態で "apply H." を読み込ませようとしても、このようなエラーが出ます。

Error: Unable to find an instance for the variable P.

前回の証明で "apply H0." を使ったときは H0 に "forall 〜" は付いていませんでしたが、今回 H は "forall P : Prop," と始まります。H に出てくる型変数 P は仮定にある "P : Prop" の P とは無関係で任意に取れるので、Coq は "apply H." を読み込もうとしても P が何なのか分からず困ってしまいます。そこで型変数 P に何を代入してやるかこちらで決めます。型変数 P に何を取れば上手く証明できるかは、頭の使いどころです。仮定をじっくり眺めて考えればどう取れば良いのか分かりますが、最初は難しいと思うので答えを言ってしまうと、型変数 P には "P -> Q" (この P は仮定にある "P : Prop" の P です)を代入すればこの証明は上手く行きます。

"X : forall A : 〜" の中の型変数 A に具体的な型 B を代入して apply するためには、"apply (X B)" とします。今回は

apply (H (P -> Q)).

となりますね。 読み込ませると証明図がこのように変わりますね。

1 subgoal
P : Prop
Q : Prop
H : forall P : Prop, (P -> Q) -> Q
H0 : (P -> Q) -> P
H1 : P
______________________________________(1/1)
(P -> Q) -> Q

ここまで来れば証明終了もあと一息です。H の型は "forall P : Prop, (P -> Q) ->. P" なので、H の型変数 P に今度は P (仮定にある)をそのまま与えればサブゴールと同じ形になります。また apply を使ってみましょう。

apply (H P).

この場合は型変数の P は仮定にある P だということを Coq が推論できるので "apply H." と P を省略して書くこともできます。

今書いた "apply (H P)." を読み込ませましょう。

Proof completed.

prop0 よりは複雑でしたが、証明が完了しました! "Qed." で証明終了を CoqIDE に伝えましょう。"Unnamed_thm is defined" と右下の枠に表示されたら OK です。

少し長くなったので、証明を通して書いてみます。

Goal forall (P Q : Prop), (forall P : Prop, (P -> Q) -> Q) -> ((P -> Q) -> P) -> P.
Proof.                  (* なくても良い *)
intros.                 (* 導入 *)
apply H0.               (* H0 をサブゴールに適用 *)
intro.
apply (H (P -> Q)).
apply (H P).
Qed.

今回の命題の証明は、以下のようにもできます。

Goal forall (P Q : Prop), (forall P : Prop, (P -> Q) -> Q) -> ((P -> Q) -> P) ->  P.
Proof.
intros.
apply H0.
intros.
apply (H Q).
intro.
apply H2.
Qed.

CoqIDE に読み込ませてみれば正しく証明できることが分かるでしょう。このように、一つの命題の証明は一通りとは限りません。もしこれから自分で書いた証明がチュートリアルで書かれている証明と違っても、"Qed." まで CoqIDE が読み込んでいれば正しい証明なので不安に思うことはありません。

練習問題

proof-editing mode で forall (任意の)、-> (ならば)だけが出てくる命題の証明ができるようになったので、証明問題を出します。以下の型に対応する命題を proof-editing mode に入って証明してください。

問2. forall (P Q R : Prop), (P -> Q) -> (Q -> R) -> P -> R

not、or、and の定義と証明

今まで「任意の」や「ならば」は型で表すことができましたが、命題の否定、「A でない」「A または B」「A かつ B」という命題を考えるとどうでしょう。これらを表現するには新しく型を作る必要があります。

Coq で新しく型を定義するには Inductive を使います。まずはプログラマの皆さんにより親しみがあるであろうリストを定義してみましょう。Inductive はこのように使って型を定義します。

Inductive list (A : Type) : Type :=
  | nil : list A
  | cons : A -> list A -> list A.

Inductive の後にはデータ型の名前、その後に型変数が続きます。":=" の後には定義を書き、"|" の後に型構成子、":" の後にその型を書きます。"|" で区切ることによりいくらでも型構成子が定義でき、最後には "." を入れます。また、最初の "|" は省略できます。

Haskell で書くと、

data List a = Nil | Cons a (List a)

と同じです。OCaml だと

type 'a list =
  | nil
  | cons of 'a * 'a list

です。

not

「A でない」は「A ならば矛盾する」と表せるので、「矛盾」という型が作れれば良いです。それでは「矛盾」を Inductive を使ってどう定義されるのでしょうか。リストは nil と cons x xs の二つの作り方がありますが、「矛盾」は正しい命題からの作り方はないのでこのように定義されます。

Inductive False : Prop :=.

"False" は「偽」という意味で違和感を覚えるかもしれませんが、Coq では False を矛盾としています。

さらに以下のような not という関数も用意されており、

Definition not (A : Prop) := A -> False.

list、 False や not は Coq の標準ライブラリにあるものと同じで、かつ最初からインポートされているので自分で定義しなくても使えます。

標準ライブラリにある not を使う場合、 "not P" のような形だけでなく

~P

のようにも書くことができます。

not を使ったこんな命題を証明してみましょう。

Goal forall P : Prop, P -> ~~P.

1 subgoal
______________________________________(1/1)
forall P : Prop, P -> ~ ~ P

forall と -> でできた形のサブゴールなので、何も考えずにまず intros を使ってみます。

intros.

1 subgoal
P : Prop
H : P
______________________________________(1/1)
~ ~ P

ここで、サブゴールの "~ ~ P" は "(P -> False) -> False" という型と同じですが、まだ -> が残っているのに仮定に "(P -> False)" が導入(intro)されませんでした。結論から言うと、intro タクティクを使えば導入されます。

intro.

1 subgoal
P : Prop
H : P
H0 : ~ P
______________________________________(1/1)
False

なぜ intros では導入されず intro で導入されるかというと、実は intros タクティクは単純に intro タクティクを繰り返しているわけではなく、構文を見て forall と -> があれば仮定に導入する作業をするので、"~" のように別の名前を使っている場合は導入してくれません。一方 intro は関数の定義まで見ているので、導入されます。

証明を続けましょう。仮定の H0 に注目すれば次にどうするべきか分かります。"~ P" は "P -> False" と同じで、かつ結論が False なので apply タクティクが使えます。

apply H0.

1 subgoal
P : Prop
H : P
H0 : ~ P
______________________________________(1/1)
P

この後は簡単ですね。サブゴールが H そのものですから、

apply H.

Proof completed.

Qed で証明を終わらせましょう。ここまでの証明をまとめてみます。

Goal forall (P : Prop), P -> ~~P.
intros.
intro.
apply H0.
apply H.
Qed.

intros と intro が連続して気持ち悪い、という方のために他の証明も紹介します。

Goal forall (P : Prop), P -> ~~P.

までは同じで、次に

unfold not.

と書いてください。

1 subgoal
______________________________________(1/1)
forall P : Prop, P -> (P -> False) -> False

"~" が "-> False" の形に展開(unfold)されました。unfold という新しいタクティクは、このように unfold の後に書いた名前の関数を展開します。これなら次に

intros.

とすれば

1 subgoal
P : Prop
H : P
H0 : P -> False
______________________________________(1/1)
False

と、intros 一度で -> が全て導入できます。後は先程と同じです。

or

今度は「A または B」という命題を表現する型を作ることを考えます。「または」を表す型 or は標準ライブラリでこのように定義されています。

Inductive or (A B : Prop) : Prop :=
  | or_introl : A -> or A B
  | or_intror : B -> or A B.

「A または B」という命題を作るには、命題 A か命題 B を与えてやれば良いので、このように命題 A を取る or_introl と 命題 B を取る or_intror から構成された定義になります。

data Either a b = Left a | Right b

二階論理では「A または B」を記号で「A ∨ B」と書くので、それを真似して Coq でも "or A B" と書く代わりに

A \/ B

と書くことができます。使っている環境で "\" が円記号と表示されていると分かりづらいかもしれませんが、"\" をバックスラッシュだと思うと "\/" が ∨ の形になっているのが分かります。今までのように、「または」を使った命題を証明してみようと思います。

Goal forall (P Q : Prop), P \/ Q -> Q \/ P.

1 subgoal
______________________________________(1/1)
forall P Q : Prop, P \/ Q -> Q \/ P

いつものように、まず intros を使ってみます。

intros.

1 subgoal
P : Prop
Q : Prop
H : P \/ Q
______________________________________(1/1)
Q \/ P

この形は、今までになかったケースです。ここで、仮定に "H : P \/ Q"(P または Q) があるので、今回は場合分けをして証明してみようと思います。一般に、証明の途中で仮定に "X : A \/ B" があり他に変形できそうな仮定やサブゴールがないときには X が A のときか B のときかで場合分けをすると上手く行くことが多いです。

場合分けをするには、case タクティクを使います。

case H.

2 subgoals
P : Prop
Q : Prop
H : P \/ Q
______________________________________(1/2)
P -> Q \/ P

______________________________________(2/2)
Q -> Q \/ P

サブゴールが二つに増えました。二つのサブゴールを見ると "P -> Q \/ P" と "Q -> Q \/ P" になっており、H が P の場合と Q の場合に分けて考えていると分かります。プログラムで言うと、パターンマッチをしたと思ってください。

まだサブゴールに "Q \/ P" があり、一見困ってしまいます。しかし、proof-editing mode では証明図の仮定の外にある定理も証明に使うことができます。この状況で使えそうな定理(関数)は、"or_introl : A -> A \/ B" か "or_intror : B -> A \/ B" です。今は A、B にはそれぞれ Q、P が入るので、or_intror が一つ目のサブゴールの型そのものですね。

apply or_intror.

1 subgoal
P : Prop
Q : Prop
H : P \/ Q
______________________________________(1/1)
Q -> Q \/ P

一つ目のサブゴールが消え、残り一つになりました。こちらも先程と同じように、今度は or_introl を使って

apply or_introl.

Proof completed.

少しややこしかったかもしれませんが、証明できました。

Goal forall (P Q : Prop), P \/ Q -> Q \/ P.
intros.
case H.             (* 場合分け *)
apply or_intror.
apply or_introl.
Qed.

この命題の証明にもこんな別証明があります。今は場合分けに case を使いましたが、似たタクティクに destruct があります。証明を巻き戻して、"case H." の代わりに

destruct H.

とすると

2 subgoals
P : Prop
Q : Prop
H : P
______________________________________(1/2)
Q \/ P

______________________________________(2/2)
Q \/ P

このようになりました。"destruct H" はまず case と同じはたらきをし、その後仮定にある H を消してから intro します。"case H." したときの証明図をもう一度載せて比べてみましょう。

2 subgoals
P : Prop
Q : Prop
H : P \/ Q
______________________________________(1/2)
P -> Q \/ P

______________________________________(2/2)
Q -> Q \/ P

確かに case のときの "H : P \/ Q" が、destruct のときではなくなっていて、さらに destruct のときの証明図は case のときから intro した形になっています。場合分けをしていることに変わりありません。

ではこの続きは、また "apply or_intror" していっても良いですが、冗長だと思えば別のこんなタクティクで済ますことができます。

right.

2 subgoals
P : Prop
Q : Prop
H : P
______________________________________(1/2)
P

______________________________________(2/2)
Q \/ P

right というタクティクを使いました。right タクティクは、サブゴール(型)が二つ型構成子を持っているとき、そのうち二つ目の型構成子を適用します。or の二つ目の型構成子は or_intror なので、right は "apply or_intror" と同じです。直感的にも「Q \/ P の右(right)側を取ってきた」と解釈でき分かりやすいです。

"apply H." で一つめのサブゴールを証明したら、証明図は

1 subgoal
P : Prop
Q : Prop
H : Q
______________________________________(1/1)
Q \/ P

となりますが、今度は

left.

というタクティクが使えます。right が二つ目の型構成子を適用したのに対し、left は一つ目の型構成子を適用します。left を使えば後の証明は簡単なので、各自やってみてください。

case と destruct、どうして二つも似たタクティクがあるのかと感じる方も多いかもしれませんが、この二つは上手く使い分けると意外にも証明が短くなります。慣れれば使い分けができるようになるので、最初のうちは何も考えずにどちらか好きな方を使っていて大丈夫です。私は destruct を使うことのほうが多いように思います。

and

「A かつ B」を表す型 and は次のようになっています。

Inductive and (A B : Prop) : Prop :=
  conj : A -> B -> and A B.

「A かつ B」という命題を作るには、命題 A と命題 B 両方を与えれば良いので、こうなります。

data (,) a b = (,) a b   -- (a,b)

二階論理では「A かつ B」は「A ∧ B」と記号で表すので、or のときと同じように Coq では "and A B" の代わりに

A /\ B

と書けます。

では、and を使った命題の証明をしてみましょう。

Goal forall (P Q : Prop), P /\ Q -> Q /\ P.

まずは intros です。

intros.

1 subgoal
P : Prop
Q : Prop
H : P /\ Q
______________________________________(1/1)
Q /\ P

or のとき case や destruct といったタクティクを使いましたが、今回も H に対して使えます。

destruct H.

1 subgoal
P : Prop
Q : Prop
H : P 
H0 : Q
______________________________________(1/1)
Q /\ P

「P かつ Q」に対して case(場合分け)、というのは奇妙に感じるかもしれませんが、case や destruct はパターンマッチをしていると思うと、「and の型構成子である conj の引数に具体的な値(今回は H と H0)を渡した(仮定に入れた)」と考えれば良いです。

証明に戻ると、conj(: A -> B -> A /\ B) が適用できることが分かります。

apply conj.

2 subgoals
P : Prop
Q : Prop
H : P
H0 : Q
______________________________________(1/2)
Q

______________________________________(2/2)
P

"A -> B -> A /\ B" の証明には A の証明と B の証明の二つを与えてやらなければならないので、サブゴールも二つになりました。or のとき left、right といったタクティクがありましたが、and は型構成子一つで構成されているので、left や right は使えません。しかし、型構成子が一つのときは split というタクティクが同じ役割になります。

"apply conj." の読み込みを戻して、

split.

を読み込ませてみると同じ挙動をするのが分かるでしょう。

この証明の続きは簡単なので、自分で証明してみましょう。

下に答えを書いておきます。

apply H0.
apply H.
Qed.

最後にまた証明のまとめを書きます。

Goal forall (P Q : Prop), P /\ Q -> Q /\ P.
intros.
destruct H.
split.
apply H0.
apply H.
Qed.

自動証明タクティク

今までした証明は、慣れないうちは難しく感じるかもしれませんが慣れてしまえば単純で面倒になってきます。Coq では、実は今までの命題くらいのものを自動で証明するタクティクがあります。auto や tauto です。 たとえば not の例で挙げた

Goal forall (P : Prop), P -> ~~P.

は、

auto.

と打てば自動で "Proof completed." になります。or や and のところで扱った命題は auto では証明できませんが、auto より強力な tauto を使うと一発で証明ができます。 また、

info auto (* tauto *).

と書くことによって右下の枠にどんなタクティクを使って証明をしたかが表示されます。

最初のうちは練習のために auto や tauto は使わないで証明してみることをおすすめしますが、便利なので慣れたらどんどん使って良いでしょう。

タクティクまとめ

タクティクが沢山出てきて、どういうときに何を使えば良いのかまだよく分からないでしょうから、まとめた表を書きます。

• 仮定に以下の H があるとき

• サブゴールが○○○のとき

• その他

練習問題と前回の答え

練習問題

2章のまとめとしての練習問題を出します。下の命題(型)の証明をしてみてください。auto や tauto は使わないでやってみましょう。

難しくても上の表を見ながら使えるタクティクを確認しながら証明していくと良いでしょう。

問3. forall (P : Prop), ~(P /\ ~P)
問4. forall (P Q : Prop), ~P \/ ~Q -> ~(P /\ Q)
問5. forall (P : Prop), (forall (P : Prop), ~~P -> P) -> P \/ ~P

問5は他より少し難易度が高いですが、パズル感覚で楽しく証明してみてください。

前回の答え

問0、問1の答え合わせをします。 問題は

問0. 任意の命題 A B に対して、A ならば 「A ならば B」ならば Bが成り立つ。
問1. 任意の命題 A B C に対して、「A ならば B ならば C」ならば「B ならば A ならば C」が成り立つ。

でした。問0を problem0、問1を problem1 とします。

Definition problem0 : forall (A B : Prop), A -> (A -> B) -> B :=
  fun A B x f => f x.

Definition problem1 : forall (A B C : Prop), (A -> B -> C) -> (B -> A -> C) :=
  fun A B C f b a => f a b.

1章で「見覚えのある型かもしれません」と書きましたが、Haskell でいうと problem0 は flip ($)、problem1 は flip と同じになります。