Personal Fabrication

音楽、勉強・読書記録、日常の感想

Coqと共に大学数学に入門する【1.簡単な導入】

 

 

私は、とある人に師事して、Coqという証明をサポートしてくれるソフト(詳しくは脚注1)を使って証明を書く能力を僅かながら身につけました。*1

 

そして、その結果、Coqと日常的なレベルの数学を上手く組み合わせることで、証明の基礎が身につけられると確信するに至りました。*2

Coqの素養を身につけることができれば、「一体どこから証明に手をつけたらいいの?」や「そもそも証明ってなに?」のような悩みのかなりの部分を解決できると思います。

サンプルは極めて少ないですが、実際の僕がそうでした。僕は、大卒後に白チャートやマセマで数学を独学した程度の実力しかなかったにも関わらず、Coqを通じて証明とは何かを理解することができました。

 

現状、Coqで検索していくつもの日本語の記事が出てきますが、一部の極めて優秀な人たちの間で使用されているだけのように思います。先に述べたように、Coqの素養は数学の素養と密接に関係があるので、非常に惜しいなと思います。

 

ただ、僕自身、Coqの素養のみでは数学をするに十分でないことを実感している最中でもあります。それはなぜかということについても、この記事を通して書きたいと思います。

先に述べておくと、僕の目標は、可能な限り厳密に松坂の『集合・位相入門』を読むことです。全てをCoqで処理しようとは考えていませんが、可能な限りCoqレベルで証明を書きたいと思っています。そして、その能力を身につけるまでの過程をここで共有できれば多くの人の数学学習の参考になると考えたので、ブログにその過程を記していこうと思います。(勉強仲間探しも兼ねています)

 

とにかく、まず初めに、Coqの威力を確かめてみましょう。スクショを連投しますが、許してください。手書きも考えましたが、経験上、一番これがわかりやすいと思います。

(間違いの指摘大歓迎です!!)

 

Coqの基本的な仕様について紹介しましょう。

左側が自分でコードを入力するところです。それに従って右上の画面が変化していきます。緑色になっているところは、その操作がCoqで認められたということです。

間違った操作をしようとすると右下にエラーメッセージが出ます。

つまり、間違った操作はCoqが認めてくれないのです。

エラー(不正な操作)があると、例えば、型(Prop(命題)とかnat(自然数)です)が違うとか、それは定義されていないとかCoqさんが優しく(だいたい厳しい)指摘してくれます。

 

かなり直感的にわかりやすくできているので、画像を見た方が早いと思います。左上にある下向きの矢印をクリックすることで証明が進んでいきます。

f:id:AAIIIOOIIIAA:20180415125809p:plain

 

Variable というtactic(命令)を使って、これは変数A B Cというものがあって、それは命題の型を持っているよと宣言しました。

型とは何かの説明は難しいのですが、説明してみます。ざっくりいうと型は、性質や構造を表します。(以下の斜体部分は細かな話なので飛ばして可)

 

性質の場合は、a:nat であれば、aはnat(自然数)の型を持っているよってことです。

構造の場合は、足し算であれば、1 + 2 = 3 とかで考えるとわかりやすいかもしれません。1 + 2 = 3、プラス(+)は、1 とか 2のような自然数をふたつ受け取って、自然数を返すような構造があるとします。それをCoq の型として書くと、nat->nat->natとなります。 1(nat)->2(nat)->3(nat)となっていて、正しい構造だとわかります。natの型を必要とするところに、間違った型を持つものをProp(命題)を入れたりするとエラーになります。

彼はペンギンである(Prop) + 2(nat)=3(nat)  みたいになってるってことです。

見ての通り意味不明です。ただ間違っても、Coqさんが優しく教えてくれるので安心してください。エラーが出る場合は、エラーを解消してからでないと下に進めない仕様です。

 

次のGoalという命令は、見たままです。これから〇〇を証明するよと宣言しています。そうすると右側にそれと全く同じものが現れたのがわかると思います。右側の線の下にあるのが、これから証明する対象(ゴール)です。

では、それを証明していきましょう。

f:id:AAIIIOOIIIAA:20180415125809p:plain

 

introという操作をしました。これは ->(ならば)の導入則にあたるものです。

P->Qを演繹する場合、Pを仮定して、Qが演繹できれば良い訳です。

Coqでも同様の操作をしています。P->Q の 矢印の左側のPを仮定に移す操作です。それが intro です。直感的には、仮定と結論を分ける操作だと考えて問題ないと思います。

では、intro してみましょう。

f:id:AAIIIOOIIIAA:20180415125818p:plain

 

A が線の上に移ったことが確認できましたね。これは、Aが仮定に移ったことを意味します。この仮定を使って証明をしましょうということです。

ただ、もうひとつ -> で繋がれたものがありますよね。これも仮定として使うために intro してあげましょう。

f:id:AAIIIOOIIIAA:20180415125822p:plain

 

大分、整理されましたね。これは証明を始めるまでの前処理のようなものです。

仮定を結論を綺麗に分けることができました。

では、仮定(道具)を使ってB(ゴール)を証明してみましょう!

ゴール(画面右側の線より下)にはBがあり、

仮定(画面右側の線より上)には A とA -> Bがあります。

A->B と A があれば、Bを演繹できるというのが ->(ならば)の除去則です。

 

Coq上でそれに似た操作は、apply です。

では、apply してみましょう。(画像では apply H0 )

H0 という名前の仮定をゴールに適用するよってことです。

f:id:AAIIIOOIIIAA:20180415125824p:plain

残念ながら証明はまだ終わりません。

なぜなら、A->B という仮定をapplyするとは言いましたが、A->B から Bを証明するには、Aが必要だからです。簡単に言えば、A->B はAが“成り立つならば” Bと言っているだけで、Aが成り立つとまでは言っていないからです。

したがって、Aを証明する必要が出てきます。

では、改めて仮定を見てみましょう。

A がありますね(なんという幸運!)

 

では、Coqにゴールと全く同じ仮定があるよということを伝えるassumption と指示してあげましょう。

 

f:id:AAIIIOOIIIAA:20180415125828p:plain

 

No more subgoals !!

おめでとうございます。これは証明が終わったことを意味します。

証明が終わったので気分的に Qed と書いておきましょう。正式に証明完了です。

 

これはCoqの使い方の一例に過ぎませんが、Coqの威力がわかっていただけたのではないでしょうか。このようにして、機械的に一つ一つの操作を適用していくだけで厳密な証明をすることができるのです。ほぼ思考停止で、その時点で可能な操作を機械的に適用するだけで対偶を証明したりすることも可能です。式に置き換えることさえできてしまえば、正確かつ比較的簡単に様々なことが証明ができるようになります。(もちろん、全てがそれほどまでに簡単な証明ではないと思います)

 

また、独学で厳密に数学書を読むためには、Coqのサポートが不可欠だと感じています。自分の証明の正しさを自分で確認できないからです。なので、可能な限りCoqで、それが難しいとしてもCoqのシステムに従って紙の上で証明を書くことで、証明の正しさを担保することが必要です。さもなければ、自分の証明の正しさを自分で検証できません。先ほど少し紹介した証明の例であれば、仮定にA->B しかないのに、Bを演繹してしまうような誤った操作をしてしまう可能性があります。悪気はなかったとしても、そういうことは多々あります。

 

他にも、仮にCoqで証明の基礎(曖昧ですが)を身につければ、数学(主に大学数学の証明)で挫折する人も減るのではないかと考えています。許された手続きに習熟することで、いちいち練習問題の解答を見る必要がなくなるからです。Coqによる証明は、数学書に書かれている証明より遥かに厳密です。

 

一つ例を紹介しましょう。

集合・位相入門(松坂)について質問ですp17の集合のドモルガンの法則の証... - Yahoo!知恵袋

mat********さん2016/5/1914:54:34

集合・位相入門(松坂)について質問です

p17の集合のドモルガンの法則の証明についてなのですが

x∉A∪B⇔x∉A,x∉B

という同値変形があったのですがどうしてこうなるのかわからないので教えてください

 

 確かに、松坂の『集合・位相入門』には、この証明が書いてあります。

この質問者さんは、この変形がわからないと言っています。なぜかというと、論理的に飛躍があるからだと思います。許された論理規則に則って変形すれば可能です。しかし、どのような規則があるかを理解していない人にとって証明は不可能だと思います。できたとして、それが正しいかどうかわからないはずです。

僕はこの変形こそがドモルガンの法則の本質だと思います。「x∉A∪B⇔x∉A,x∉B 」を証明してくださいと言われて、自分の証明の正しさを確信しつつ、その証明を書けるでしょうか。なぜ、\/ の否定が /\になるのでしょうか? (そもそも、x∉A,x∉Bが何を意味するか不明瞭です。/\のことだと思いますが)

この問題も、Coqがあれば解決できます。今は意味がわからないと思うので飛ばしてください。

( No more subgoals なので、証明はOKです!)同値なので、左から右と、右から左を証明しました。

f:id:AAIIIOOIIIAA:20180415152015p:plain

このように、Coqを使えば、数学書のギャップを埋めた厳密な証明ができます。この手順で実際に証明をするとわかりますが、理解した感が違います。Coqで認められた操作のみを用いて証明している訳ですから、基本的に間違いは起こりません。

Coqの証明の正しさは、アカデミアでも認められています。四色定理 - Wikipedia

 

ただ最も大きな問題は、Coqは証明をスタートするにあたって必要な仮定とゴールを明確にする必要があることです。(Coq無しでの数学でもそうかもしれませんが)つまり、数学書に書かれた内容の論理式に変換する作業です。変換さえ終わらせてしまえば、先ほどのようにほとんどは機械的な操作の連続で証明を終わらせることができるのですが、それが本当に大変です。脅したいわけではないですが、一例を紹介します。

A×Bの直積集合がその部分集合Gを含んでいて、任意のAの元aに関して[(x,y)G]を満たすようなBの元yがただ一つ存在する。

写像のことです。厳密に書くと、何とも物騒な式になります。

 

G⊂A×B /\ ∀x ∈A ∃y∈B[(x,y)∈G /\ ∀y’∈B(x,y')∈G -> y=y']

最初に「ただ一つ存在する」を厳密に書いた式を見たとき、物々しさに若干退いたと同時に「直観的には自明なことでも厳密に表現して取り扱うのは大変なんだ」と感じました。

 このような式を仮定やゴールに書くことができなければ、証明のスタートラインにすら立てないのです。逆に書けてさえしまえば、そんなに難しくないことが大半です。式が書けているのに、全く手が動かないということもないです。

 

ただ、悲しいことに、僕の観測範囲内では、厳密な写像の論理式が書いてある集合位相の入門書は一冊しかありませんでした。

基幹講座 数学 集合・論理と位相

基幹講座 数学 集合・論理と位相

 

 

とにかく、数学書に書かれていない部分を上手く読み取り、論理式として表現する力が必要なのだと思います。しかし、その能力を獲得する適切な方法は、今の僕にはわかりません。

ただ、その能力を獲得できたのであれば、練習問題の解答をほとんど見ることなく(もはや解答が参考にならないかもしれない)、数学書の論理的ギャップを埋めながら厳密に数学書を読む力が付くと思います。それは非常に大きな価値のあることだと思います。

実際、松坂本の写像の分野などに関しては自分で証明を書きましたが、自分の証明が正しいことを自分で確信しています。勿論、解答を見るまでもありませんでした。

 

今後、さらに自分の手で色々な証明をできるような力を獲得するためにもがいてみようと思います。正確に論理式として表現する能力を獲得するためには、まず、Coqについてもっと知る必要があると考えたので、この本を読むことにしました。

Coq’Art という本です。英語の本ですが、試読した限り、そんなに難しい単語も出てこないので大丈夫だと思います。(試読できます)

Interactive Theorem Proving and Program Development: Coq’Art: The Calculus of Inductive Constructions (Texts in Theoretical Computer Science. An EATCS Series)

Interactive Theorem Proving and Program Development: Coq’Art: The Calculus of Inductive Constructions (Texts in Theoretical Computer Science. An EATCS Series)

 

 

この正しい道である保証はないですが、正しくなかったとして、この道が正しくないことが記録として残り、誰かの参考になれば良いと思います。 僕の数学力は、一般的なレベルから見てもかなり低いと思います。ただ、低いからこそ丁寧に書けることもあると思います。少しずつ、このブログで共有できれば良いと思っています。

 

もし、このようなことに興味のある人がいれば、是非気軽に僕に連絡をください。

質問も大歓迎です。言うまでもないことですが、お金を取ったりしないので安心してください。むしろ、近場であれば、ランチでもご馳走させてください。

大阪or京都であれば、定期的に直接会って勉強しましょう。もし直接は嫌or遠方の方であれば、スカイプなどを使って上手く連絡を取り合って勉強しませんか?

Twitter からDMください。(誰でもDM可です)

https://twitter.com/nmurajshi

Twitterがわからないということであれば、捨てアドでブログにコメントしてくだされば、そこに僕のメールアドレスを送ります。

 

僕の実力ですが、Coq上での命題論理と述語論理を使った証明の基本は身についているくらいと思ってください。そこについては教えられますが、それ以上のことは、これから学んでいこうという感じです。

 

*1:Coqのようなソフトは日本語では、定理証明支援系とも言われます。「結局どんな感じなの?」というのは、 Coqを使った実際の証明を、この記事で紹介するので、それを見ると雰囲気はわかると思います

*2:Coqは数学そのものなのですがあえてそう書きました