Mathmatics In Lean4の第5章 初等数論の２つ目の話題は帰納法と再帰です。自然数では定義が帰納的であること（自然数型は帰納型であること）を知ります。
inductive Nat
| zero : Nat
| succ (n : Nat) : Nat
この意味は、0はNat型、Nat型の要素を１つとってnとするとsucc nもNat型です。そしてsucc n=0となるようなnはありません。ちなみにsucc nはn+1とも書かれます。
次にこの型の上で階乗関数を再帰的に定義します。
def fac : ℕ → ℕ
| 0 => 1
| n + 1 => (n + 1) * fac n
そして階乗関数について幾つかの性質を証明します。
fac 0 = 1 "0の階乗は1"
fac (n+1) = (n+1)*fac n "n+1の階乗はnの階乗にn+1をかけたものと等しい"
theorem fac_pos (n:Nat) : 0 < fac n := by ... 階乗の値は正である。
theorem dvd_fac {i n : ℕ} (ipos : 0 < i) (ile : i ≤ n) : i ∣ fac n := by ...
nの階乗は1以上n以下の全ての自然数で割り切れる。
ここで数学的帰納法が登場し、それに対応するinduction'タクティクが紹介されます。とは言ってもあまり難しいものではありません。全ての自然数について成り立つ時ことを証明する際に、induction'タクティクを使うと、証明が２つに分かれて、0で成り立つことの証明とnで成り立つことを仮定してn+1でも成り立つことを証明します。0 < fac nの証明ではinduction'タクティクが必要になります。
ここまでの話のまとめの意味を込めて階乗関数の下からの評価 2 ^ (n - 1) ≤ fac nを証明します。まさにinduction'タクティクを使えばごく自然に証明は終了できます。
帰納法と再帰の後半の話題は有限集合です。ここではn以下の自然数を有限集合として取り上げて、その全ての要素にわたる総和や総積が導入されます。例えば
theorem sum_id (n : ℕ) : ∑ i in range (n + 1), i = n * (n + 1) / 2 := by ...
これは$\sum_{i=0}^n i = \frac{n\,(n+1)}{2}$という総和の式です。
と読み進んできて、「あれ！これ！」と気がつきました。この道具があれば任意桁数の場合の３の倍数の確認方法を形式化して証明できそうです。
というわけで次回はその話を書くことにしましょう。
