Lean4で累積帰納法を証明する
ライセンス
この記事上のコードはすべて CC0 (パブリックドメイン) で公開します。
この記事のコードは以下でも公開しています。
Lean4とは
Lean4は関数型プログラミング言語のように使える証明支援系です。証明支援系では数学で行われる「証明」を形式化して展開することができます。
注意
この記事では自然数 (
数学的帰納法
数学的帰納法について振り返ります。
ある自然数に関する命題
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番目の例は
受験数学までによく見かける数学的帰納法の用途は、4番目以降の例のような、一般項を求める問題などではないでしょうか。
さて、すべての
すべての、というのはつまり、
数学的帰納法とは次のようなスキームの証明方法です。
- 任意の
についてn を証明しますP(n) - 初期:
のときを証明しますn=0 - 帰納:
のとき、n=k+1 では成り立つと仮定して、k で成り立つことを証明しますn
これは先程の一般化した述語
- 初期:
を証明しますP(0) - 帰納: 任意の
に付いてk \in \N が成り立つと仮定するとP(k) が成り立つことを証明しますP(k+1)
帰納ケースは記号記号を使えば
この2つを証明することにより、任意の
-
: 初期ケースによって証明されている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パターンの場合分けによって、任意の自然数についての証明を、
-
を証明するとき: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)
(↑ここでは記号
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)とは、数学的帰納法の亜種のようなもので、
先程見たように、
-
を証明するとき:P(100) の順で証明を得られるP(0) \to P(1) \to P(2) \to \cdots \to P(99) \to P(100)
とう順番で証明されるわけですから、
実際、
数学的な感覚では2つの論法が等価であることは上記の説明で通じるのですが、Lean4ではきちんと証明しなければなりません。この2つの間の関係を見ていきましょう。まずは論理式として定式化してみます。
数学的帰納法
Lean4での定義は以下のようになります[4]。
def NatInd := ∀P : Nat → Prop, (P 0 → (∀k, P k → P (k+1)) → ∀n, P n)
累積帰納法
Lean4での定義は以下のようになります。
def NatCompleteInd := ∀P : Nat → Prop, ((∀n, (∀k < n, P k) → P n) → ∀n, P n)
ここで、累積帰納法に初期ケースが存在しないように思うかもしれませんが、
累積帰納法を構成的に証明してみる
いきなりLean4の証明に取り掛かる前に、まずは方針を立てます。さて、先程の説明のとおり、数学的帰納法と累積帰納法は多少方法が異なるだけで同じことをしています。逆に数学的帰納法をもたない体系は本質的により弱いもになります。
ということは、数学的帰納法をどこかで使う必要はあるだろうな、という考察ができます。
これを証明しようとしてみるとわかりますが、かなり混乱します。(私だけかもしれないですが)
しかし、混乱を整理しながら証明を構築できて、誤った論法を許さないのもLean4のような証明支援系の利点と言えますね。
以下では試行錯誤の末にLean4で作成した証明を翻訳してみます。
証明:
累積帰納法で示したい述語を
まず、元の累積帰納法の仮定に
さて、ここから数学的帰納法を適用することから考えます。そのための
とそのまま設定すればよいです。
初期:
帰納:
明らかに帰納法の前提を使えば
しかし、帰納法の仮定より
***
さて、あえて日本語で書いた構成的な証明は上記のようになるわけですが、とにかく混乱するポイントが多いような気がしますね...とにかく、各変数のスコープがわかりにくいように思えます。
最終的に完成した 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 の証明
使用例: なお、
なお、ここでは
例:
\lg 1 = \lg 1_{(2)} = 0 \lg 10 = \lg 1010_{(2)} = 3 \lg 100 = \lg 1100100_{(2)} = 6
なお、二進表記の場合は
一方で、
なので、4列目
まずは方針を考えます。
さて、
そして、これと同じ定義がすでにLean4組み込みのInit/Data/Nat/Log2.leanにあります。
def log2 (n : @& Nat) : Nat :=
if n ≥ 2 then log2 (n / 2) + 1 else 0
なお、自然数同士の割り算 n / m
は、そのまま自然数上で切り捨てられた値 (n // m
やC/Rust の整数除算 n / m
に近いです。[8]
全域関数にするために log2 0 = 0
として定義されていますが、本質ではないので気にしなくて問題ないです。
なお、同ファイル の中で、より弱い定理 Nat.log2 n ≤ 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 としてすでにあるということでした。
-
はペアノ算術 (ペアノの公理のWikipedia(英語)も参照) ↩︎\mathrm{PA} -
任意の整列順序上の帰納法(超限帰納法)はその累積版と等価な規則であることが証明できる。「コンピュータは数学者になれるのか?[1:1]」にて紹介されています ↩︎
-
実際の
Nat.rec
は宇宙に対する量化が入っています。#check @Nat.rec.{0} : NatInd
が通ることが確認できます ↩︎ -
私は最初
で定義していたのですが、手前の前提は必要がないというのを実際にLean4で証明を書きながら、Unused Variables(未使用変数)と警告されたタイミングで気づきました。不必要な前提がUnused Variableとして警告されるのもメリットかもしれませんね。(必ず警告してくれるわけではなく、それが不必要で、実際に使わずに証明した場合のみ) ↩︎P(0) \to {}^{\forall n}({}^{\forall k < n}P(k) \to P(n)) \to {}^{\forall n}P(n) -
そして、このような簡単な性質すら、それを証明するか、定理を探し出す必要があり、これが現代の証明支援系のつらいところで、未成熟なところでもあります。(といっても、それらはタクティクスなどで部分的に解決されていたりもするので、私がまだLean4を使いこなせていない部分もあります。とはいえ、現代の証明支援系全般が紙とペンと同等の感覚には至っていないのも事実かなとお見おます) ↩︎
-
さらに言えばこの定理をサクッと利用して別のことを証明したくて始めたことだが、思ったよりはるかに証明の形式化は大変だった ↩︎
-
数論や数学基礎論を色々と見ていると、実数を経由した自然数上の演算のほうがよほど遠回りに感じられてきます。整数除算とは、商と剰余を一意に出す操作であり、そのうち商のみを参照するのが
n / m
にすぎないのだ、みたいな気分になれます。 ↩︎
Discussion