Coq/SSReflect/MathCompで解析入門の1章の命題を全て証明

はじめに

Coqで解析入門の1章にある命題を全て証明してみたので記事を書いてみます。

Coqでの証明

大学で記号論理学の授業を受けたことはありますか？記号論理学では数学の命題を証明木を用いて形式的証明をしていましたがCoqでも形式的証明をします。流れは以下です。

• 数学の命題を論理記号で書きます
• ゴールが表示されるので適切にCoqのTacticを使います
• するとゴールが変わるので未証明のゴールがなくなるまで繰り返しTacticを使います

Coqでの証明の魅力は

• 証明が正しいことをCoqが保証してくれること(Coqにバグがあるかもしれませんが多分)
• 証明した定理が他の定理の証明に使えて楽しいところ

などです。

やろうと思った背景

大学1年生の頃、解析入門を前から読んで途中で理解できなくなって読み直すというのを繰り返していました。

いつか理解したいなと思っていたときに記号論理学の授業を受けて解析入門の証明も証明木を書けるようになりたいなと思いました。

でも解析入門の定理の証明木を書いても紙に収まらないだろうし書けても正しさを検証できないだろうと思って諦めていました。

5年経って修士2年生になって数学の研究をしていたのですが、自分のしていた定理の証明が正しいか気になって、当時既に知っていたCoqで証明したいなと思うようになりました。

そこで自分の研究の証明にも解析の定理は使うし、以前やりたいと思っていたのでやってみようと思いました。

やったこと

Coqで解析入門の1章にある命題 • 定理 • 系を全て証明しました。ライブラリや公理は Standard Library のもののみを使いました。ソースコードは こちら に公開されています。

証明が難しかった定理3選

1. 定理3.4

定理の主張は以下です。

有界実数列は常に収束する部分列を持つ。

ボルツァーノ • ワイヤストラスです。証明の概要は以下です。

1. 有界実数列$a_n$に対して以下を満たす閉区間の列$I_n$を構成する
   • 任意の自然数$n$に対し$\{k \in \mathbb{N} \ | \ a_k \in I_n\}$は無限集合
   • 任意の自然数$n$に対し$I_{n+1}\subset I_n$
   • 任意の自然数$n$に対し$I_{n+1}$の幅が$I_n$の幅の$\frac{1}{2}$
2. 区間縮小法を用いて任意の自然数$n$に対して$x\in I_n$となる$x\in \mathbb{R}$が唯一存在することを言う
3. 自然数列$b_n$を以下を満たすように作り
   • 任意の自然数$n$に対し$b_n < b_{n+1}$
   • 任意の自然数$n$に対し$a_{b_n} \in I_n$

$a_{b_n}$が$x$に収束することを言う

これの難しかったところはただでさえ証明が複雑なのに以下の2つが初めてでてきたことです。

• 再帰を用いた関数の定義
• 閉区間の型の定義

再帰を用いた関数の定義は例えば階乗だと

      (fix fact (n : nat) : nat := 
match n with 
  | 0%nat => 1%nat
  | S n0 => (S n0) * (fact n0)%nat 
end)
    

このように書けます。これだけだと難しくないのですが閉区間の型をどう定義するか分からないので閉区間の列の再帰的な定義が大変でした。色々調べているとCoqには$\{x : T \ | \ A \ x\}$という型があることを知りました。感覚的には数学での意味と同じで$T$の要素$x$の中で$A \ x$を満たすものの集まりです。これの要素は

      exist A (Tの要素t) (A tが成立する証明)
    

とすると作ることができます。つまり($T$の要素$t$)と($A \ t$が成立する証明)の組で作れます。公理なしだと2つの$A \ t$の証明H1,H2に対し

      exist A t H1 = exist A t H2
    

を示すことができません。そこで Coq.Logic.ProofIrrelevance の

      Axiom proof_irrelevance : forall (P:Prop) (p1 p2:P), p1 = p2.
    

を使いました。同じ命題の証明は全て等しいという公理です。ここまで分かると定理を証明するのは流れ作業でできましたがそれまでが大変で挫折しかけました。

2. 定理5.8

定理の主張は以下です。

$a_n$,$b_n$を実数(複素数)列とする。$\sum_{n=0}^\infty a_n$,$\sum_{n=0}^\infty b_n$が$a$,$b$に絶対収束するとき
実数(複素数)列$c_n$を$c_n=\sum_{k=0}^na_k b_{n-k}$と定義すると$\sum_{n=0}^\infty c_n$は$ab$に絶対収束する。

証明の本質部分は
$$\sum_{k=0}^{2n}c_k - \sum_{k=0}^na_k\sum_{k=0}^nb_k$$
が$n\to\infty$で$0$に収束することの証明です。これを証明するには
$$ \sum_{k=0}^nc_n = \sum_{k=0}^n\sum_{l=0}^{n-k}a_kb_l $$
を示せないといけません。これは並び替えるだけなので教科書では明らかとされていますがCoqではきちんと証明しないといけません。$n = 2$の場合上の式の左辺と右辺はそれぞれ

• $ a_0b_0 + (a_0b_1 + a_1b_0) + (a_0b_2 + a_1b_1 + a_2b_0) $
• $ a_0b_0 + a_0b_1 + a_0b_2 + (a_1b_0 + a_1b_1) + a_2b_0$

です。この2つは並び替えているだけなので等しいことは分かりますが、一般の$n$で愚直に交換法則と結合法則を用いて証明するのはやりたくないと思いました。
そこで「並び替えているだけなので等しい」をCoqで一般化して作りそれを使おうと思いました。作ったものは こちら です。
ここで作ったもののイメージは$X$の有限集合$A$と可換モノイド$(M,+)$と$f : X \rightarrow M$に対し
$$ \sum_{a\in A} f \ a$$
を定義しました。これを定義するには$A$からどういう順番で要素を取っても値が等しいことを証明しないといけませんでしたが、それは交換法則や結合法則を繰り返し用い示しました。またこれに関して様々なライブラリを作りました。例えば

• $X$の有限集合$A$,$B$に対し$A\cap B=\phi$なら$\sum_{x\in A\cup B} \ f \ x = \sum_{x\in A} \ f \ x \ + \sum_{x\in B} \ f \ x$
• $X$の有限集合$A$と$g : X \rightarrow Y$に対し$\sum_{x\in A} \ f \ x = \sum_{y\in g (A)}\sum_{g \ x \ = \ y}\ f \ x$

などです。これらを使うと示すことができました。

3. 定理 7.4

定理の主張(のうち証明が難しかったの)は以下です。

$\mathbb{R}^n$の集合$K$に対して$K$が有界閉集合ならコンパクトである。

証明の概略は以下です。

1. 背理法を使う。有界閉集合$K$に対して有限個の開集合$U_{\lambda_1},U_{\lambda_2},\cdots,U_{\lambda_m}$で$K \subset \cup_{k=1}^mU$を満たすものが存在しない開被覆$(U_\lambda)_{\lambda\in L}$を取る
2. 以下を満たす$n$次元有界閉区間の列$I_m$を構成する
   • 任意の自然数$m$に対し$I_m$は有限個の開集合$U_{\lambda_1},U_{\lambda_2},\cdots,U_{\lambda_k}$で被覆できない
   • 任意の自然数$m$に対し$I_{m+1}\subset I_m$
   • 任意の自然数$m$に対し$I_{m+1}$のそれぞれの幅が$I_m$の対応する幅の$\frac{1}{2}$
3. 区間縮小法を用いて任意の自然数$m$に対して$x\in I_m$となる$x\in \mathbb{R}^n$が唯一存在することを言う
4. Kは閉集合なので$x\in K$で$x\in U_{\lambda_x}$となる$\lambda_x \in L$が存在することを言う
5. $I_m \subset U_{\lambda_x}$を満たす$m\in \mathbb{N}$が存在することを言い矛盾を導く

これは定理3.4がパワーアップした感じです。2で$I_m$を$2^n$個に分けるとどれかは有限個の開集合$U_{\lambda_1},U_{\lambda_2},\cdots,U_{\lambda_k}$で被覆できないを示すのが大変ですし、他の所も大変でした。

終わりに

始める前はどこかで作業量が多くなりすぎて挫折するかもしれないと思っていました。しかし§6に入ると少なくとも1章まではなんとかなるだろうと思うようになりました。
　終わってみると24336行の728kbのソースコードができあがりました。教科書の証明よりは形式的証明は長くなってしまいますが労力は高々数倍なのかなと思いました。
　数学の証明をCoqで検証するのはライブラリが充実していてそれが検索可能な状態になっていたら実用的なのかなと思いました。
　教科書の証明をCoqに翻訳したものを公開するのはその状態を作ることにつながると思うので、時間があるときに引き続きやっていきたいと思います。

これから

自分の修士の研究の証明をするためには基礎的な線形代数が必要なのでまずはそれをやります。解析入門の2章は微分なのですが微分にも行列が出てくるので線形代数が必要になります。