今回はかけ算の定義と、かけ算関連の証明です。最初に目的としていた、
(3 + 4) ✕ 5 = (3 ✕ 5) + (4 ✕ 5)
の証明が最後になされています(※１)。
開始時の.agdaファイルと、終了時の.agdaファイルはこれ（https://polymony.net/agdathird/）になります。
動画の中にも出てきた、証明の方針（攻略法）について気づいたことですが、大事だと思うのでここにも書いておきます。
１．対象となる変数（x, y, zとか）について場合分けをする。場合分けの対象となる変数を選ぶには、succが消えるようなものを選ぶ。選ぶ際には、足し算とか、かけ算の定義の、succの部分とにらめっこする。
２．数学的帰納法（証明したい定理自身の流用）を検討する。succが入っている場合には使えない（なので、１．をよくよく検討する）。
３．足し算、かけ算などの演算から予め予想される定理(0*, *0, 1*, *1, comm, assoc, など)をまず証明しておく。
Agdaの足し算、かけ算に関する一連の証明編はこれで一旦終了です。興味のある人は、自然数に関する定理的なものを自分で探してきて証明してみるとか、Bool（真(true)、偽(false)）について、自然数と同様に定義して、いろいろ証明して遊んでみると、Agdaのやり方が身につくと思います。学生さんであれば、夏休み等の長期連休の自由研究にも使えたりするかも知れません。下の画像が一例ですが、ド・モルガンの定理とかって中学か高校の数学で出てきた気がします。学校の数学ネタに絡ませることができそうです。
次は、ソート(並び替え)関連の証明を対象にします。つまり、リストの定義から入ろうと思っています。リストを対象にすれば、Haskellでお馴染みの高階関数（map, foldとか）が出てくるので、関数型プログラミング的にも面白いネタになると期待しています。
Haskellに慣れていない人向けにも、これらの関数が何を表しているかも含めてご説明する予定です。実は、Excelのシートで簡単に再現することができます。
さらに、Agdaは依存型、正確にはType dependent on Termを扱うことが出来ます。リストと関連する一例としては、長さがn（このnがTerm）のリスト（これがType）、に関する証明とか出来るわけです。その辺りもうまく使っていきたいです。たとえば、並び替え前と後で要素の数が変わらない、とか証明できます。
では、次回もよろしくお願いします。
（※１）動画を見ていただくとわかったかも知れませんが、人力で証明するとなると結構きついです。Agdaは証明支援系言語というカテゴリーにありますが、支援と言っても、式を簡約するとかこれはおかしいですよとか、そういうのを教えてはくれますが、自動でAgdaが証明してくれる、みたいなところまでは到達していません（一応、, a (emacsならCtrl a)というコマンド(auto)は存在しますが、そんなに賢くはない印象です）。場合分けを幾つか繰り返していくと、可能性が発散していきます。例えばxで場合分け、yで場合分け、前に出てきたこの定理でrewrite、みたいなのを全パターン網羅するとなると、その時点で採れる作戦数をnとするとn * n * n * .. という具合に発散していきます。プログラムで自動化する場合はこの辺りを何とかする必要があります。
解消するアプローチは少なくとも２つあると思っています。
１．機械学習アプローチ
Googleの所謂A.I.が囲碁の達人に勝ったなどのニュースが数年前にありましたね。証明も囲碁のような作戦を立てながら進める行為に似ています。同じく証明支援系にカテゴリーされるCoqではTactic（戦略）という概念があるらしいです。この、機械学習技術を証明にも応用したら、というのがひとつの方法論だと思っています（※２）。
２．量子コンピューティング
２つめは量子コンピュータです。これは、応用先としてNP問題を解くことができるという面が強調されますが、上の戦略の組み合わせ爆発はまさにNP問題です。
（※２）
先日、Proof Summit2019(https://proof-summit.connpass.com/)というイベントに参加してきました。今年はAgdaについての話はなかったですが、その中でYutaka Nagashimaさんという方が、機械学習技術を定理照明系に応用する、という発表をされていました(https://github.com/data61/PSL/blob/master/slide/2019_ps.pdf)。AITP(Conference on Artificial Intelligence and Theorem Proving)というイベントもあるそうです。要チェックですね。このProof Summitというイベント、本当に楽しかったです。周りにこれ系のことをやっている人が居ないので本当に刺激になりました。Idrisという言語も前から存在は知っていたのですが、このイベントでの発表を聴き早速テキストを買いました。Agdaよりも実用プログラム向けらしいです。テキストを見ながらAgdaで実装してみようと思っています。
次回のそれ系の大型イベントはHaskell Day2019(https://techplay.jp/event/727059)というのがあります。こちらも楽しみです。HPを見ると分かりますが、Haskell界隈の著名な方たちが発表予定されています。アイドルとか全然興味がないタイプなのですが、こういう感覚かｗと新鮮な感じです。