import FormalLab.Recursion.FixedPoints
import FormalLab.TypeTheory.RecursiveTypes

/-!
# 第30章：領域理論・連続写像・再帰方程式

停止しない計算にも意味を与えるには、「値がない」を単なるエラーでなく最小の情報として扱う方法が
必要です。さらに再帰関数を零段、一步、二歩と有限に近似し、その増大列の極限を意味とするには、
任意集合の上限より計算に即した可算増大列の上限が重要になります。

本章では最下元を持つω完備半順序（ω-CPO）を定義します。増大列、上限、Scott連続写像を別々に
形式化し、最下元からの反復の上限が不動点であり、全ての前不動点以下であることを証明します。
最後に `Option A` の平坦な情報順序と有限燃料の階乗近似から、部分性と近似の読み方を具体化します。

## ω鎖は情報が段階ごとに増える列である

半順序 `(D,⊑)` の列 `d₀,d₁,…` がω鎖であるとは `dₙ⊑dₙ₊₁` が全ての `n` で成り立つことです。
上限 `⊔ₙdₙ` は全要素以上であり、そのような上界のうち最小です。任意部分集合の上限を要求する
完備格子と異なり、ω-CPOが要求するのはこの可算増大列の上限です。

$$
d_0\sqsubseteq d_1\sqsubseteq\cdots,
\qquad
d_n\sqsubseteq\bigsqcup_{k<\omega}d_k,
\qquad
(\forall n,\ d_n\sqsubseteq u)
  \Rightarrow\bigsqcup_{k<\omega}d_k\sqsubseteq u.
$$
-/

namespace FormalLab.Recursion.DomainTheory

universe u v

structure OmegaChain {D : Type u} (le : D → D → Prop) where
  term : Nat → D
  increasing : ∀ n, le (term n) (term (n + 1))

structure PointedOmegaCPO (D : Type u) where
  le : D → D → Prop
  refl : ∀ x, le x x
  trans : ∀ {x y z}, le x y → le y z → le x z
  antisymm : ∀ {x y}, le x y → le y x → x = y
  bottom : D
  bottom_le : ∀ x, le bottom x
  supremum : OmegaChain le → D
  le_supremum : ∀ (chain : OmegaChain le) n, le (chain.term n) (supremum chain)
  supremum_le : ∀ (chain : OmegaChain le) upper,
    (∀ n, le (chain.term n) upper) → le (supremum chain) upper

/-!
`PointedOmegaCPO` は順序法則、最下元、各ω鎖の指定上限とその普遍性を束ねます。`supremum` という
演算だけでは不十分であり、`le_supremum` と `supremum_le` が上限であることを保証します。
本章では簡潔さのため構造フィールドとして法則を保持しますが、mathlibの既存順序階層と同じAPIだとは
みなしません。

## 連続写像はω鎖の上限を保存する

写像 `f:D→D` がScott連続であるためには、単調であるだけでなく、各ω鎖について
`f(⊔ₙdₙ)=⊔ₙf(dₙ)` を満たす必要があります。像列が再びω鎖になることは単調性から従います。

$$
f\!\left(\bigsqcup_{n<\omega}d_n\right)
=\bigsqcup_{n<\omega}f(d_n).
$$
-/

def mapChain {D : Type u} {E : Type v}
    (source : PointedOmegaCPO D) (target : PointedOmegaCPO E)
    (f : D → E)
    (monotone : ∀ {x y}, source.le x y → target.le (f x) (f y))
    (chain : OmegaChain source.le) : OmegaChain target.le where
  term n := f (chain.term n)
  increasing n := monotone (chain.increasing n)

structure ScottContinuous {D : Type u} (domain : PointedOmegaCPO D) (f : D → D) where
  monotone : ∀ {x y}, domain.le x y → domain.le (f x) (f y)
  preservesSupremum : ∀ chain : OmegaChain domain.le,
    f (domain.supremum chain) =
      domain.supremum (mapChain domain domain f monotone chain)

/-!
単調性だけなら各近似の像の順序は保ちますが、極限で新しい結果が突然現れないことまでは保証しません。
上限保存が、有限近似から再帰意味を回収する推論に必要です。

## 最下元から作用素を反復する

連続な `f:D→D` に対し `d₀=⊥`、`dₙ₊₁=f(dₙ)` と置きます。最下元性と単調性によりこの列は増大します。

$$
d_0=\bot,
\qquad d_{n+1}=f(d_n),
\qquad
\operatorname{fix}(f)=\bigsqcup_{n<\omega}d_n.
$$
-/

def approximant {D : Type u} (domain : PointedOmegaCPO D) (f : D → D) : Nat → D
  | 0 => domain.bottom
  | n + 1 => f (approximant domain f n)

theorem approximantIncreasing {D : Type u} (domain : PointedOmegaCPO D) (f : D → D)
    (monotone : ∀ {x y}, domain.le x y → domain.le (f x) (f y)) :
    ∀ n, domain.le (approximant domain f n) (approximant domain f (n + 1)) := by
  intro n
  induction n with
  | zero => exact domain.bottom_le _
  | succ n hypothesis => exact monotone hypothesis

def approximationChain {D : Type u} (domain : PointedOmegaCPO D) (f : D → D)
    (monotone : ∀ {x y}, domain.le x y → domain.le (f x) (f y)) :
    OmegaChain domain.le where
  term := approximant domain f
  increasing := approximantIncreasing domain f monotone

def kleeneFixedPoint {D : Type u} (domain : PointedOmegaCPO D) (f : D → D)
    (continuous : ScottContinuous domain f) : D :=
  domain.supremum (approximationChain domain f continuous.monotone)

/-!
像鎖の第 `n` 項は元の鎖の第 `n+1` 項です。元の鎖と先頭を一つ落とした像鎖は同じ上限を持ちます。
この一段のずれ、上限保存、反対称性を組み合わせて固定性を証明します。
-/

theorem kleene_is_fixed {D : Type u} (domain : PointedOmegaCPO D) (f : D → D)
    (continuous : ScottContinuous domain f) :
    f (kleeneFixedPoint domain f continuous) = kleeneFixedPoint domain f continuous := by
  unfold kleeneFixedPoint
  rw [continuous.preservesSupremum]
  apply domain.antisymm
  · apply domain.supremum_le
    intro n
    exact domain.le_supremum
      (approximationChain domain f continuous.monotone) (n + 1)
  · apply domain.supremum_le
    intro n
    cases n with
    | zero => exact domain.bottom_le _
    | succ n =>
        exact domain.le_supremum
          (mapChain domain domain f continuous.monotone
            (approximationChain domain f continuous.monotone)) n

theorem approximantBelowPrefixpoint {D : Type u} (domain : PointedOmegaCPO D)
    (f : D → D) (continuous : ScottContinuous domain f) {upper : D}
    (preFixed : domain.le (f upper) upper) :
    ∀ n, domain.le (approximant domain f n) upper := by
  intro n
  induction n with
  | zero => exact domain.bottom_le upper
  | succ n hypothesis =>
      exact domain.trans (continuous.monotone hypothesis) preFixed

theorem kleene_least_prefixpoint {D : Type u} (domain : PointedOmegaCPO D)
    (f : D → D) (continuous : ScottContinuous domain f) {upper : D}
    (preFixed : domain.le (f upper) upper) :
    domain.le (kleeneFixedPoint domain f continuous) upper := by
  apply domain.supremum_le
  exact approximantBelowPrefixpoint domain f continuous preFixed

/-!
`kleene_is_fixed` と `kleene_least_prefixpoint` により、反復上限は不動点であり全前不動点以下です。
前章のKnaster–Tarski構成は完備格子と単調性を使いました。本章のKleene構成はω鎖の上限と連続性を使い、
有限反復がどのように解へ近づくかも与えます。存在定理の仮定と得られる計算的情報が異なります。

$$
f(\operatorname{fix}(f))=\operatorname{fix}(f),
\qquad
f(u)\sqsubseteq u\Rightarrow\operatorname{fix}(f)\sqsubseteq u.
$$

## `Option A` は未定義を最小情報にする

平坦領域では `none` を未定義または未計算、`some a` を確定値と読みます。`none⊑x` は常に成立し、
二つの確定値は中身が等しいときだけ比較できます。
-/

def FlatLe {A : Type u} : Option A → Option A → Prop
  | none, _ => True
  | some left, some right => left = right
  | some _, none => False

theorem flat_refl {A : Type u} (x : Option A) : FlatLe x x := by
  cases x <;> simp [FlatLe]

theorem flat_trans {A : Type u} {x y z : Option A} :
    FlatLe x y → FlatLe y z → FlatLe x z := by
  cases x <;> cases y <;> cases z <;> simp [FlatLe]
  intro equal₁ equal₂
  exact equal₁.trans equal₂

theorem flat_antisymm {A : Type u} {x y : Option A} :
    FlatLe x y → FlatLe y x → x = y := by
  cases x <;> cases y <;> simp [FlatLe]
  intro equal _
  cases equal
  rfl

def partialMap {A : Type u} {B : Type v} (f : A → B) : Option A → Option B
  | none => none
  | some value => some (f value)

theorem partialMapMonotone {A : Type u} {B : Type v} (f : A → B)
    {x y : Option A} (information : FlatLe x y) :
    FlatLe (partialMap f x) (partialMap f y) := by
  cases x <;> cases y <;> simp [FlatLe, partialMap] at information ⊢
  cases information
  rfl

/-!
確定値どうしを無関係に順序づけないため、順序は数値の大小でなく情報量を表します。`partialMap` は
未定義を未定義のまま送り、確定値へ通常の関数を適用するので情報順序を保存します。

## 有限燃料は再帰計算の近似を作る

燃料が零なら結果は未計算です。燃料が一つ増えるたびに階乗の一段を展開します。
-/

def factorialApproximation : Nat → Nat → Option Nat
  | 0, _ => none
  | _ + 1, 0 => some 1
  | fuel + 1, n + 1 =>
      partialMap (fun result => (n + 1) * result) (factorialApproximation fuel n)

theorem factorialApproximation_insufficient : factorialApproximation 3 3 = none := rfl

theorem factorialApproximation_sufficient : factorialApproximation 4 3 = some 6 := rfl

/-!
入力 `3` には零の場合を含め四段の観察が必要です。燃料を増やして `some 6` に達した後は結果が変わりません。
これは平坦順序の増大列の具体例です。ただし本章では抽象ω-CPO上のKleene定理と、この有限燃料関数を
同一の定理で接続したとは主張しません。接続には近似列の単調性と上限の具体的構成が必要です。

## 要点

* ω-CPOは全ての可算増大列の上限を持ち、pointedなら最下元も持つ。
* Scott連続写像は単調であり、ω鎖の上限を保存する。
* 最下元からの反復は増大列をなし、その上限は連続作用素の不動点である。
* 反復上限は全前不動点以下なので最小不動点である。
* 平坦領域では未定義値が最小情報で、異なる確定値は比較不能である。

## 研究史と文献案内

Scottの1970年技術報告 [SCO70] はデータを近似順序で扱い、ラムダ計算とプログラム意味論へ数学的モデルを
与える研究計画を提示しました。Scottの連続格子論 [SCO72] は位相・順序・関数空間をさらに発展させます。
本章のω-CPOとKleene反復は現代的な教育用再構成であり、二文献の定義順や全定理をそのまま写したものでは
ありません。領域理論の標準的なプログラム意味論への展開は [PFPL16] も参照してください。

## 問題

### 反復列の上限が固定される証明を分解する

`kleene_is_fixed` の二つの包含を通常の順序記法で書き、零段と後者段を分けてください。連続性を使う行、
像鎖と元の鎖を一段ずらす行、反対称性を使う行を特定します。連続性を単調性だけへ弱めた場合に
不足する等式を明示し、証明の穴を仮定で隠していないことを確認すれば完了です。
さらに元の鎖と像鎖の最初の四項を書き、添字の一段ずれが各Lean項のどこに現れるかを対応づけてください。

### 平坦順序のω鎖を分類する

`Option Bool` 上の増大列を複数作り、`none` だけの列、途中で `some true` に確定する列、異なる確定値へ
移ろうとする非例を比較してください。最後の列がどの隣接段階で `FlatLe` を破るかを示します。
任意の正しい鎖が未定義のままか一つの値へ安定する理由を述べ、上限候補を構成すれば完了です。

### 燃料近似を意味論的近似へ接続する

`factorialApproximation fuel n` が燃料について `FlatLe` で増大することを、`fuel` と `n` のどちらへ
帰納すべきか検討して証明してください。十分な燃料で通常の階乗値を返す補題も別に定式化します。
停止入力、燃料不足、永久発散を `Option` の結果だけでどこまで区別できるかを説明すれば完了です。
-/

end FormalLab.Recursion.DomainTheory