概要

定理証明支援系のLeanにおいて、自然数は帰納型によって定義されています。この定義と、帰納型の除去則である帰納法を用いた自然数の基本的な性質についてまとめます。

環境構築

以下に従い、VS Codeの拡張機能を利用してLeanをインストールしてください。

ライブラリ内の定義と重複しないように適当なnamespaceを用意しその中に定義や定理を記述していきます。

namespace Example

end Example

定義や定理名は基本的に以下のソースコードに従っていますが、証明は個人的な分かりやすさのため書き換えている箇所があります。

https://github.com/leanprover/lean4/blob/master/src/Init/Prelude.lean
https://github.com/leanprover/lean4/blob/master/src/Init/Core.lean
https://github.com/leanprover/lean4/blob/master/src/Init/Data/Nat/Basic.lean

自然数

定義

/-! # Nat definition -/

inductive Nat where
  | zero : Nat
  | succ (n : Nat) : Nat

自然数は帰納型によって定義されています。帰納型は、各コンストラクタによって構築された項全てからなります。

自然数の場合、1つの項zero : Natと、既に構築された項n : Natを引数としてNatを返す関数succによって作られる項からなります。zeroから始めてsuccを繰り返し適用することで、zero (= 0), succ (zero) (= 1), succ (succ (zero)) (= 2), ...と無限に項を作ることができます。

加法

定義

/-! # Nat.add definition -/

def Nat.add : Nat → Nat → Nat
  | n, Nat.zero => n
  | n, Nat.succ m => Nat.succ (Nat.add n m)

自然数の加法も帰納的に定義されています。自然数n, mを受け取ったときに和を返す関数を、nを固定してmに関して帰納的に定義します。すなわち、まずn + 0を定義し、次にn + mの定義を仮定した上でn + succ mを定義します。

性質

/-! # Nat.add theorems -/

/-- ```n + 0 = n``` -/
theorem Nat.add_zero (n : Nat) : Nat.add n Nat.zero = n :=
  rfl

/-- ```n + (succ m) = succ (n + m)``` -/
theorem Nat.add_succ (n m : Nat) : Nat.add n (Nat.succ m) = Nat.succ (Nat.add n m) :=
  rfl

n + 0 = nとn + succ m = succ (n + m)は加法の定義から直ちに成り立ちます。

/--
```0 + n = n```
nについての帰納法で示す。
```
0 + n = n             -- 仮定
succ (0 + n) = succ n -- 両辺に`succ`を適用
0 + succ n = succ n   -- `Nat.add`の定義を適用
```
-/
theorem Nat.zero_add : ∀ (n : Nat), Nat.add Nat.zero n = n
  | Nat.zero => rfl
  | Nat.succ n => congrArg Nat.succ (Nat.zero_add n)

/--
```(succ n) + m = succ (n + m)```
mについての帰納法で示す。
```
succ n + m = succ (n + m)               -- 仮定
succ (succ n + m) = succ (succ (n + m)) -- 両辺に`succ`を適用
succ n + succ m = succ (n + succ m)     -- `Nat.add`の定義を適用
```
-/
theorem Nat.succ_add : ∀ (n m : Nat), Nat.add (Nat.succ n) m = Nat.succ (Nat.add n m)
  | _, Nat.zero => rfl
  | n, Nat.succ m => congrArg Nat.succ (Nat.succ_add n m)

0 + n　 = nや(succ n) + m = succ (n + m)の証明には帰納法が必要です。それぞれn, mによる帰納法と加法の定義によって示すことができます。

/--
```(n + m) + k = n + (m + k) ```
kについての帰納法で示す。
```
(n + m) + k = n + (m + k)              -- 仮定
succ ((n + m) + k) = succ(n + (m + k)) -- 両辺に`succ`を適用
(n + m) + succ k = n + (m + succ k)    -- `Nat.add`の定義を適用
```
-/
theorem Nat.add_assoc : ∀ (n m k : Nat), Nat.add (Nat.add n m) k = Nat.add n (Nat.add m k)
  | _, _, Nat.zero => rfl
  | n, m, Nat.succ k => congrArg Nat.succ (Nat.add_assoc n m k)

/--
```n + m = m + n ```
mについての帰納法で示す。
-/
theorem Nat.add_comm : ∀ (n m : Nat), Nat.add n m = Nat.add m n
  | n, Nat.zero => Eq.symm (Nat.zero_add n)
  | n, Nat.succ m => by
    rw [Nat.add_succ, Nat.succ_add, Nat.add_comm n m]

結合法則、交換法則も同様に帰納法によって示されます。Eq.symmは、等号の対称律です。

乗法

定義

/-! # Nat.mul definition -/

def Nat.mul : Nat → Nat → Nat
  | _, Nat.zero => Nat.zero
  | n, Nat.succ m => Nat.add (Nat.mul n m) n

加法の定義を利用して、乗法も帰納的に定義されています。

性質

/-! # Nat.mul theorems -/

/-- ```n * 0 = 0``` -/
theorem Nat.mul_zero (n : Nat) : Nat.mul n Nat.zero = Nat.zero :=
  rfl

/-- ```n * succ m = n * m + n``` -/
theorem Nat.mul_succ (n m : Nat) : Nat.mul n (Nat.succ m) = Nat.add (Nat.mul n m) n :=
  rfl

加法の場合と同様に、これらは乗法の定義から直ちに成り立ちます。

/-- ```0 * n = 0``` -/
theorem Nat.zero_mul : ∀ (n : Nat), Nat.mul Nat.zero n = Nat.zero
  | Nat.zero => rfl
  | Nat.succ n => by
    rw [Nat.mul_succ, Nat.add_zero, Nat.zero_mul n]

/-- ```(succ n) * m = n * m + m``` -/
theorem Nat.succ_mul : ∀ (n m : Nat), Nat.mul (Nat.succ n) m = Nat.add (Nat.mul n m) m
  | n, Nat.zero => by
    rw [Nat.mul_zero, Nat.add_zero, Nat.mul_zero]
  | n, Nat.succ m => by
    rw [Nat.mul_succ, Nat.add_succ, Nat.succ_mul n m, Nat.mul_succ, Nat.add_succ]
    rw [Nat.add_assoc, Nat.add_comm m n, ← Nat.add_assoc]

0 * n = 0や(succ n) * m = n * m + mの証明は加法の場合と同様に、帰納法が必要です。

/-- ```n * m = m * n``` -/
theorem Nat.mul_comm : ∀ (n m : Nat), Nat.mul n m = Nat.mul m n
  | n, Nat.zero => Eq.symm (Nat.zero_mul n)
  | n, Nat.succ m => by
    rw [Nat.mul_succ, Nat.succ_mul, Nat.mul_comm n m]

/-- ```n * (m + k) = n * m + n * k``` -/
theorem Nat.mul_add : ∀ (n m k : Nat), Nat.mul n (Nat.add m k) = Nat.add (Nat.mul n m) (Nat.mul n k)
  | Nat.zero, _, _ => by
    repeat rw [Nat.zero_mul]
    rw [Nat.add_zero]
  | Nat.succ n, m, k => by
    rw [Nat.succ_mul, Nat.mul_add n m k, Nat.succ_mul, Nat.succ_mul]
    rw [Nat.add_assoc, ← Nat.add_assoc (Nat.mul n k), Nat.add_comm (Nat.mul n k), Nat.add_assoc, ← Nat.add_assoc]

/-- ```(n + m) * k = n * k + m * k``` -/
theorem Nat.add_mul (n m k : Nat) : Nat.mul (Nat.add n m) k = Nat.add (Nat.mul n k) (Nat.mul m k) := by
  rw [Nat.mul_comm (Nat.add n m) k, Nat.mul_comm n k, Nat.mul_comm m k, Nat.mul_add k n m]

/-- ```(n * m) * k = n * (m * k)``` -/
theorem Nat.mul_assoc : ∀ (n m k : Nat), Nat.mul (Nat.mul n m) k = Nat.mul n (Nat.mul m k)
  | _, _, Nat.zero => rfl
  | n, m, Nat.succ k => by
    rw [Nat.mul_succ, Nat.mul_succ, Nat.mul_add, Nat.mul_assoc]

/-- ```n * 1 = n``` -/
theorem Nat.mul_one : ∀ (n : Nat), Nat.mul n (Nat.succ Nat.zero) = n :=
  Nat.zero_add

/-- ```1 * n = n``` -/
theorem Nat.one_mul (n : Nat) : Nat.mul (Nat.succ Nat.zero) n = n := by
  rw [Nat.mul_comm, Nat.mul_one]

交換法則、結合法則に加えて、分配法則、1との積に関しても証明していきます。

前者関数(predecessor)

定義

/-! # Nat.pred definition -/

def Nat.pred : Nat → Nat
  | Nat.zero => Nat.zero
  | Nat.succ n => n

次の数を返すsucccessorの反対の関数であるpredecessorも帰納的に定義できます。
自然数は０以上ですので、pred　(zero)はzeroと定義することに注意します。

性質

/-! # Nat.pred theorems -/

/-- ```pred 0 = 0``` -/
theorem Nat.pred_zero : Nat.pred Nat.zero = Nat.zero :=
  rfl

/-- ```pred (succ n) = n``` -/
theorem Nat.pred_succ (n : Nat) : Nat.pred (Nat.succ n) = n :=
  rfl

定義から直ちに成り立つ性質です。

/-- ```n ≠ 0 → succ (pred n) = n``` -/
theorem Nat.succ_pred : ∀ (n : Nat), n ≠ Nat.zero → Nat.succ (Nat.pred n) = n
  | Nat.zero => fun h => False.elim (h rfl)
  | Nat.succ _ => fun _ => rfl

succ (pred n) = nには、n ≠ 0の仮定が必要です。n = 0の場合の証明に関しては、n ≠ 0がn = 0 → Falseを意味するので、仮定によってFalseが導かれ、Falseの除去則によって任意の命題が真となります。

切り捨て減法

定義

/-! # Nat.sub definition -/

def Nat.sub : Nat → Nat → Nat
  | n, Nat.zero => n
  | n, Nat.succ m => Nat.pred (Nat.sub n m)

減法も定義できますが、ここでは自然数の範囲で考えているので、n < mのときはn - m = 0と定義することに注意します。上で定義した前者関数を使うことで帰納的に定義することができます。

性質

/-! # Nat.sub theorems -/

/-- ```n - 0 = n``` -/
theorem Nat.sub_zero (n : Nat) : Nat.sub n Nat.zero = n :=
  rfl

/-- ```n - (succ m) = pred (n - m)``` -/
theorem Nat.sub_succ (n m : Nat) : Nat.sub n (Nat.succ m) = Nat.pred (Nat.sub n m) :=
  rfl

定義から直ちに成り立つ性質です。

/-- ```succ n - succ m = n - m``` -/
theorem Nat.succ_sub_succ : ∀ (n m : Nat), Nat.sub (Nat.succ n) (Nat.succ m) = Nat.sub n m
  | _, Nat.zero => rfl
  | n, Nat.succ m => congrArg Nat.pred (Nat.succ_sub_succ n m)

/-- ```n - n = 0``` -/
theorem Nat.sub_self : ∀ (n : Nat), Nat.sub n n = Nat.zero
  | Nat.zero => rfl
  | Nat.succ n => by
    rw [Nat.succ_sub_succ, Nat.sub_self n]

/-- ```(n + m) - n = m``` -/
theorem Nat.add_sub_self_left : ∀ (n m : Nat), Nat.sub (Nat.add n m) n = m
  | Nat.zero, _ => by
    rw [Nat.zero_add, Nat.sub_zero]
  | Nat.succ n, m => by
    rw [Nat.succ_add, Nat.succ_sub_succ, Nat.add_sub_self_left n m]

/-- ```(n + m) - m = n``` -/
theorem Nat.add_sub_self_right (n m : Nat) : Nat.sub (Nat.add n m) m = n := by
  rw [Nat.add_comm, Nat.add_sub_self_left m n]

/-- ```n - (m + k) = (n - m) - k``` -/
theorem Nat.sub_add_eq : ∀ (n m k : Nat), Nat.sub n (Nat.add m k) = Nat.sub (Nat.sub n m) k
  | _, _, Nat.zero => by
    rw [Nat.add_zero, Nat.sub_zero]
  | n, m, Nat.succ k => by
    rw [Nat.add_succ, Nat.sub_succ, Nat.sub_add_eq n m k, Nat.sub_succ]

減法に関する性質です。切り捨ての場合も含めて上手く証明されていますね。

べき乗

/-! # Nat.pow definition -/

def Nat.pow : Nat → Nat → Nat
  | _, Nat.zero => Nat.succ Nat.zero
  | n, Nat.succ m => Nat.mul (Nat.pow n m) n

最後に、べき乗に関しても触れておきます。べき乗は乗法を用いて帰納的に定義されます。

/-! # Nat.pow theorems -/

/-- ```n ^ 0 = 1``` -/
theorem Nat.pow_zero (n : Nat) : Nat.pow n Nat.zero = Nat.succ Nat.zero :=
  rfl

/-- ```n ^ (succ m) = (n ^ m) * n``` -/
theorem Nat.pow_succ (n m : Nat) : Nat.pow n (Nat.succ m) = Nat.mul (Nat.pow n m) n :=
  rfl

定義から直ちに成り立つ性質です。

まとめ

自然数に関する様々な性質が、シンプルな帰納法によって見事に示されるのは驚きですね。公式のソースコードには他にも様々な性質が定理として示されているので眺めてみると面白いです。

実は、一見全く異なるような存在量化子やリスト型も同様に帰納型によって定義されています。これらの性質や、この記事で触れられなかった自然数の等号や不等号の定義についてもいずれ扱えればと思います。

参考文献