ライセンス

この記事上のコードはすべて CC0 (パブリックドメイン) で公開します。

この記事のコードは以下でも公開しています。

Lean4とは

Lean4は関数型プログラミング言語のように使える証明支援系です。証明支援系では数学で行われる「証明」を形式化して展開することができます。

注意

この記事では自然数 ( $\N$ ) は $0$ から始まります。

$\N = \{0, 1, 2, \cdots\}$

数学的帰納法

数学的帰納法について振り返ります。

ある自然数に関する命題 $P(n)$ について、すべての $n \in \N$ で成り立つことを証明するのがゴールです。

$P(n)$ としては以下のような例が考えられます

$n = n$
$n + 1 = 1 + n$
$n$ は奇数
$\displaystyle\sum_{k=0}^{n} k = \frac{n(n+1)}{2}$
$a_0 = 2, a_{n+1} = 2 a_n + 3^n$ の一般項は $a_n = 2^n + 3^n$

3番目の例は $n=8$ や $n=12$ などで当然正しくない命題ですが、いずれにしても命題ではあります。

受験数学までによく見かける数学的帰納法の用途は、4番目以降の例のような、一般項を求める問題などではないでしょうか。

さて、すべての $n$ で $P(n)$ が成り立つ、というのを $\forall n \in \N, P(n)$ のように書きます。場合によっては $\forall n, P(n)$ のようにドメインを省略したりします。

$\forall$ という記号は全称記号と呼ばれ、日本語では「すべての...」「任意の...」などのように読み、英語では "for all ..." などのように読みます

すべての、というのはつまり、 $P(0), P(1), P(2)$ はもちろん成り立つし、 $P(8)$ や $P(100)$ など、あらゆるすべての自然数に対して、一切の漏れなく成り立つということです。

数学的帰納法とは次のようなスキームの証明方法です。

任意の $n$ について $P(n)$ を証明します
初期: $n=0$ のときを証明します
帰納: $n=k+1$ のとき、 $k$ では成り立つと仮定して、 $n$ で成り立つことを証明します

これは先程の一般化した述語 $P$ を用いて以下のように書き換えられます

初期: $P(0)$ を証明します
帰納: 任意の $k \in \N$ に付いて $P(k)$ が成り立つと仮定すると $P(k+1)$ が成り立つことを証明します

帰納ケースは記号記号を使えば $\forall k \in \N, P(k) \Rightarrow P(k+1)$ とかけます。重要なのは、帰納ケースでは $P(10)$ が具体的に正しいとか言うことは言っていなくて $P(0) \Rightarrow P(1)$ , $P(1) \Rightarrow P(1)$ , $P(2) \Rightarrow P(3)$ , ..., $P(9) \Rightarrow P(10)$ , ... のように無限個の「〇〇ならば〇〇」

$A \Rightarrow B$ は「AならばBである」と読んでください。

この２つを証明することにより、任意の $n$ について正しいことが証明されます。

$P(0)$ : 初期ケースによって証明されている
$P(1)$ : $P(0)$ が証明されている、また、帰納ケースにより $P(0) \Rightarrow P(1)$ が証明されている、よって $P(1)$ が証明された (前件肯定)
$P(2)$ : $P(1)$ が証明されている、また、帰納ケースにより $P(1) \Rightarrow P(2)$ が証明されている、よって $P(2)$ が証明された
...
$P(k+1)$ : $P(k)$ が証明されている、また、帰納ケースにより $P(k) \Rightarrow P(k+1)$ が証明されている、よって $P(k+1)$ が証明された

このようにして、2パターンの場合分けによって、任意の自然数についての証明を、 $0$ から辿って得ることができました。

$P(5)$ を証明するとき: $P(0) \to P(1) \to P(2) \to P(3) \to P(4) \to P(5)$ の順で証明を得られる
$P(100)$ を証明するとき: $P(0) \to P(1) \to P(2) \to \cdots \to P(99) \to P(100)$ の順で証明を得られる
$P(n)$ を証明するとき: $P(0) \to P(1) \to P(2) \to \cdots \to P(n-1) \to P(n)$ の順で証明を得られる

(↑ここでは記号 $\to$ に特別な意味はありません)

Lean4における数学的帰納法

累積帰納法の説明の前に、Lean4における数学的帰納法の扱い方を紹介します。

数学的帰納法をおそらく中学生か高校生ぐらいの頃に授業で習ったかと思います。上記の論法は納得できますが、なにかこう、突拍子もなく登場した感じがして、テクニックとして考えている方も多いかもしれません。
しかし、数学的帰納法とは自然数を自然数たらしめる特徴とも考えられて、小学校までの算数で行われた算術(計算問題)の枠を出た、自然数に関した証明をしようとおもうと必然的に必要になります。

また、このような考察から始まり数理論理学に入門できる「コンピュータは数学者になれるのか?^[1]」という書籍も個人的には非常におすすめです。

数学的帰納法が本質的に重要な公理であるか、というのを説明してきました。Lean4での扱いはどうなっているのでしょうか？ Lean4 には Nat という、今我々がこの記事で論じている自然数に対応する型がデフォルトで用意されています。そして、数学的帰納法に対応する公理が Nat.rec として、これまた用意されています。

#check Nat
#check Nat.rec

更に踏み込めば、自然数に限らず、あらゆる帰納的な構造に自動でLean4が構造的機能法に対応する形で導入されます。
Lean4においては自然数も構造であり、数学的帰納法も構造的機能法の一種という形になっているのです。

ですので、Lean4で自分で自然数を定義したり自然数論をその上で展開することも可能です。

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

累積帰納法

累積帰納法(完全帰納法、Course-of-value recursion, complete recursive)とは、数学的帰納法の亜種のようなもので、 $\forall n \in \N, P(n)$ を示したい、というのは変わらないのですが、帰納ケース ( $n=k+1$ ) において使える前提を、 $P(k)$ だけではなく $P(0)$ から $P(k)$ まですべてに拡張したものです。

先程見たように、

$P(100)$ を証明するとき: $P(0) \to P(1) \to P(2) \to \cdots \to P(99) \to P(100)$ の順で証明を得られる

とう順番で証明されるわけですから、 $P(100)$ を証明しようというときに $P(99)$ が証明されていることを利用するだけでなく、 $P(1)$ や $P(10)$ , $P(50)$ が証明されているという事実も使えてよいはずです。

実際、 $\mathrm{PA} = \mathrm{PA}^{-} + (数学的帰納法)$ と $\mathrm{PA}^{-} + (累積帰納法)$ ^[2] の証明力は等価^[3]になります。

数学的な感覚では２つの論法が等価であることは上記の説明で通じるのですが、Lean4ではきちんと証明しなければなりません。この２つの間の関係を見ていきましょう。まずは論理式として定式化してみます。

数学的帰納法

$P(0) \to {}^{\forall k}(P(k) \to P(k+1)) \to {}^{\forall n}P(n)$

Lean4での定義は以下のようになります^[4]。

def NatInd := ∀P : Nat → Prop, (P 0 → (∀k, P k → P (k+1)) → ∀n, P n)

累積帰納法

${}^{\forall n}({}^{\forall k < n}P(k) \to P(n)) \to {}^{\forall n}P(n)$

Lean4での定義は以下のようになります。

def NatCompleteInd := ∀P : Nat → Prop, ((∀n, (∀k < n, P k) → P n) → ∀n, P n)

ここで、累積帰納法に初期ケースが存在しないように思うかもしれませんが、 ${}^{\forall n}({}^{\forall k < n}P(k) \to P(n))$ に $n=0$ を代入すると ${}^{\forall k < 0}P(k) \to P(0)$ が得られます。一方、 $k < 0$ は成り立つことはなく、無前提で $P(0)$ が得られることを意味しています。^[5]

累積帰納法を構成的に証明してみる

いきなりLean4の証明に取り掛かる前に、まずは方針を立てます。さて、先程の説明のとおり、数学的帰納法と累積帰納法は多少方法が異なるだけで同じことをしています。逆に数学的帰納法をもたない体系は本質的により弱いもになります。
ということは、数学的帰納法をどこかで使う必要はあるだろうな、という考察ができます。

これを証明しようとしてみるとわかりますが、かなり混乱します。(私だけかもしれないですが)

しかし、混乱を整理しながら証明を構築できて、誤った論法を許さないのもLean4のような証明支援系の利点と言えますね。

以下では試行錯誤の末にLean4で作成した証明を翻訳してみます。

証明:
累積帰納法で示したい述語を $Q(N)$ とします。任意の $n$ 　のものとで ${}^{\forall k < n} Q(k) \to Q(n)$ というのがわかっているもとで、任意の $N$ について $Q(N)$ が成り立つことを示したいです。

まず、元の累積帰納法の仮定に $n=N$ を代入すると　 ${}^{\forall k < N} Q(k) \to Q(N)$ が得られるので、任意の $N$ について、 ${}^{\forall k < N} Q(k)$ を示せば良いことがわかります。

さて、ここから数学的帰納法を適用することから考えます。そのための $P(n)$ を考えます。
$P(N) = {}^{\forall k < N} Q(k)$
とそのまま設定すればよいです。

初期: $P(0)$ は $k < 0$ を満たす $k$ が存在しないので成立します。

帰納: $P(K) = {}^{\forall k < K} Q(k)$ が成り立っているとします。つまり、 $Q(0), Q(1), \cdots, Q(K-1)$ が成り立っているとします。

$P(K+1) = {}^{\forall k < K+1} Q(k)$ を証明したいです。つまり $Q(0), Q(1), \cdots, Q(K-1), Q(K)$ を証明したいです。
明らかに帰納法の前提を使えば $Q(0)$ から $Q(K-1)$ までは証明できます。 $Q(K)$ を証明するには累積帰納法の前提を利用して ${}^{\forall k < K+1} Q(k) \to Q(K+1)$ 、つまり $Q(0) \wedge Q(1) \wedge \cdots \wedge Q(K) \to Q(K+1)$ がわかっているとします。

しかし、帰納法の仮定より $Q(0) \wedge Q(1) \wedge \cdots \wedge Q(K)$ はわかっているわけですから、 $(K+1)$ が得られました。■

***

さて、あえて日本語で書いた構成的な証明は上記のようになるわけですが、とにかく混乱するポイントが多いような気がしますね...とにかく、各変数のスコープがわかりにくいように思えます。

最終的に完成した Lean4 の証明が以下になります。

-- 累積帰納法
theorem cov_recursion { motive : Nat → Sort u } : (∀n, (∀k, (k < n) → motive k) → motive n) → (∀n, motive n) := by
  intro h N
  apply h N
  induction N with
  | zero => intros; contradiction
  | succ K H =>
    have hK := h K H
    intro k hk
    exact if _ : k < K then by
      have : k < K := by assumption
      apply H
      assumption
    else by
      have : ¬ k < K := by assumption
      have : K ≤ k := Nat.ge_of_not_lt ‹¬ k < K›
      apply Nat.le_of_succ_le_succ at hk
      have : k = K := Nat.le_antisymm ‹k ≤ K› ‹K ≤ k›
      rw [this]
      assumption

/-
'Nat.rec' does not depend on any axioms
-/
#print axioms Nat.rec
/-
'cov_recursion' does not depend on any axioms
-/
#print axioms cov_recursion

途中で使用している定理を紹介します。といっても、どれもあまりにも基本的な性質に関するものです。^[6]

Nat.ge_of_not_lt: $n \not< m \to n ≥ m$
Nat.le_of_succ_le_succ: $n+1 \le m+1 → n \le m$
Nat.le_antisymm: 反対称律 $n \le m \wedge m \le n \to n = m$

使用例: $2^{\lg n} \le n$ の証明

なお、 $1 \le n$ で考えます。

$2^{\lg n} \le n$ を証明してみます。というか、もともとこれを証明したくて^[7]、累積帰納法をそのために準備しました。
なお、ここでは $\lg x$ は $\lfloor \log_2 x \rfloor$ に相当する自然数上の関数としておきます。つまるところ、二進表記における桁数から $1$ 引いた数です。

例:

$\lg 1 = \lg 1_{(2)} = 0$
$\lg 10 = \lg 1010_{(2)} = 3$
$\lg 100 = \lg 1100100_{(2)} = 6$

なお、二進表記の場合は $(2)$ を小さく末尾につけることで表現しています。
一方で、 $2^{\lg n}$ とは、二進表記の最上位ビット以外を $0$ にした数です。

$n$	$n {}_{(2)}$	$\lg n$	$2^{\lg n} {}_{(2)}$
$1$	$1$	$0$	$1$
$2$	$10$	$1$	$10$
$3$	$11$	$1$	$10$
$4$	$100$	$2$	$100$
$10$	$1010$	$3$	$1000$
$100$	$1100100$	$6$	$1000000$

なので、4列目 $\le$ 2列目の関係、つまり $2^{\lg n} \le n$ とは感覚としては当たり前なのですが、この当たり前を Lean4 で証明してみようという試みです。

まずは方針を考えます。

$\lg$ の再帰関数としての定義

さて、 $\lg n = \lfloor\log_2 n\rfloor$ の定義のままだと扱いづらいので、 $\lg$ は以下のように定義します。

\lg n = \begin{cases} 0 & \text{if } n \le 1 \\ 1 + \lg \lfloor\frac{n}{2}\rfloor & \text{otherwise} \end{cases}

そして、これと同じ定義がすでにLean4組み込みのInit/Data/Nat/Log2.leanにあります。

def log2 (n : @& Nat) : Nat :=
  if n ≥ 2 then log2 (n / 2) + 1 else 0

なお、自然数同士の割り算 n / m は、そのまま自然数上で切り捨てられた値 ( $\lfloor \frac n m \rfloor$ ) になります。 Pythonの n // m やC/Rust の整数除算 n / m に近いです。^[8]

全域関数にするために log2 0 = 0 として定義されていますが、本質ではないので気にしなくて問題ないです。

なお、同ファイルの中で、より弱い定理 Nat.log2 n ≤ n が証明されていますね。

証明の概略

準備ができたので証明の概略を紹介します。といっても簡単です。

累積帰納法で示します。対象となる術後は当然 $P(n) = 2^{\lg n} \le n$ です。

$n = 1$ のときは計算すれば確認できるので、 $2 \le n$ の場合を考えます。示したいのは $2^{\lg n} \le n$ です。 $\lg$ の定義より、 $2^{1+\lg \lfloor \frac{n}{2} \rfloor} \le n$ と書き直せます。

また、累積帰納法の仮定より、 $\lfloor \frac{n}{2} \rfloor \le n$ なので $P(\lfloor \frac{n}{2} \rfloor) = 2^{\lg \lfloor \frac{n}{2} \rfloor} \le \lfloor \frac{n}{2} \rfloor$ が利用できます。両辺に2をかけると

$2^{1 + \lg \lfloor \frac{n}{2} \rfloor} \le 2 \lfloor \frac{n}{2} \rfloor$ が得られますが、ここで　 $2 \lfloor \frac{n}{2} \rfloor \le n$ なので、 $P(n)$ が示されました。 ■

***

最終的にLean4で以下のように証明できました。

-- 2^(lg n) ≤ n
theorem power2to_lg_n_le_n : ∀n > 0, 2^(Nat.log2 n) ≤ n := by
  apply cov_recursion
  intro n
  match n with
  | 0 => intros; contradiction
  | 1 => trivial
  | n+2 =>
    intro h _
    set n := n+2
    set log2_n := Nat.log2 n
    let k := n/2
    let log2_k := Nat.log2 k

    have hk := h k
    have : k < n := Nat.bitwise_rec_lemma (Nat.succ_ne_zero _)
    have hk := hk ‹k < n›
    have : 2 ≤ n := Nat.le_add_left ..
    have : 0 < k := Nat.div_pos ‹2 ≤ n› (show 0 < 2 by trivial)
    have hk : 2 ^ log2_k ≤ k := hk ‹0 < k›
    have hk2 : 2 * 2 ^ log2_k ≤ 2 * k := Nat.mul_le_mul_left 2 hk
    have : 2 * 2 ^ log2_k = 2 ^ (log2_k + 1) := d_mul_pow_d_to_k_eq_d_to_pow_succ_k 2 log2_k
    rw [this] at hk2
    have : 2 * k ≤ n := d_mul_n_div_d_le_d ..
    have : log2_n = log2_k + 1 := by
      generalize h: log2_k + 1 = rhs
      unfold Nat.log2
      split
      . rw [←h]
      . contradiction
    rw [‹log2_n = log2_k + 1›]
    show 2 ^ (log2_k+1) ≤ n
    calc
      2 ^ (log2_k+1) ≤ 2 * k := hk2
      _ ≤ n := ‹2*k ≤ n›
    done

/-
'power2to_lg_n_le_n' depends on axioms: [propext, Classical.choice, Quot.sound]
-/
#print axioms power2to_lg_n_le_n

どうやら Nat.log2 の定義により排中律やらを利用しているかたちになっているようです。

こちらも証明中に利用した各種定理を説明します。

cov_recursion: さきほど証明した累積帰納法です。
Nat.succ_ne_zero: $n+1 \neq 0$ (なにかの後者であるならばゼロではない)
Nat.bitwise_rec_lemma: $\lfloor \frac n 2 \rfloor \le n$
Nat.le_add_left: $n \le m + n$
Nat.div_pos (Mathlib4): $0 < b \le a \to 0 < \lfloor \frac a b \rfloor$
Nat.mul_le_mul_left (Mathlib4): $n < m \to kn \le km$
d_mul_pow_d_to_k_eq_d_to_pow_succ_k: $d \cdot d^k = d^{k+1}$
d_mul_n_div_d_le_d: $n \lfloor{ \frac m n }\rfloor \le m$

上記で利用している2つの定理の証明は以下です。

-- d * d^k = d^(k+1)
theorem d_mul_pow_d_to_k_eq_d_to_pow_succ_k (d k : Nat) : d * d^k = d^(k+1) := by
  match k with
  | 0 => simp
  | k+1 =>
    rw [Nat.mul_comm]
    rfl

/-
'd_mul_pow_d_to_k_eq_d_to_pow_succ_k' depends on axioms: [propext]
-/
#print axioms d_mul_pow_d_to_k_eq_d_to_pow_succ_k

-- d*n/d ≤ d
theorem d_mul_n_div_d_le_d (m n : Nat) : n * (m / n) ≤ m := by
  have h1 : n * (m / n) + m % n = m := Nat.div_add_mod _ _
  have h2 : n * (m / n) ≤ n * (m / n) + m % n := Nat.le_add_right ..
  calc
    n * (m / n) ≤ n * (m / n) + m % n := h2
    _ = m := h1

/-
'd_mul_n_div_d_le_d' depends on axioms: [propext]
-/
#print axioms d_mul_n_div_d_le_d

Nat.mul_comm: 可換則 $nm = mn$
Nat.div_add_mod: 整数除算 (商と剰余) n * (m / n) + m % n = m
Nat.le_add_right: $n \le n + k$

感想

いままで Coq や Lean4 をなんとなく表面だけ触って「なるほどねー(?)」と言ってましたが、初めてまともに目的を持って定理証明をしてみました。大変でした。
とにかく、当たり前のことを言うための定理を探してくるのが大変でした。また、Mathlib4 のインポートを絞ろうとしたときに、最初に Mathlib.RingTheory.Localization.FractionRing みたいな大きめのものをインポートしていると、何に依存しているのか特定するのが大変でした。とはいえ、今回はこの大きめのライブラリに依存するのも変だったため、ちょうどよい小ささの依存を探す必要がありました。最終的には以下で落ち着きました。

import Mathlib.Data.Nat.Basic
import Mathlib.Tactic.Common

なお、当初の目的は IEEE754 2019 の形式化と諸性質の証明をするつもりでした。すべての関数を揃えた形式化には実数の利用が必要ですが、四則演算ぐらいであれば有理数があれば十分だろうと思っています。
上の定理は、有理数から、それに最も近い IEEE754 representation を算出するアルゴリズムの性質を示すのに必要だったために用意しました。そちらの続きはまた今度やろうかなと思います。当分やらないかもです。冬休みも終わったので。

また、今回これを証明するに当たり、軽く探してみた感じここにある定理は Lean4 や Mathlib4 の中に入っていないのではないかなと思うので、取りこんでもらう提案をしてみるのも良いかなと思っています。

追記

Zulipで聞いたらNat.strongInductionOn としてすでにあるということでした。

脚注

コンピュータは数学者になれるのか? -数学基礎論から証明とプログラムの理論へ- 2015 照井一成 (著) ↩︎ ↩︎
$\mathrm{PA}$ はペアノ算術 (ペアノの公理のWikipedia(英語)も参照) ↩︎
任意の整列順序上の帰納法（超限帰納法）はその累積版と等価な規則であることが証明できる。「コンピュータは数学者になれるのか?^[1:1]」にて紹介されています ↩︎
実際の Nat.rec は宇宙に対する量化が入っています。 #check @Nat.rec.{0} : NatInd が通ることが確認できます ↩︎
私は最初 $P(0) \to {}^{\forall n}({}^{\forall k < n}P(k) \to P(n)) \to {}^{\forall n}P(n)$ で定義していたのですが、手前の前提は必要がないというのを実際にLean4で証明を書きながら、Unused Variables(未使用変数)と警告されたタイミングで気づきました。不必要な前提がUnused Variableとして警告されるのもメリットかもしれませんね。(必ず警告してくれるわけではなく、それが不必要で、実際に使わずに証明した場合のみ) ↩︎
そして、このような簡単な性質すら、それを証明するか、定理を探し出す必要があり、これが現代の証明支援系のつらいところで、未成熟なところでもあります。（といっても、それらはタクティクスなどで部分的に解決されていたりもするので、私がまだLean4を使いこなせていない部分もあります。とはいえ、現代の証明支援系全般が紙とペンと同等の感覚には至っていないのも事実かなとお見おます） ↩︎
さらに言えばこの定理をサクッと利用して別のことを証明したくて始めたことだが、思ったよりはるかに証明の形式化は大変だった ↩︎
数論や数学基礎論を色々と見ていると、実数を経由した自然数上の演算のほうがよほど遠回りに感じられてきます。整数除算とは、商と剰余を一意に出す操作であり、そのうち商のみを参照するのが n / m にすぎないのだ、みたいな気分になれます。 ↩︎

Discussion