Coqで解析入門の1章にある命題を全て証明してみたので記事を書いてみます。
大学で記号論理学の授業を受けたことはありますか?記号論理学では数学の命題を証明木を用いて形式的証明をしていましたがCoqでも形式的証明をします。流れは以下です。
Coqでの証明の魅力は
などです。
大学1年生の頃、解析入門を前から読んで途中で理解できなくなって読み直すというのを繰り返していました。
いつか理解したいなと思っていたときに記号論理学の授業を受けて解析入門の証明も証明木を書けるようになりたいなと思いました。
でも解析入門の定理の証明木を書いても紙に収まらないだろうし書けても正しさを検証できないだろうと思って諦めていました。
5年経って修士2年生になって数学の研究をしていたのですが、自分のしていた定理の証明が正しいか気になって、当時既に知っていたCoqで証明したいなと思うようになりました。
そこで自分の研究の証明にも解析の定理は使うし、以前やりたいと思っていたのでやってみようと思いました。
Coqで解析入門の1章にある命題 • 定理 • 系を全て証明しました。ライブラリや公理は Standard Library のもののみを使いました。ソースコードは こちら に公開されています。
定理の主張は以下です。
有界実数列は常に収束する部分列を持つ。
ボルツァーノ • ワイヤストラスです。証明の概要は以下です。
これの難しかったところはただでさえ証明が複雑なのに以下の2つが初めてでてきたことです。
再帰を用いた関数の定義は例えば階乗だと
(fix fact (n : nat) : nat :=
match n with
| 0%nat => 1%nat
| S n0 => (S n0) * (fact n0)%nat
end)
このように書けます。これだけだと難しくないのですが閉区間の型をどう定義するか分からないので閉区間の列の再帰的な定義が大変でした。色々調べているとCoqには
exist A (Tの要素t) (A tが成立する証明)
とすると作ることができます。つまり(
exist A t H1 = exist A t H2
を示すことができません。そこで Coq.Logic.ProofIrrelevance の
Axiom proof_irrelevance : forall (P:Prop) (p1 p2:P), p1 = p2.
を使いました。同じ命題の証明は全て等しいという公理です。ここまで分かると定理を証明するのは流れ作業でできましたがそれまでが大変で挫折しかけました。
定理の主張は以下です。
, を実数(複素数)列とする。 , が , に絶対収束するとき
実数(複素数)列を と定義すると は に絶対収束する。
証明の本質部分は
が
を示せないといけません。これは並び替えるだけなので教科書では明らかとされていますがCoqではきちんと証明しないといけません。
です。この2つは並び替えているだけなので等しいことは分かりますが、一般の
そこで「並び替えているだけなので等しい」をCoqで一般化して作りそれを使おうと思いました。作ったものは
こちら
です。
ここで作ったもののイメージは
を定義しました。これを定義するには
などです。これらを使うと示すことができました。
定理の主張(のうち証明が難しかったの)は以下です。
の集合 に対して が有界閉集合ならコンパクトである。
証明の概略は以下です。
これは定理3.4がパワーアップした感じです。2で
始める前はどこかで作業量が多くなりすぎて挫折するかもしれないと思っていました。しかし§6に入ると少なくとも1章まではなんとかなるだろうと思うようになりました。
終わってみると24336行の728kbのソースコードができあがりました。教科書の証明よりは形式的証明は長くなってしまいますが労力は高々数倍なのかなと思いました。
数学の証明をCoqで検証するのはライブラリが充実していてそれが検索可能な状態になっていたら実用的なのかなと思いました。
教科書の証明をCoqに翻訳したものを公開するのはその状態を作ることにつながると思うので、時間があるときに引き続きやっていきたいと思います。
自分の修士の研究の証明をするためには基礎的な線形代数が必要なのでまずはそれをやります。解析入門の2章は微分なのですが微分にも行列が出てくるので線形代数が必要になります。