プログラムを使って数学の証明をしよう～後編：Leanで色々証明する！～

2025/02/12 Lean 証明アシスタント数学

Lean4を使って色々な証明をしてみよう

前前回・前回のおさらい

前前回は自然数をLean4内で定義しました。
前回はLean4内で計算を行い、自然数の定義に成功している事を確認しました。また、Lean4を使って証明を行う方法を紹介しました。

ここまでのコード

フォルダ構成

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

N.lean

inductive N where
  | zero : N
  | succ : N → N
  deriving Repr

namespace N

-- Define addition (add function) and assign it
def add (m n : N) : N := match n with
| zero => m
| succ n' => succ (add m n')

instance : Add N where
  add := add

-- Define multiplication (mul function) and assign it
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

NaturalNumber.lean

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

-- Use #eval to evaluate a formula
#eval zero
#eval succ zero
#eval zero.succ
#eval succ (succ zero)
#eval zero.succ.succ

-- Defining values
def one := zero.succ
def two := one.succ

-- Addition
#eval add two zero
#eval add two one

#eval two + zero
#eval two + one

-- Multiplication
#eval mul two zero
#eval mul two one
#eval mul two two

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

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

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

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

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

本シリーズ最終回の今回は、より複雑な証明を行っていこうと考えています。最後まで読んでいただけると幸いです！

足し算の定義を定理として名前を付ける

まずはコードをどどん！

theorem add_zero (m: N) : m + zero = m := rfl
theorem add_succ (m n: N) : m + succ n = succ (m + n) := rfl

色々と新記法が登場しましたね！　一つずつ解説していきます！

まずはtheoremについて。これはその名の通り定理を表します。実は補題を意味するlemmaとtheoremの違いはほとんどなく、重要な物はtheorem、それほど重要で無い物はlemmaと考えてひとまず大丈夫です。

次に := rflという部分。「byを使わずに証明を書いて大丈夫なの？！」と戸惑うかもしれませんが、実は大丈夫です。省略形という奴ですね。

さて、add_zeroは自然数 $m$ について $m+0=m$ が成り立つという事を示しています。これは足し算の定義から明らかなので、証明無しでrfl出来ます。

また、add_succは自然数 $m, n$ について $m+succ(n)=succ(m + n)$ が成り立つという事を示しています。これも足し算の定義から明らかなので、証明無しでrfl出来ます。

※参考：足し算の定義
$n+0=n$
$n+succ(m)=succ(n+m)$

つまりここでは足し算の定義を定理として名前を付けています。

掛け算も同じようにやってみよう！

theorem mul_zero (m: N) : m * zero = zero := rfl
theorem mul_succ (m n: N) : m * (succ n) = (m * n) + m := rfl

参考：掛け算の定義
$n\times 0=0$
$n\times succ(m)=(n \times m) + n$

足し算同様に掛け算の定義にも定理名を付けました。

zero_add：0+n=?

問題4

$0+n=n$ を証明せよ

「これも足し算の定義から当たり前だな」と思ったそこの貴方、ご注意を！　これは足し算の定義には存在しません！！

定義そのままではないのでキチンと証明するまではrflしてはいけません！

解答

数学的帰納法を用いて証明する。

$n=0$ の時、add_zeroより左辺は $0$ である。 $0=0$ となりrfl。

$n'$ の時この命題が成立していると仮定する。
$n=succ(n')$ の時、add_succより $0+succ(n')=succ(0+n')$ のように変形できる。
仮定より $succ(0+n')=succ(n')=n$ であり、 $succ(n')=succ(n')$ となりrfl。

「おいおい、数学的帰納法とか言い出したぞコイツ！」

「はい。こんな簡単な証明をするにも数学的帰納法が必要なのです。先が思いやられますね」

ともかく、上記の数学的帰納法をLeanに直すと次のようになります。

theorem zero_add (n : N) : zero + n = n := match n with
| zero => by
  rewrite [add_zero] -- 0 = 0
  rfl
| succ n' => by
  rewrite [add_succ] -- succ(0+n') = succ(n')
  rewrite [zero_add] -- succ(n') = succ(n')
  rfl

match n withという構文が出てきましたね。……説明しなくても分かりますかね？　nがzeroの時とそれ以外で証明が分岐する事を意味しています。

zeroの時はrewrite [add_zero]で $0+0$ を $0$ に変形してからrflです。

succ n'の時はまずrewrite [add_succ]で $0+succ(n')$ を $succ(0+n')$ に変形します。
rewrite [zero_add]では数学的帰納法の仮定として自分自身を適応しています。これで $succ(0+n')$ が $succ(n')$ に変形されrflです。

succ_add：succ(m)+n=?

問題5

$succ(m)+n=succ(m+n)$ を証明せよ

解答

数学的帰納法を用いて証明する。

$n=0$ の時、add_zeroより両辺共に $succ(m)$ となりrfl。

$n'$ の時この命題が成立していると仮定する。
$n=succ(n')$ の時、add_succより左辺は $succ(m)+succ(n')=succ(succ(m)+n')$ のように変形できる。
また右辺は $succ(m+succ(n'))=succ(succ(m+n'))$ のように変形できる。
仮定より左辺は $succ(succ(m)+n')=succ(succ(m+n'))$ となりrfl。

theorem succ_add (m n: N) : succ m + n = succ (m + n) := match n with
| zero => by
  repeat rewrite [add_zero] -- succ(m)=succ(m)
  rfl
| succ n' => by
  repeat rewrite [add_succ] -- succ(succ(m) + n') = succ(succ(m + n'))
  rewrite [succ_add] -- succ(succ(m + n')) = succ(succ(m + n'))
  rfl

repeat rewriteという構文が出てきました。これはrewriteを複数回適応するという意味です。左辺右辺共に適応する為に今回使用しました。

交換法則を証明する

問題6

$a + b = b + a$ を証明せよ。

いわゆる交換法則というものですね。これも数学的帰納法を使って証明します。

解答

theorem add_comm(a b:N) : a + b = b + a := match b with
| zero => by
  rewrite [add_zero] -- a = 0+a
  rewrite [zero_add] -- a = a
  rfl
| succ b' => by
  rewrite [add_succ] -- succ(a + b') = succ(b') + a
  rewrite [succ_add] -- succ(a + b') = succ(b' + a)
  rewrite [add_comm] -- succ(b' + a) = succ(b' + a)
  rfl

結合法則を証明する

問題7

$(a + b) + c = a + (b + c)$ を証明せよ。

いわゆる結合法則と呼ばれるものです。これも証明していきましょう！

解答

theorem add_assoc(a b c:N) : (a + b) + c = a + (b + c) := match c with
| zero => by
  repeat rewrite [add_zero] -- a + b = a + b
  rfl
| succ c' => by
  repeat rewrite [add_succ] -- succ((a + b) + c') = succ(a + (b + c'))
  rewrite [add_assoc] -- succ(a + (b + c')) = succ(a + (b + c'))
  rfl

repeat rewrite [add_succ]の部分だけ途中計算を記しておきますね。赤枠が青枠に変換されています。

(a + b)

succ(c')

= a + (b + succ(c'))

succ((a + b) + c')

= a + (

succ(c')

)

succ((a + b) + c') =

succ(b + c')

succ((a + b) + c') =

succ(a + (b + c'))

分配法則を証明する

問題8

$(a + b) * c = a * c + b * c$ を証明せよ

解答

-- 再掲
theorem mul_zero (m: N) : m * zero = zero := rfl
theorem mul_succ (m n: N) : m * (succ n) = (m * n) + m := rfl
--

theorem distributive(a b c:N) : (a + b) * c = a * c + b * c := match c with
| zero => by
  repeat rewrite [mul_zero]
  rewrite [add_zero]
  rfl
| succ c' => by
  repeat rewrite [mul_succ]
  rewrite [distributive]
  nth_rewrite 1 [add_assoc]
  nth_rewrite 1 [add_assoc]
  nth_rewrite 2 [← add_assoc]
  nth_rewrite 2 [add_comm]
  nth_rewrite 2 [← add_assoc]
  nth_rewrite 2 [add_comm]
  nth_rewrite 6 [add_comm]
  rfl

途中過程を載せるとこんな感じ

theorem distributive(a b c:N) : (a + b) * c = a * c + b * c := match c with
| zero => by
  repeat rewrite [mul_zero]
  rewrite [add_zero]
  rfl
| succ c' => by
  repeat rewrite [mul_succ] -- (a + b) * c' + (a + b) = a * c' + a + (b * c' + b)
  rewrite [distributive] -- a * c' + b * c' + (a + b) = a * c' + a + (b * c' + b)
  nth_rewrite 1 [add_assoc] -- a * c' + (b * c' + (a + b)) = a * c' + a + (b * c' + b)
  nth_rewrite 1 [add_assoc] -- a * c' + (b * c' + (a + b)) = a * c' + (a + (b * c' + b))
  nth_rewrite 2 [← add_assoc] -- a * c' + (b * c' + a + b) = a * c' + (a + (b * c' + b))
  nth_rewrite 2 [add_comm] -- a * c' + (b + (b * c' + a)) = a * c' + (a + (b * c' + b))
  nth_rewrite 2 [← add_assoc] -- a * c' + (b + b * c' + a) = a * c' + (a + (b * c' + b))
  nth_rewrite 2 [add_comm] -- a * c' + (a + (b + b * c')) = a * c' + (a + (b * c' + b))
  nth_rewrite 6 [add_comm] -- a * c' + (a + (b + b * c')) = a * c' + (a + (b + b * c'))
  rfl

最後に

これにて『プログラムを使って数学の証明をしよう』シリーズは完結となります。ここまで飽きずにこの記事を読んでいただき本当にありがとうございます！！

KUMEC