/-!
# 第23章：自然数の再帰・場合分け・帰納法

自然数は無限にありますが、各自然数は零から有限回の後者操作で作られます。この生成の仕方を
利用すれば、無限個の値についての主張を、基底部と一つの帰納段階へ圧縮できます。同じ構成子に
沿って値を作るときは再帰、命題の証明を作るときは帰納法になります。

本章では場合分け・構造再帰・数学的帰納法を、同じ `Nat` の除去原理が異なる目的へ特殊化した
ものとして比較します。帰納仮定が必要な証明と不要な証明を見分け、後に整礎帰納法、帰納族、
初代数、最小不動点へ一般化できる形で整理します。

## 零と後継者が全自然数を尽くす

自然数は `0` と後者操作 `S(n)` から生成されます。述語 `P` について

$$
\frac{p_0:P(0)\qquad p_S:\prod_{n:\mathbb N}P(n)\to P(S(n))}
     {\mathsf{ind}_{\mathbb N}(p_0,p_S):\prod_{n:\mathbb N}P(n)}.
$$

計算規則は、零では基底証明を返し、後者では直前までの帰納結果を段階へ渡します。

$$
\mathsf{ind}_{\mathbb N}(p_0,p_S,0)\equiv p_0,
\qquad
\mathsf{ind}_{\mathbb N}(p_0,p_S,S(n))
\equiv p_S(n,\mathsf{ind}_{\mathbb N}(p_0,p_S,n)).
$$

を帰納原理とします。したがって `∀ n, P n` を示すには、

1. **基底部**：`P 0`
2. **帰納段階**：任意の `n` について `P n → P (Nat.succ n)`

を与えます。帰納段階で受け取る `P n` が帰納仮定です。場合分け `cases` は各構成子を
調べるだけで、部分構造についての仮定を受け取りません。

帰納法は「小さい数をいくつか試したので一般化する」推測ではありません。自然数が
`0` と `succ` だけから有限回で作られるという生成原理に対応する除去規則です。証明する
述語 `P : Nat → Prop` を固定し、二つの構成方法のどちらで作られた値にも `P` が保存
されることを示すため、すべての自然数を覆えます。


-/

namespace FormalLab.Mathematics.NaturalNumberInduction

/-!
## 帰納法で全ての自然数について証明する

Leanで `induction n` を実行すると、目標 `P n` から `P 0` と
`∀ n, P n → P (n + 1)` に対応する二つの目標が生成されます。`zeroAdd` では
`P n` が `0 + n = n` です。帰納仮定は一般の等式ではなく、直前の `n` における
ちょうど `0 + n = n` です。
-/

/-- `0 + n = n` を `n` の構成に沿って証明します。 -/
theorem zeroAdd (n : Nat) : 0 + n = n := by
  induction n with
  | zero => rfl
  | succ n inductionHypothesis =>
      change Nat.succ (0 + n) = Nat.succ n
      exact congrArg Nat.succ inductionHypothesis

/-- 同じ帰納証明を、生成された再帰子へ基底部と帰納段階を直接渡して構成します。 -/
theorem zeroAddByRecursor : ∀ n : Nat, 0 + n = n :=
  Nat.rec rfl (fun _ inductionHypothesis => congrArg Nat.succ inductionHypothesis)

/-!
`zeroAddByRecursor` はtactic状態を介さず、上の $p_0$ に `rfl`、$p_S$ に後者への合同写像を
そのまま渡します。`zeroAdd` と結論は同じですが、一方は対話的に生成された証明項、他方は除去子へ
明示的に与えた証明項です。帰納法が追加のメタ推論ではなく `Nat.rec` の依存する使用だと確認できます。

後者の場合を計算すると、目標は `succ (0 + n) = succ n` になります。帰納仮定そのものは
`0 + n = n` なので、両辺へ同じ構成子 `Nat.succ` を適用する合同性により目標を得ます。
ここでは「帰納法を使えば自動的に解ける」のではなく、帰納仮定を現在の目標へ運ぶ一手が
必要です。

対照的に、`n + 0 = n` は加算が第二引数を再帰して定義されているため計算だけで閉じます。
数学的には左右とも単位元の法則でも、定義の向きによってLeanで必要な証明は異なります。
-/

theorem addZeroByComputation (n : Nat) : n + 0 = n :=
  rfl

/-! ## 同じ構成子に沿って値を計算する -/

/-- `0 + 1 + ... + n` を再帰的に計算します。 -/
def sumTo : Nat → Nat
  | 0 => 0
  | n + 1 => sumTo n + (n + 1)

/-- 後者入力に対する計算規則は定義展開だけで成立します。 -/
theorem sumToSucc (n : Nat) : sumTo (n + 1) = sumTo n + (n + 1) :=
  rfl

example : sumTo 3 = 6 :=
  rfl

/-!
再帰と帰納法は同じ構成子分解に基づきますが、目的が違います。`sumTo` は各自然数から
新しい値を**計算**し、`zeroAdd` は各自然数について命題の証明を**構成**します。
Leanの型理論では後者も依存する再帰として統一的に表せますが、学習時には「返すものが値か
証明か」をまず区別すると見通しがよくなります。
-/

/-! ## 一段の観察だけなら場合分けする -/

/-- 自然数は `0` か、ある自然数の後者です。 -/
theorem zeroOrSuccessor (n : Nat) : n = 0 ∨ ∃ k, n = k + 1 := by
  cases n with
  | zero => exact Or.inl rfl
  | succ k => exact Or.inr ⟨k, rfl⟩

/-!
この定理は `n` の一段目の形だけを知れば十分です。後者の場合に、内部の `k` について
同じ命題が成立するという情報は使いません。したがって `induction` ではなく `cases` が
証明に必要な情報の流れに正確に対応します。帰納仮定を使わない帰納法は、しばしば場合分けで
十分だという合図です。
-/

#eval sumTo 10

/-!
## 再帰・場合分け・帰納法の使い分け

`sumTo` は値を返す再帰定義、`zeroAdd` は命題の証明です。`sumToSucc` は計算だけで
`rfl` が使えますが、`zeroAdd` は加算の再帰する引数の向きのため帰納法が必要です。
構造的でない再帰や整礎帰納法は、減少関係を導入した後に扱います。

## 要点

* 場合分けは値の最外構成子だけを調べ、帰納法は部分構造についての仮定も受け取る。
* 再帰は構成子に沿って値を作り、帰納法は構成子に沿って依存する命題を証明する。
* 基底部は最小構成子、帰納段階は帰納仮定から次の構成子の場合を作る。
* `rfl` で閉じるか帰納法が要るかは、数学的対称性だけでなく定義の再帰方向にも依存する。

## 研究史と文献案内

Dedekindの1888年の単純無限系 [DED88] とPeanoの1889年の算術体系 [PEA89] は、
自然数公理化・帰納原理の重要な原典です。ただし、両者の基礎理論と記法は異なります。Martin-Löf
型理論では自然数の導入・除去・等式規則が一つの型の意味説明をなします [ML84]。Leanの
`Nat.rec` はLean固有の帰納型宣言から生成される除去子です [LEAN-REF]。

## 問題

### 帰納法の四つの役割を分離する

`zeroAdd` で証明している述語を `P n := ...` の形で書き、基底部、帰納仮定、帰納段階、
最終的な全称命題を区別せよ。Leanの `Nat.rec` または帰納法タクティックの各引数が、この
数式による構成のどこに対応するかを表にする。

続いて `n + 0 = n` と `0 + n = n` を証明し、片方が定義計算で閉じ、もう片方が帰納法を
要する理由を加算の再帰引数から説明せよ。式の左右対称性だけでは証明方法まで対称にならない
ことを確認できれば完了である。

### 再帰計算と帰納証明を同じ構造から読む

`sumTo 3` を定義に従って一段ずつ展開する。その後、
`sumTo (n + 1) = sumTo n + (n + 1)` をまず定義展開だけで証明し、どの式が判断的に簡約され、
どの式が命題的等式として残るかを記録せよ。

`zeroOrSuccessor` ではなぜ帰納仮定を使わないのかも説明する。構造を一段観察する場合分けと、
小さい対象について得た命題を次へ運ぶ帰納法との違いを、Leanコードと推論規則による導出の両方から
述べること。

### 別の帰納型へ原理を移す

要素型 `α` をもつ自作のリスト型を定義し、長さ関数を構造再帰で実装せよ。さらに、連結した
二つのリストの長さが長さの和になることを構造帰納法で証明する。再帰関数の各分岐と帰納証明の
各分岐を一対一に対応づけること。

自然数で学んだ構成のうち、`0` と後者関数に固有だった部分と、任意の帰納型にも通用する部分を
分けて説明できれば、この問題の到達点に達している。
-/

end FormalLab.Mathematics.NaturalNumberInduction