import FormalLab.Bridges.CoinductionAndFinalCoalgebras
import FormalLab.Mathematics.Cardinality
import FormalLab.CategoryTheory.Limits

/-!
# 第69章：無限の三つの意味——基数・尽きない観察・無限図式

「無限」という一語は、異なる問いへの答えを隠すことがあります。自然数型が無限であるというときは要素数を
比較しています。ストリームが無限であるというときは、任意の有限時刻まで観察を続けられることを指します。
可算個の対象からなる図式を考えるときは、構成に現れる添字圏が無限です。

三者を同一視すると、有限状態機械は尽きない振舞いを作れないと誤解します。また、無限状態機械は無限個の
異なる振舞いを持つと推論してしまいます。無限図式の極限対象は無限集合になるという推論も成り立ちません。
本章ではそれぞれに反例を与えます。

最後に、長さ `n` の有限prefixを制限写像で結んだ逆系を構成します。ストリームは全ての有限prefixを整合的に
選ぶ糸を与えます。この例を通して、潜在的に尽きない観察と、無限図式の極限による一つの全体対象との関係を
明示します。ただし、どちらも基数的無限の定義へ還元しません。

## 基数的無限は要素の対応を問う

第25章の `CountablyInfinite A` は、`A` と自然数の間の全単射が存在するという命題です。まず自然数自身と
偶数型の例を再確認します。

$$
\mathsf{CountablyInfinite}(A)
\;:\Longleftrightarrow\;A\cong\mathbb N.
$$
-/

namespace FormalLab.Bridges.ThreeNotionsOfInfinity

open _root_.CategoryTheory
open FormalLab.Mathematics.FunctionProperties
open FormalLab.Mathematics.Cardinality
open FormalLab.Recursion.CoinductivePredicates
open FormalLab.CategoryFoundations.FinalCoalgebras
open FormalLab.Bridges.CoinductionAndFinalCoalgebras

universe u

theorem natCountablyInfinite : CountablyInfinite Nat := by
  refine ⟨id, ?_⟩
  exact ⟨fun _ _ h => h, fun n => ⟨n, rfl⟩⟩

example : CountablyInfinite EvenNat := evenCountablyInfinite

theorem boolStreamsNotEnumeratedByNat :
    ¬ ∃ table : Nat → (Nat → Bool), IsSurjective table :=
  noSurjectionToBoolPowers

/-!
`Nat→Bool` の各要素は一つのストリームです。対角線定理は、ストリーム全体の型が自然数では全射的に列挙できない
ことを示します。一方、一つのストリームが持つ観察位置は自然数で添字づけられます。「各値を何番目かで観察
できる」と「全ストリームを何番目かで列挙できる」は量化の対象が異なります。

## 尽きない観察に無限個の状態は要らない

決定的なストリーム余代数 `S→A×S` の構造射は、現在の出力と次状態を常に返します。状態型 `S` が有限でも、
この一段観察を任意の有限回だけ反復できます。
-/

def toggleMachine : _root_.CategoryTheory.Endofunctor.Coalgebra
    (streamFunctor Bool) where
  V := Bool
  str := ↾fun state => (state, !state)

def alternating (initial : Bool) : Nat → Bool :=
  unfold toggleMachine initial

example : alternating false 0 = false := rfl
example : alternating false 1 = true := rfl
example : alternating false 2 = false := rfl
example : alternating false 3 = true := rfl

def finitePrefix {A : Type u} : Nat → (Nat → A) → List A
  | 0, _ => []
  | n + 1, stream => stream 0 :: finitePrefix n (fun k => stream (k + 1))

theorem finitePrefix_length {A : Type u} (n : Nat) (stream : Nat → A) :
    (finitePrefix n stream).length = n := by
  induction n generalizing stream with
  | zero => rfl
  | succ n ih => simp [finitePrefix, ih]

#eval finitePrefix 8 (alternating false)

/-!
状態は `false,true` の二つだけですが、`finitePrefix n` は任意の自然数 `n` について長さ `n` の観察列を返します。
ここでの「無限」は完成した実行が状態型の中に無限個の状態を格納するという意味ではありません。どの有限境界を
指定しても、その先まで観察できるという非有界性です。全振舞いは終余代数 `Nat→Bool` の一要素として表されます。

## 無限個の状態があっても振舞いは一つに潰れ得る

逆に、状態型が可算無限でも、観察が状態を区別するとは限りません。全ての状態が単位値を出力し、後者状態へ
移る機械を考えます。
-/

def invisibleNatMachine : _root_.CategoryTheory.Endofunctor.Coalgebra
    (streamFunctor Unit) where
  V := Nat
  str := ↾fun n => ((), n + 1)

theorem invisibleNatMachine_same_behavior (left right : Nat) :
    unfold invisibleNatMachine left = unfold invisibleNatMachine right := by
  funext n
  exact Subsingleton.elim _ _

example (left right : Nat) :
    Bisimilar (observe invisibleNatMachine) (observe invisibleNatMachine)
      (next invisibleNatMachine) (next invisibleNatMachine) (left, right) :=
  bisimilar_of_behaviorallyEqual invisibleNatMachine
    (invisibleNatMachine_same_behavior left right)

/-!
`Nat` が可算無限であることは内部状態の個数を述べます。全状態が終余代数の同じ点へ写るため、観察可能な
振舞いは一つです。基数的な状態空間の大きさと、振舞意味論が区別する同値類の個数を分けなければなりません。

## 無限図式は添字の形が無限である

可算逆系は、型 `D₀,D₁,…` と制限写像 `Dₙ₊₁→Dₙ` から成ります。これは圏論では自然数の反対向きの鎖を
形とする図式です。ここでは型と関数だけで同じデータを明示します。

$$
D_0\xleftarrow{r_0}D_1\xleftarrow{r_1}D_2\xleftarrow{}\cdots,
\qquad
\lim D=\{(x_n)_n\mid r_n(x_{n+1})=x_n\}.
$$
-/

structure InverseSequence where
  obj : Nat → Type u
  restrict : ∀ n, obj (n + 1) → obj n

def CompatibleThread (D : InverseSequence.{u}) :=
  {values : ∀ n, D.obj n // ∀ n, D.restrict n (values (n + 1)) = values n}

structure SequenceCone (D : InverseSequence.{u}) (X : Type u) where
  leg : ∀ n, X → D.obj n
  compatible : ∀ n x, D.restrict n (leg (n + 1) x) = leg n x

def threadProjection (D : InverseSequence.{u}) (n : Nat) :
    CompatibleThread D → D.obj n :=
  fun thread => thread.1 n

def threadLift {D : InverseSequence.{u}} {X : Type u}
    (cone : SequenceCone D X) : X → CompatibleThread D :=
  fun x => ⟨fun n => cone.leg n x, fun n => cone.compatible n x⟩

theorem threadLift_fac {D : InverseSequence.{u}} {X : Type u}
    (cone : SequenceCone D X) (n : Nat) :
    threadProjection D n ∘ threadLift cone = cone.leg n := rfl

theorem threadLift_unique {D : InverseSequence.{u}} {X : Type u}
    (cone : SequenceCone D X) (candidate : X → CompatibleThread D)
    (fac : ∀ n, threadProjection D n ∘ candidate = cone.leg n) :
    candidate = threadLift cone := by
  funext x
  apply Subtype.ext
  funext n
  exact congrFun (fac n) x

/-!
`CompatibleThread D` は逆系の極限を具体化します。射影 `threadProjection` は各段階の値を取り出し、`threadLift`
は整合する脚の族を一つの糸へ束ねます。`threadLift_fac` と `threadLift_unique` は、極限の媒介射の計算則と
一意性です。図式が可算個の対象を持つことと、極限型が無限個の要素を持つことは別の主張です。

## 無限図式の極限が一点になる例

全ての段階を `Unit`、全ての制限写像を恒等写像にした逆系を考えます。添字は自然数全体ですが、整合する糸は
ただ一つです。
-/

def unitSequence : InverseSequence where
  obj _ := Unit
  restrict _ := id

theorem unitSequence_thread_unique (left right : CompatibleThread unitSequence) :
    left = right := by
  apply Subtype.ext
  funext n
  change left.1 n = right.1 n
  exact Unit.ext _ _

/-!
従って「無限図式だから極限対象も基数的に無限」という含意は成り立ちません。無限性はここでは図式の形、
すなわち対象と整合条件を何段階並べるかに属します。

## 有限prefixの逆系からストリームへ近づく

長さ `n` の真偽値prefixを `Fin n→Bool` と表します。長さ `n+1` のprefixから最後の一項を忘れると長さ `n` の
prefixになります。これらを全て整合的に選ぶ糸は、無限ストリームの有限近似を一度に記録します。
-/

def boolPrefixSequence : InverseSequence where
  obj n := Fin n → Bool
  restrict _ longer := fun position => longer position.castSucc

def streamToThread (stream : Nat → Bool) : CompatibleThread boolPrefixSequence :=
  ⟨fun _ position => stream position.val, by
    intro n
    rfl⟩

def threadToStream (thread : CompatibleThread boolPrefixSequence) : Nat → Bool :=
  fun n => thread.1 (n + 1) ⟨n, Nat.lt_add_one n⟩

theorem threadToStream_streamToThread (stream : Nat → Bool) :
    threadToStream (streamToThread stream) = stream := by
  funext n
  rfl

/-!
`streamToThread` は一つのストリームから全有限prefixを同時に作り、その制限整合性を証明します。
`threadToStream` は長さ `n+1` のprefixから位置 `n` を読みます。示した逆法則により、有限近似の整合族は
少なくともストリームの情報を失いません。逆向きの法則には、整合条件を有限回反復して任意の長いprefixを
短いprefixへ制限する証明が必要です。

この極限表示は、各段階では有限な観察しか持たず、全段階の整合性によってストリーム全体を特徴づけます。
一方 `Nat→Bool` が非可算であることは対角線による基数の主張です。同じ型が両方の議論に現れても、証明する
普遍性と基数比較は異なります。

$$
(\mathbb N\to\mathsf{Bool})
\longrightarrow\lim_n(\mathsf{Fin}(n)\to\mathsf{Bool})
$$

は有限prefixを全段階で取り出す写像であり、本章では反対向きとの一方の逆法則まで形式化しています。

## 三つの量化を比較する

| 観点 | 量化するもの | 代表的な主張 | 反例が示す境界 |
|---|---|---|---|
| 基数 | 型の要素と写像 | `A≃Nat`、単射・全射 | 状態が無限でも振舞いは一つになり得る |
| 尽きない観察 | 任意の有限時刻 | `∀n`, 長さ `n` のprefixを得る | 二状態でも観察は任意に続く |
| 無限図式 | 添字圏の対象・射 | 可算逆系の極限 | 可算個の段階でも極限は一点になり得る |

量化の対象を明示すれば、必要な証明原理も分かれます。基数には単射・全射、尽きない観察には全域的な一段展開と
余帰納、無限図式には錐の整合性と普遍性を使います。

## 要点

* 基数的無限は型の要素数を単射・全射・全単射で比較する主張である。
* 潜在的に尽きない観察は、任意の有限境界まで一段観察を反復できるという主張である。
* 有限状態機械でも無限に観察でき、無限状態機械でも全状態が同じ振舞いを持ち得る。
* 無限図式の無限性は添字の形に属し、極限対象の基数的無限を含意しない。
* ストリームは有限prefixの逆系の整合する糸として表せるが、その極限普遍性と非可算性は別の定理である。
* 「何を無限個量化しているか」を明示することが、三概念を接続しつつ混同を避ける基準になる。

## 研究史と文献案内

集合の濃度比較と非可算性の成立史は Cantor [CAN74]、真部分と全体の対応による無限系は Dedekind [DED88] を
参照してください。現在の基数概念を両原典の記法へそのまま投影しません。終余代数と潜在的に無限なシステムの
振舞意味論は Rutten [RUT00]、図式・錐・極限の現代的な定式化は Mac Lane [MAC98] を参照してください。
本章の三分法は歴史上の単一文献の分類を転記したものではなく、異なる現代理論の量化対象を比較するための構成です。
`CompatibleThread` は可算逆極限の教育用実装であり、mathlibの一般の `Cone` と `IsLimit` を置き換えません。

## 問題

### 状態数と振舞い数の四つの組合せを作る

有限状態・有限振舞い、有限状態・尽きない振舞い、無限状態・一振舞い、無限状態・複数振舞いの機械をそれぞれ
構成してください。状態型の基数、終余代数への像、任意長prefixの存在を別々に証明します。一つの証明を別の欄へ
流用できない箇所を特定し、状態同型と振舞等価の差を最小の二機械で説明できれば完了です。

### 有限prefixの糸とストリームの同値を完成する

`streamToThread` と `threadToStream` の残る合成が恒等になることを証明してください。整合条件を一段だけ使う補題を
作り、長いprefixを位置の差だけ繰り返し制限する帰納法へ一般化します。Subtype外延性、関数外延性、`Fin` の値と
境界証明の扱いを分離し、どの等式が計算で、どの等式が整合性から従うかを記録できれば完了です。

### 一般の錐として可算逆極限を再構成する

自然数を反対向きの射で結ぶ圏を定義し、`InverseSequence` をその圏から `Type` への関手へ移してください。
`SequenceCone` をmathlibの `Cone`、`CompatibleThread` を極限錐へ対応させ、`threadLift_fac` と
`threadLift_unique` が `IsLimit.fac` と `IsLimit.uniq` のどの引数になるかを全ての射型つきで示してください。

### ストリーム全体の基数と一つの観察列を分ける

`boolStreamsNotEnumeratedByNat` の量化順序を書き下し、任意の列挙候補から対角ストリームを作る段階を追跡して
ください。一方、固定したストリームの位置が自然数で列挙される写像を示します。「位置の集合が可算だから
ストリームの集合も可算」という誤推論で交換された量化を特定し、有限アルファベットの場合へ一般化できれば完了です。
-/

end FormalLab.Bridges.ThreeNotionsOfInfinity