/-!
# 第3章：帰納型・場合分け・再帰・構造体

真偽値には二つの値があり、自然数には零と後者という生成法があります。値を列挙するだけでは
自然数のような無限の型を定義できませんが、値を作る有限個の規則なら記述できます。さらに、
作り方を完全に列挙できれば、値を使う側が処理すべき場合もそこから決まります。

本章では、構成子による生成、場合分け、構造再帰を一つの原理として学びます。有限型と再帰的な
型を比較し、構造体も「名前付きフィールドを持つ一構成子の帰納型」として位置づけます。この
見方は後の帰納法だけでなく、構文木、証明、添字付き帰納族、初代数へつながります。

## 値を構成子から有限に生成する

帰納的に定義された対象は構成子によって生成されます。これは「既知の値を列挙する」という意味ではなく、
**有限回の構成子適用で得られる値だけを認める**という定義です。値を使うときは各構成子を
処理します。再帰的な構成子があれば、直前の小さい値に対する結果を利用できます。

## 帰納的定義から生じる四種類の規則

帰納型の宣言からは、少なくとも四種類の情報が生まれます。

1. **形成規則**：その型がどの宇宙に属するか。
2. **導入規則**：構成子を使って値をどう作るか。
3. **除去規則**：全構成子を処理して値をどう使うか。
4. **計算規則**：構成子へ除去規則を適用したとき何へ簡約するか。

たとえば二値型なら、二つの構成子が導入規則であり、二分岐の場合分けが除去規則です。
入力が第一構成子なら第一分岐へ計算されます。構文を覚えるより、この四点を同じ宣言から
復元する方が、後の論理結合子や添字付き帰納族にも再利用できます。

二値型を $\mathsf{Switch}$ と書けば、形成・導入規則は

$$
\mathsf{Switch}:\mathsf{Type},
\qquad
\mathsf{off}:\mathsf{Switch},
\qquad
\mathsf{on}:\mathsf{Switch}
$$

です。値 $s$ に応じて結果の型も変わり得る族 $C:\mathsf{Switch}\to\mathsf{Sort}(u)$ に対する除去子は

$$
\mathsf{rec}_{\mathsf{Switch}}:
C(\mathsf{off})\to C(\mathsf{on})\to
\prod_{s:\mathsf{Switch}}C(s)
$$

という型を持ちます。計算規則は、第一の構成子では第一の分岐、第二の構成子では第二の分岐を選びます。

$$
\mathsf{rec}_{\mathsf{Switch}}(c_{\mathrm{off}},c_{\mathrm{on}},\mathsf{off})
\equiv c_{\mathrm{off}},
\qquad
\mathsf{rec}_{\mathsf{Switch}}(c_{\mathrm{off}},c_{\mathrm{on}},\mathsf{on})
\equiv c_{\mathrm{on}}.
$$

## 有限列挙と再帰的生成を区別する

`Switch` の値は二つだけですが、`Nat` は `zero` と `succ` という有限個の構成子から
無限個の値を生成します。「構成子が有限個」と「値が有限個」は別です。再帰的構成子が
自分と同じ型の小さい値を引数に取ることで、有限の規則から無限のデータが生まれます。


-/

namespace FormalLab.Foundation.InductiveTypes

/-! ## 二値型を構成し、全ての場合を処理する -/

/-- `off` と `on` の二構成子だけから生成される型です。 -/
inductive Switch where
  | off
  | on

/-- 入力の構成子を調べ、もう一方の構成子を返します。 -/
def toggle : Switch → Switch
  | .off => .on
  | .on => .off

#reduce toggle .off

/-!
`toggle` は二つの分岐を両方書かなければなりません。これは作り手が将来どの値を追加するかを
推測しているのではなく、`Switch` の値が二構成子からしか作れないという定義を使っています。
この性質が**網羅性**（exhaustiveness）です。
-/

/-- `Switch` を標準の真偽値へ解釈する。 -/
def Switch.toBool : Switch → Bool
  | .off => false
  | .on => true

#eval Switch.toBool .on

/-! ## 構造再帰 -/

/-- 自然数の構成に沿って定義した階乗です。 -/
def factorial : Nat → Nat
  | 0 => 1
  | n + 1 => (n + 1) * factorial n

/-- リストの構成に沿って定義した長さです。 -/
def listLength {α : Type} : List α → Nat
  | [] => 0
  | _ :: tail => listLength tail + 1

#eval factorial 5
#eval listLength [10, 20, 30]

/-!
再帰呼出し `factorial n` と `listLength tail` は、入力の直部分へ向かいます。Leanの
停止性検査がこの減少を確認するため、受理された構造再帰は有限時間で停止します。

場合分けと再帰の差は分岐数ではありません。場合分けは構成子の引数だけを受け取り、
再帰はそれに加えて再帰的部分へすでに関数を適用した結果を使います。`listLength` の
cons分岐では `tail` だけでなく `listLength tail` が利用できるため、リスト全体を畳み込めます。

`factorial` の `n + 1` は任意の加算式ではなく、自然数の後者構成子に一致するパターンです。
右辺の再帰呼出しはその直接の部分 `n` へ向かうので、停止性が構文から確認できます。

## 生成された再帰原理を観察する

パターンマッチは便利な表面構文ですが、kernelは帰納型ごとの再帰子を使う形へ精緻化します。
再帰子の型には「各構成子の場合を与えれば、任意の値について結果を作れる」という除去原理が
現れます。今は出力を暗記せず、構成子ごとの分岐が引数になっている箇所を探してください。
-/

#check Switch.rec
#check Nat.rec

/-!
`Switch.rec` の出力で `motive` は上の $C$、二つの分岐は $c_{\mathrm{off}}$ と $c_{\mathrm{on}}$ です。
自然数の再帰子では、後者分岐が直前の自然数 $n$ だけでなく、既に得た結果 $C(n)$ も受け取ります。

$$
\mathsf{rec}_{\mathsf{Nat}}:
C(0)\to
\left(\prod_{n:\mathsf{Nat}}C(n)\to C(n+1)\right)\to
\prod_{n:\mathsf{Nat}}C(n).
$$

この追加引数が、単なる零・後者の場合分けと構造再帰を分けます。$C(n)$ がデータの型なら再帰計算を、命題なら
帰納法を表します。同じ再帰子の値域をどのsortに選ぶかで用途が分かれます。

## 構造体は名前付きの一構成子

複数の成分を常に一緒に持つ型には `structure` を使えます。単純な構造体は、一つの
構成子と名前付き射影を持つ帰納型です。後に、データだけでなく演算と法則も束ねます。
-/

/-- 二つの整数成分を名前付きで束ねた構造体です。 -/
structure Point where
  x : Int
  y : Int

/-- 構造体は構文 `⟨...⟩` で作り、射影 `.x` で成分を使えます。 -/
def origin : Point :=
  ⟨0, 0⟩

#eval origin.x

/-!
`Point` の値を作るには `x` と `y` の両成分が必要で、使う側は射影によって各成分を
取り出せます。順序だけで区別する直積と違い、名前付き射影は各成分の役割を記録します。
-/

/-- 点を二方向へ平行移動する。 -/
def Point.translate (point : Point) (dx dy : Int) : Point :=
  ⟨point.x + dx, point.y + dy⟩

#eval (origin.translate 3 (-2)).y

/-!
## 帰納的定義が保証する範囲

場合分けは現在の値がどの構成子かだけを使います。再帰は部分構造について計算済みの
結果も使います。全ての値について命題を示す帰納法は、「自然数の帰納法・再帰」で導入します。
そこでは、場合分けと再帰との違いも同じ構成子から比較します。

構造体は「複数の値を束ねる構文」に留まりません。後には演算と、その演算が満たす法則を
同じ構造へ持たせます。ただし、構造体を定義しただけでは型クラス探索は起きません。
構造と自動探索の区別は「法則を持つ構造と型クラス探索」で扱います。

## 要点

帰納型は値の生成法を構成子で閉じ、その生成法から依存除去子と計算規則を得ます。値域をデータの型に
選べば場合分け・再帰、命題に選べば帰納法になります。
有限個の構成子から無限個の値を作れること、場合分けと再帰で利用できる情報が違うこと、
構造体が名前付き一構成子の帰納型であることが要点です。

## 研究史と文献案内

Dedekindは1888年に、自然数と再帰的定義を写像の言葉で基礎づけました [DED88]。Peanoは1889年に、
算術を記号的公理体系として提示しました [PEA89]。Martin-Löf型理論では形成・導入・除去・
等式規則が型の意味説明を構成します [ML84]。現代の帰納型と操作的意味論は [PFPL16]、
Lean固有の生成規則は [LEAN-REF] を参照してください。これらは同じ自然数体系の版違いでは
ありません。

## 問題

### 四種類の規則から有限データ型を設計する

三構成子 `red`、`yellow`、`green` を持つ `TrafficLight` を設計します。Leanコードを書く前に、形成規則、
三つの導入規則、全分岐による除去規則、各分岐の計算規則を数式で書いてください。その後で次の色を返す
`next` を実装し、三分岐が入力を尽くすことを構成子一覧から説明します。

`Switch` と `TrafficLight` の除去原理を比較し、構成子数が増えたときに何が変わり、何が同じ図式のままかを述べます。
検証は `next red = green`、`next green = yellow`、`next yellow = red` を計算で確かめるだけでなく、それぞれがどの計算規則の実例かを指します。

### 場合分けと構造再帰を呼出し関係で見分ける

`toggle` と `listLength` の定義を、分岐ごとに「構成子の引数」「再帰呼出し」「返り値」の三列で書き直してください。
`listLength` の再帰呼出しが元の入力ではなく直接の部分構造に対して行われることを、引数の構文から説明します。

次に、同じ入力をそのまま再帰呼出しする不正な長さ関数を試し、Leanの停止性診断を記録します。
エラー文の引用で終えず、どの再帰呼出しに対して構造的な減少を示せないかを入力木に印をつけて示してください。

### 帰納型の無限と余帰納的観察を混同しない

`Nat.rec` の型を転写し、基底値、帰納段階、入力自然数、出力の四成分を色分けします。次にそれらを `factorial`
の零分岐、後継者分岐、再帰結果、最終出力へ対応させ、再帰定義が除去原理の使用であることを説明してください。

自然数型が無限個の値を持つ主張と、任意の一つの自然数が有限回の `succ` で生成される主張を、量化子の順序を含む二文で書き分けます。
その上で、無限ストリームに求められる「任意の有限段階まで観察できる」という性質が、有限な構成子列とどう異なるかを論じます。
-/

end FormalLab.Foundation.InductiveTypes