17

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

2288
1

はじめに

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

Coqでの証明

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

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

Coqでの証明の魅力は

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

などです。

やろうと思った背景

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

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

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

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

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

やったこと

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

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

1. 定理3.4

定理の主張は以下です。

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

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

  1. 有界実数列anに対して以下を満たす閉区間の列Inを構成する
    • 任意の自然数nに対し{kN | akIn}は無限集合
    • 任意の自然数nに対しIn+1In
    • 任意の自然数nに対しIn+1の幅がInの幅の12
  2. 区間縮小法を用いて任意の自然数nに対してxInとなるxRが唯一存在することを言う
  3. 自然数列bnを以下を満たすように作り
    • 任意の自然数nに対しbn<bn+1
    • 任意の自然数nに対しabnIn

abnxに収束することを言う

これの難しかったところはただでさえ証明が複雑なのに以下の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

定理の主張は以下です。

an,bnを実数(複素数)列とする。n=0an,n=0bna,bに絶対収束するとき
実数(複素数)列cncn=k=0nakbnkと定義するとn=0cnabに絶対収束する。

証明の本質部分は
k=02nckk=0nakk=0nbk
n0に収束することの証明です。これを証明するには
k=0ncn=k=0nl=0nkakbl
を示せないといけません。これは並び替えるだけなので教科書では明らかとされていますがCoqではきちんと証明しないといけません。n=2の場合上の式の左辺と右辺はそれぞれ

  • a0b0+(a0b1+a1b0)+(a0b2+a1b1+a2b0)
  • a0b0+a0b1+a0b2+(a1b0+a1b1)+a2b0

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

  • Xの有限集合A,Bに対しAB=ϕならxAB f x=xA f x +xB f x
  • Xの有限集合Ag:XYに対しxA f x=yg(A)g x = y f x

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

3. 定理 7.4

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

Rnの集合Kに対してKが有界閉集合ならコンパクトである。

証明の概略は以下です。

  1. 背理法を使う。有界閉集合Kに対して有限個の開集合Uλ1,Uλ2,,UλmKk=1mUを満たすものが存在しない開被覆(Uλ)λLを取る
  2. 以下を満たすn次元有界閉区間の列Imを構成する
    • 任意の自然数mに対しImは有限個の開集合Uλ1,Uλ2,,Uλkで被覆できない
    • 任意の自然数mに対しIm+1Im
    • 任意の自然数mに対しIm+1のそれぞれの幅がImの対応する幅の12
  3. 区間縮小法を用いて任意の自然数mに対してxImとなるxRnが唯一存在することを言う
  4. Kは閉集合なのでxKxUλxとなるλxLが存在することを言う
  5. ImUλxを満たすmNが存在することを言い矛盾を導く

これは定理3.4がパワーアップした感じです。2でIm2n個に分けるとどれかは有限個の開集合Uλ1,Uλ2,,Uλkで被覆できないを示すのが大変ですし、他の所も大変でした。

終わりに

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

これから

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

投稿日:20201230
OptHub AI Competition

この記事を高評価した人

高評価したユーザはいません

この記事に送られたバッジ

バッジはありません。
バッチを贈って投稿者を応援しよう

バッチを贈ると投稿者に現金やAmazonのギフトカードが還元されます。

投稿者

itleigns
itleigns
18
2509

コメント

他の人のコメント

コメントはありません。
読み込み中...
読み込み中
  1. はじめに
  2. Coqでの証明
  3. やろうと思った背景
  4. やったこと
  5. 証明が難しかった定理3選
  6. 1. 定理3.4
  7. 2. 定理5.8
  8. 3. 定理 7.4
  9. 終わりに
  10. これから