Leanによるペアノの公理

Lean で証明を書いていく勉強を始めました。エディタは VSCode を使うことにしました（公式のインストールガイド）。JetBrains 系のエディタも試したのですが、補完がほとんど効かず辛かったので断念しました。

教材には「ゼロから始めるLean言語入門 手を動かして学ぶ形式数学ライブラリ開発」を使い、内容を写経しながら学んだことをまとめていきます。今回はその第一歩、ペアノの公理です。

ペアノの公理とは

ペアノの公理は自然数の定義です。「1, 2, 3, ... と無限に続く数」と素朴に説明したくなりますが、それではプログラムにできません。Lean で自然数を厳密に扱うためには、ペアノの公理のように形式的に定義する必要があります。

ペアノの公理は以下の5つです。

1. 0 は自然数である
2. 自然数から自然数への関数 succ が存在する（例: succ(0) = 1）
3. 異なる自然数に対する関数 succ の結果は異なる
4. 0 と succ の結果は必ず異なる
5. 数学的帰納法が成り立つ。つまり、0 である主張が成り立つことを示し、任意の n に対して「n である主張が成り立つならば n+1 でもその主張が成り立つ」ことを示せば、すべての自然数でその主張が成り立つことになる

数学では主張のことを命題と呼び、変数 n によって変わる命題のことを述語と呼びます。

Lean で自然数を自作する

Lean には標準で Nat という自然数の型が用意されていますが、勉強のためにまずは自分で MyNat を定義してみます。

inductive MyNat where
    | zero
    | succ(n : MyNat)

これだけでペアノの公理を満たす自然数の定義として完成しているそうです。本当にそうなのか確かめてみます。1. と 2. についてはそのまま定義しているので満たしていることがわかります。一方で、succ の単射性（公理3）や 0 が succ の結果に現れないこと（公理4）を明示的に定義していない点は少し気になりますが、これらは inductive によって自動的に保証される性質のようです。

ここで出てくる where と | について整理しておきます。

• where キーワードは、「ここから先が、このデータ型の具体的な中身（構成子のリスト）ですよ」というスコープを開始することを示します。
• |（バー）は、「新しく独立した構成子（値の作り方）を1つ宣言する」ために使用されます。

zero と succ がどちらも MyNat 型であることは、以下のコマンドで確認できます。

#check MyNat.zero
#check MyNat.succ

足し算を定義する

次は足し算です。match で場合分けし、n = 0 のときは m を、n が succ n のときは succ (add m n) を返すように定義します。この定義はペアノの算術そのままです。

def MyNat.add(m n : MyNat): MyNat :=
    match n with
    | .zero => m
    | .succ n => succ (add m n)

:= は定義を表しますが、以下のように = を使うと命題として扱われます。「1 + 1 = 2」のような等式も、Lean の世界では Prop（命題型）として表現されることが、#check を使うと確認できます。

#check MyNat.add .one .one = .two

#reduce は式を簡約した結果を表示するコマンドです。簡約とは、式を最も基本的な形であるコンストラクタでの表現に書き直すこと、つまり公理の組み合わせまで書き下すことを意味します。

#reduce MyNat.add .one .one
#reduce MyNat.two

証明してみる

「1 + 1 = 2」は以下のように証明できます。example は名前をつけずに証明するコマンドで、定理として残したい場合は theorem を使います。

example : MyNat.add .one .one = .two := by
    rfl

rfl は自動証明で使うキーワードです。rfl は Reflexivity（反射律）の略で、「左辺と右辺の計算結果が完全に一致する（同じものになる）ので、この等式は正しい」ということを Lean に認めさせます。VSCode の infoview に Goals accomplished! と表示されれば証明成功です。

同じ命題を、式を段階的に書き換えることでも証明できます。

example : MyNat.add .one .one = .two := by
    change MyNat.succ (MyNat.add .one .zero) = .two
    change MyNat.succ .one = .two
    change MyNat.succ .one = MyNat.succ .one
    trivial

ビルドしてみる

lakefile.lean を以下のように修正すると、LearnLean をビルド対象に加えることができます。

@[default_target]
lean_lib «LearnLean» where
  globs := #[.submodules `LearnLean]

lake build を実行すると、以下のようにビルドされます。

LearnLean % lake build
ℹ [2/3] Built LearnLean.NaturalNumber
info: LearnLean/NaturalNumber.lean:7:0: MyNat.zero : MyNat
info: LearnLean/NaturalNumber.lean:8:0: MyNat.succ (n : MyNat) : MyNat
info: LearnLean/NaturalNumber.lean:9:0: MyNat.zero.succ : MyNat
info: LearnLean/NaturalNumber.lean:21:0: MyNat.one.add MyNat.one = MyNat.two : Prop
info: LearnLean/NaturalNumber.lean:26:0: MyNat.succ (MyNat.succ MyNat.zero)
info: LearnLean/NaturalNumber.lean:27:0: MyNat.succ (MyNat.succ MyNat.zero)
Build completed successfully (3 jobs).

無事ビルドが通り、自作の MyNat 上で 1 + 1 = 2 が証明できることを確認できました。