Lean4を使って計算してみよう

前回のおさらい

前回は自然数をLean4内で定義しました。そのプログラムを再掲します。

inductive N where
  | zero : N
  | succ : N → N
  deriving Repr
namespace N
def add (m n : N) : N := match n with
| zero => m
| succ n' => succ (add m n')
instance : Add N where
  add := add
def mul (m n : N) : N := match n with
| zero => zero
| succ n' => mul m n' + m
instance : Mul N where
  mul := mul
end N

ここではペアノの公理を用いて自然数およびその足し算、掛け算が定義されています。これを利用して計算を行ってみましょう！

なお、プロジェクトフォルダの構成はこのようになっています。

root
├NaturalNumber.lean　(←今回書くプログラム)
├NaturalNumber
│└ N.lean　(←上記のプログラム)
└その他の依存ファイル

まずは諸々をインポート

プロジェクトフォルダ直下にあるソースファイルを編集していきます。まずは必要な物をインポートしましょう。Pythonと似たイメージですね。ただしleanではimportはファイルの最初に書く必要があるので注意が必要です。

import Mathlib.Tactic.Common
import NaturalNumber.N
open N

inductive Nの内容にアクセスする為にopen Nと書いています。C++で言うusing namespace N;のようなイメージです。

デバッグはprintではなく#eval

計算結果を表示する時、Pythonならprint文で表示しますが、Leanなら#evalを使います。例えばこんな感じです。

#eval zero

-- 以下の二つは同じ意味になる
#eval succ zero
#eval zero.succ

-- 以下の二つは同じ意味になる
#eval succ (succ zero)
#eval zero.succ.succ

-- これはだめ
-- #eval succ succ zero

実行結果

N.zero
N.succ (N.zero)
N.succ (N.zero)
N.succ (N.succ (N.zero))
N.succ (N.succ (N.zero))

このように関数呼び出しはsucc 引数もしくはsucc (引数)もしくは引数.succのように書く事が出来ます。

ただしsucc succ zeroのように書くと(succ succ) zeroと解釈されてエラーとなります。succ 引数のようにかっこを省略できるのは、引数が明確な時だけなので注意しましょう。

数を定義しよう

zeroは定義済みですが、その他の数値が未定義のままとなっており、少し扱いにくいです。そこでoneとtwoだけでも定義しておきましょうか。そんな訳で以下のコードを書きます。

def one := zero.succ
def two := one.succ

ゼロの次が1、1の次が2という意味ですね。Pythonと違って定数の定義もdefで行う事に注意しましょう。

足し算をしてみよう

続いて足し算です。足し算はadd関数で定義されており、それを+記号と等価にするようにしていました。ですのでadd関数を呼び出す事でも+する事でも足し算の検証を行えます。

#eval add two zero
#eval add two one

#eval two + zero
#eval two + one

実行結果

N.succ (N.succ (N.zero))
N.succ (N.succ (N.succ (N.zero)))
N.succ (N.succ (N.zero))
N.succ (N.succ (N.succ (N.zero)))

想定通りの挙動をしています。

掛け算をしてみよう

次に掛け算です。足し算と同様、掛け算もmul関数および*で呼び出す事が出来ます。

#eval mul two zero
#eval mul two one
#eval mul two two

#eval two * zero
#eval two * one
#eval two * two

実行結果

N.zero
N.succ (N.succ (N.zero))
N.succ (N.succ (N.succ (N.succ (N.zero))))
N.zero
N.succ (N.succ (N.zero))
N.succ (N.succ (N.succ (N.succ (N.zero))))

$2 \times 0 = 0$
$2 \times 1 = 2$
$2 \times 2 = 4$

の三つの掛け算を計算しています。上手く動作している事が確認できますね！

Lean4を使って証明をしてみよう

プログラムを使って証明？

プログラムを使ってどのように証明を行うかと言いますと「式変形を繰り返し、左辺等辺が同じになる事を確認」します。その方法を順序だてて解説していきます。

Q.E.Dではなくrfl

早速ですが問題です。

問題1

$x * y + z = x * y + z$ を証明せよ

「？」となった方が多いでしょう。証明するも何も、当たり前の事じゃないかと。そうです、当たり前の事ではあるのです。しかしながら、プログラム的にはキチンと「証明完了」という事を明記しないといけないのです。
数学的に表現すると、問題1の解答は以下のようになります。

解答

Q.E.D.

これらの事をLeanで書くと次のようになります。

lemma example_rfl (x y z : N) : x * y + z = x * y + z := by
  rfl

lemmaとは補題という意味の英単語です。続くexample_rflは補題名です。 (x y z : N)では「この補題にはx,y,zという三つの自然数が登場します」という意味です。

: 中略 := byの部分が補題の内容です。今回は「x * y + z = x * y + z」が補題の内容です。

二行目の rflが数学で言うQ.E.D.です。

おめでとうございます、これで「Leanを使って証明をする」の実績解除です！

代入はrewrite

問題2

$y=x+1 \rArr 2y = 2(x+1)$ を証明せよ

解答

$y$ に$y=x+1$ を代入すると$2(x+1)=2(x+1)$ となる。
Q.E.D.

またビックリするくらい簡単な問題です。こんなの問題と言ってもいいのか……。それはともかく、ここでは新しく「代入」という操作が出てきました。これをleanではrewriteで表します。

lemma example_rewrite_1 (x y : N) (h: y=x+one) : two * y = two * (x+one) := by
  rewrite [h]
  rfl

一行目で先ほどから変わっているのは(h: y=x+one)の部分でしょう。これは「hという名前でy=x+oneという前提条件を使います」という意味です。

二行目でrewrite [h]と書いており、これが「hの内容を代入する」という意味です。ここで注意したいのはhを[]で囲む事です。このかっこを付けるのを忘れないようにしましょう。

三行目はみんな大好きQ.E.D.の代わりであるrflです。

別解

$x+1$ に$y=x+1$ を代入すると$2y=2y$ となる。
Q.E.D.

先ほどの問題の別解です。ここでは$y=x+1$ を命題に代入する際、(x+1)にyを代入するという「先ほどと逆」の操作をしています。これを行うLeanのコードがこちらです。

lemma example_rewrite_2 (x y : N) (h: y=x+one) : two * y = two * (x+one) := by
  rewrite [← h]
  rfl

※←は\r で変換される。また<-でも可。

「おいおい、プログラミングに矢印なんで出てきたぞ」と驚きました。Leanはなかなかスタイリッシュな言語ですね！

問題3

$y=x+1 \rArr y \times y = y \times (x+1)$ を証明せよ

解答

二つ目の$y$ に$y=x+1$ を代入すると$y \times (x+1)=y \times (x+1)$ となる。
Q.E.D.

上記のような「○○個めのyに代入」のような操作はnth_rewriteというコマンドを使います。という訳でLeanのコードをドン！

lemma example_nth_rewrite (x y : N) (h: y=x+one) : y * y = y * (x+one) := by
  nth_rewrite 2 [h]
  rfl

nth_rewrite 数字 [条件名]という記法で「○○個めに代入」という操作を行えます。

今回はここまでとします！

次回はもっと難しい証明を出来たらと思っています。それではしーゆー！