import FormalLab.TypeTheory.SubtypesAndRefinements

/-!
# 第35章：添字付き帰納族

通常のリストでは長さは値を調べて初めて分かります。長さを型の添字にすれば、空列の長さは
零であり、要素を追加すると長さが一つ増えることを構成子の型そのものが保証できます。
不変条件は後から証明する性質ではなく、構成可能な値の形へ移ります。

本章では長さ付き列 `Vector A n` を例に、全構成子で固定されるパラメータ `A` と、構成結果を
分類する添字 `n` を分けます。型の合わない分岐が除去原理から消える仕組みを読み、一般の
帰納族、等式型、有限集合 `Fin n`、厳密正値性へ進む準備をします。

## 構成の結果を型の添字に記録する

長さ付き列を型族 `Vector : 𝒰 → Nat → 𝒰` とし、その導入規則を

$$
\frac{}{\mathsf{nil}:\mathsf{Vector}(A,0)}
\qquad
\frac{a:A\qquad xs:\mathsf{Vector}(A,n)}
     {\mathsf{cons}(a,xs):\mathsf{Vector}(A,S(n))}.
$$

形成規則を含めると、$A:\mathsf{Type}_u$ ごとに

$$
\mathsf{Vector}(A,-):\mathbb N\to\mathsf{Type}_u
$$

という型族を得ます。構成子は値だけでなく、結果が属するファイバー $0$ または $S(n)$ も決めます。

と書きます。`Vector A n` では、`A` は全構成子で固定される**パラメータ**、`n` は構成結果によって
変わる**添字**です。構成子の結果型を見ると、作れる長さが分かります。

通常の帰納型では構成子が「どの値を作るか」を決めます。帰納族ではさらに「どのファイバー
の値を作るか」まで決めます。添字は保存したい性質を後から証明する注釈ではなく、構成子の
型によって最初から制約される分類情報です。


-/

namespace FormalLab.TypeTheory.IndexedFamilies

universe u v

/-! ## 構成子の結果型が添字を決める -/

/-- 要素型 `α` と長さ `n` で分類された列です。 -/
inductive Vector (α : Type u) : Nat → Type u where
  | nil : Vector α 0
  | cons {n : Nat} : α → Vector α n → Vector α (n + 1)

/-!
宣言を四つの観点から読みます。

* `Vector (α : Type u) : Nat → Type u` は、各長さに型を割り当てる型族を形成する。
* `nil` は長さ `0` のファイバーだけに値を導入する。
* `cons` は長さ `n` の値から長さ `n + 1` の値を導入する。
* 除去時には、入力の添字と両立する構成子だけが分岐として残る。

この最後の点により、`Vector α (n + 1)` は `.nil` ではあり得ず、`head` に空の場合を
書く必要がありません。
-/

/-- 一要素から、長さが定義上 `1` のベクトルを作ります。 -/
def singleton {α : Type u} (value : α) : Vector α 1 :=
  .cons value .nil

/-- 空でないことが型に現れるため、失敗分岐なしに先頭を返せます。 -/
def head {α : Type u} {n : Nat} : Vector α (n + 1) → α
  | .cons value _ => value

/-- 非空ベクトルの残りは、型レベルでも一つ短いベクトルです。 -/
def tail {α : Type u} {n : Nat} : Vector α (n + 1) → Vector α n
  | .cons _ rest => rest

/-- 要素を変換しても、構成子の個数すなわち長さ添字は保存されます。 -/
def map {α : Type u} {β : Type v} (f : α → β) : {n : Nat} → Vector α n → Vector β n
  | 0, .nil => .nil
  | _ + 1, .cons value rest => .cons (f value) (map f rest)

/-- 同じ長さの二ベクトルは、不可能分岐なしに点ごとの対へ結合できます。 -/
def zip {α : Type u} {β : Type v} : {n : Nat} →
    Vector α n → Vector β n → Vector (α × β) n
  | 0, .nil, .nil => .nil
  | _ + 1, .cons left lefts, .cons right rights =>
      .cons (left, right) (zip lefts rights)

/-- 添字を返すだけなので、値を走査する必要がありません。 -/
def vectorLength {α : Type u} {n : Nat} (_ : Vector α n) : Nat :=
  n

theorem singletonLength {α : Type u} (value : α) :
    vectorLength (singleton value) = 1 :=
  rfl

example : head (singleton true) = true := rfl
example : vectorLength (map Nat.succ (singleton 0)) = 1 := rfl
example : zip (singleton 1) (singleton true) = singleton (1, true) := rfl

#check Vector.nil
#check Vector.cons
#check head

/-!
## 添字は実行時検査ではない

`{xs : List α // xs.length = n}` も長さを保証します。部分型は既存データに性質を付加し、
添字付き帰納族は許された構成操作そのものを設計します。表現が常に同じ計算特性やAPIを
持つわけではないため、論理的に似た不変条件だけで同一視しません。

添字は実行時に必ず保存された自然数フィールドだとも限りません。`vectorLength` は型から
`n` を返す定義であり、列を走査して数えません。抽出・実行時表現と、型検査時の添字情報を
混同しないことが必要です。

`zip` では二入力が同じ添字 `n` を共有します。一方だけが空でもう一方だけが非空という組合せは型が
一致せず、定義の分岐に現れません。これは実行時に二つの長さを比較して失敗を返す処理ではなく、呼出し前に
同じファイバーへ属することを要求するAPIです。

## 要点

* 帰納族は値だけでなく、その値が属する型族のファイバーも構成子で決める。
* パラメータは定義全体で固定され、添字は構成結果を分類する。
* 不可能な構成子は依存パターンマッチから消え、失敗分岐のない関数を書ける。
* 部分型は既存データへ証明を付け、帰納族は正しいデータの構成方法を直接設計する。

## 研究史と文献案内

Dybjerの1994年論文 [DYB94] はMartin-Löf型理論における帰納族を一般的に扱います。
長さ付きvectorは代表例ですが、論文の主眼は個別のデータ構造ではなく一般の形成・導入・
除去原理です。Leanの帰納族・依存パターンマッチはその概念を発展させた実装であり、現行仕様は
[LEAN-REF] を参照します。

## 問題

### 構成子の結果型から不可能な場合を読む

`Vector.nil` と `Vector.cons` の型を展開し、`α` がパラメータ、長さが添字であることを説明せよ。
`Vector.nil` が `Vector α 1` を作れない理由を結果型から示し、`head` と `tail` に空ベクトルの
分岐が存在しない理由を入力型へ戻って説明する。

長さ `0` のベクトルから任意の命題を導くのではなく、長さ `1` の入力を除去すると空の構成子が
候補にならない、という依存パターンマッチの働きを正確に述べること。

### 添字保存をプログラムの型で検査する

`map` の各分岐を追い、入力と出力の長さが一致する根拠を構成子の型まで遡れ。二つの関数を順に
写すプログラムを定義し、`map g (map f xs) = map (g ∘ f) xs` をベクトルの帰納法で証明せよ。

等式の両辺がそもそも同じ型をもつことと、値として等しいことを分けて記述する。前者は添字保存、
後者は関数法則であり、型検査だけで後者まで得られるわけではない。

### 帰納族と部分型による表現を比較する

`Vector α n` と `{xs : List α // xs.length = n}` について、値の構成、先頭の除去、連結、等式の
証明を比較せよ。同じ数学的対象を表し得ても、計算時に現れる等式輸送と帰納原理の形が異なる。

少なくとも一つの操作を両表現で実装し、どちらで長さの整合性が構成子により自動化され、どちらで
証明成分を明示的に運ぶ必要があるかをコード上で指摘せよ。
-/

end FormalLab.TypeTheory.IndexedFamilies