import FormalLab.Recursion.Lattices

/-!
# 第28章：最小・最大不動点とKnaster–Tarski定理

再帰的な定義 `X = F(X)` は方程式だけでは解を一つに決めません。作用素が複数の不動点を持つとき、
有限回の生成で正当化される最小の解を選ぶのか、有限回の観察で否定できない最大の解を選ぶのかで
意味が変わります。

本章では述語集合の完備格子上でKnaster–Tarski型の構成を証明します。最小不動点を全前不動点の共通部分、
最大不動点を全後不動点の和として定義し、単調性だけから各々が不動点であることを示します。その後、
自然数を生成する作用素を例に、最小性が帰納法を与える仕組みを具体化します。

## 前不動点の共通部分を最小候補にする

`F : P(A)→P(A)` を単調作用素とします。`F(X)⊆X` を満たす前不動点は、`F` の規則で一段生成しても
閉じています。全前不動点の共通部分を `μF` と定めます。

$$
\mu F\;:\!\equiv\;\bigcap\{X\subseteq A\mid F(X)\subseteq X\}.
$$

定義から `μF` は任意の前不動点以下です。しかし `F(μF)=μF` を得るには、単調性を二度使って両方向の
包含を示す必要があります。
-/

namespace FormalLab.Recursion.FixedPoints

universe u

open FormalLab.Recursion.Lattices

def leastFixedPoint {A : Type u} (operator : PredSet A → PredSet A) : PredSet A :=
  Infimum (Prefixpoint operator)

def greatestFixedPoint {A : Type u} (operator : PredSet A → PredSet A) : PredSet A :=
  Supremum (Postfixpoint operator)

theorem leastBelowEveryPrefixpoint {A : Type u} (operator : PredSet A → PredSet A)
    {set : PredSet A} (preFixed : Prefixpoint operator set) :
    Subset (leastFixedPoint operator) set :=
  fun _ inLeast => inLeast set preFixed

theorem operatorLeastBelowLeast {A : Type u} {operator : PredSet A → PredSet A}
    (monotone : Monotone operator) :
    Subset (operator (leastFixedPoint operator)) (leastFixedPoint operator) := by
  intro x inOperatorLeast set preFixed
  have imageInclusion := monotone (leastBelowEveryPrefixpoint operator preFixed)
  exact preFixed (imageInclusion inOperatorLeast)

/-!
任意の前不動点 `X` に対して `μF⊆X` です。単調性から `F(μF)⊆F(X)`、前不動点性から
`F(X)⊆X` なので、`F(μF)` は全前不動点に含まれます。したがって `F(μF)⊆μF` です。

逆包含では、今得た包含に単調性を適用して `F(F(μF))⊆F(μF)` を得ます。つまり `F(μF)` 自身が
前不動点です。`μF` は全前不動点の共通部分なので `μF⊆F(μF)` となります。
-/

theorem leastBelowOperatorLeast {A : Type u} {operator : PredSet A → PredSet A}
    (monotone : Monotone operator) :
    Subset (leastFixedPoint operator) (operator (leastFixedPoint operator)) := by
  have operatorIsPrefix : Prefixpoint operator (operator (leastFixedPoint operator)) :=
    monotone (operatorLeastBelowLeast monotone)
  exact leastBelowEveryPrefixpoint operator operatorIsPrefix

theorem leastIsFixedPoint {A : Type u} {operator : PredSet A → PredSet A}
    (monotone : Monotone operator) :
    FixedPoint operator (leastFixedPoint operator) :=
  ⟨operatorLeastBelowLeast monotone, leastBelowOperatorLeast monotone⟩

theorem leastAmongFixedPoints {A : Type u} (operator : PredSet A → PredSet A)
    {set : PredSet A} (fixed : FixedPoint operator set) :
    Subset (leastFixedPoint operator) set :=
  leastBelowEveryPrefixpoint operator fixed.1

/-!
ここまでで `μF` が不動点であり、他の全不動点以下であることを証明しました。完全な格子一般の
Knaster–Tarski定理では同じ論証を任意下限で行います。本章のLean定理は述語集合という重要な場合を
完全に証明しており、一般の完備格子定理を証明したと主張するものではありません。

## 後不動点の和を最大候補にする

双対に、`X⊆F(X)` を満たす全後不動点の和を `νF` とします。

$$
\nu F\;:\!\equiv\;\bigcup\{X\subseteq A\mid X\subseteq F(X)\}.
$$

単調性のもとで、二候補は次の不動点方程式と極値性を満たします。

$$
F(\mu F)=\mu F,\qquad F(\nu F)=\nu F,
\qquad
\mu F\subseteq X\subseteq\nu F
\quad(F(X)=X).
$$

各後不動点 `X` は `νF` に含まれます。単調性により各 `F(X)` も `F(νF)` に含まれるため、
`νF⊆F(νF)` が得られます。
-/

theorem everyPostfixpointBelowGreatest {A : Type u} (operator : PredSet A → PredSet A)
    {set : PredSet A} (postFixed : Postfixpoint operator set) :
    Subset set (greatestFixedPoint operator) :=
  fun _ membership => ⟨set, postFixed, membership⟩

theorem greatestBelowOperatorGreatest {A : Type u} {operator : PredSet A → PredSet A}
    (monotone : Monotone operator) :
    Subset (greatestFixedPoint operator) (operator (greatestFixedPoint operator)) := by
  intro x inGreatest
  rcases inGreatest with ⟨set, postFixed, inSet⟩
  have imageInclusion := monotone (everyPostfixpointBelowGreatest operator postFixed)
  exact imageInclusion (postFixed inSet)

theorem operatorGreatestBelowGreatest {A : Type u} {operator : PredSet A → PredSet A}
    (monotone : Monotone operator) :
    Subset (operator (greatestFixedPoint operator)) (greatestFixedPoint operator) := by
  have operatorIsPostfix : Postfixpoint operator (operator (greatestFixedPoint operator)) :=
    monotone (greatestBelowOperatorGreatest monotone)
  exact everyPostfixpointBelowGreatest operator operatorIsPostfix

theorem greatestIsFixedPoint {A : Type u} {operator : PredSet A → PredSet A}
    (monotone : Monotone operator) :
    FixedPoint operator (greatestFixedPoint operator) :=
  ⟨operatorGreatestBelowGreatest monotone, greatestBelowOperatorGreatest monotone⟩

theorem greatestAmongFixedPoints {A : Type u} (operator : PredSet A → PredSet A)
    {set : PredSet A} (fixed : FixedPoint operator set) :
    Subset set (greatestFixedPoint operator) :=
  everyPostfixpointBelowGreatest operator fixed.2

/-!
最小側と最大側の証明は包含の向きを全て反転した双対です。単に `μ` を `ν` へ書き換えるのではなく、
共通部分を和へ、前不動点を後不動点へ、最小性を最大性へ同時に反転します。

## 自然数生成作用素から帰納法を読む

`F(X) = {0} ∪ {n+1 | n∈X}` とします。`F` は単調で、その前不動点は零を含み後者で閉じた述語です。
したがって `μF` は全てのそのような述語に含まれる要素、すなわち有限回の零・後者で生成できる自然数です。
-/

def naturalGenerator (set : PredSet Nat) : PredSet Nat :=
  fun n => n = 0 ∨ ∃ predecessor, set predecessor ∧ n = predecessor + 1

theorem naturalGeneratorMonotone : Monotone naturalGenerator := by
  intro left right inclusion n generated
  cases generated with
  | inl zero => exact Or.inl zero
  | inr successor =>
      rcases successor with ⟨predecessor, inLeft, equation⟩
      exact Or.inr ⟨predecessor, inclusion inLeft, equation⟩

theorem everyNaturalInLeastFixedPoint (n : Nat) :
    leastFixedPoint naturalGenerator n := by
  induction n with
  | zero =>
      intro set preFixed
      exact preFixed (Or.inl rfl)
  | succ n hypothesis =>
      intro set preFixed
      exact preFixed (Or.inr ⟨n, hypothesis set preFixed, rfl⟩)

/-!
この証明の `set` と `prefix` は任意の前不動点です。零の場合は閉包規則を一度使い、後者の場合は帰納仮定で
前の数が `set` に属すことを得てから再び閉包規則を使います。最小不動点の所属を「全ての閉じた述語に
属すること」と展開すると、通常の帰納法が現れます。

単調性を外すと前不動点の共通部分が前不動点である証明の `monotone` の行が失敗します。不動点が存在する
特定の非単調作用素はあり得ますが、完備格子上の一様な存在定理はこの仮定なしには得られません。

## 要点

* 最小不動点 `μF` は全前不動点 `F(X)≤X` の下限として構成される。
* 最大不動点 `νF` は全後不動点 `X≤F(X)` の上限として構成される。
* 単調性により `F(μF)=μF` と `F(νF)=νF` の両包含が得られる。
* `μF` は全不動点以下、`νF` は全不動点以上である。
* 生成規則の最小不動点を全ての閉じた述語で特徴づけると帰納原理が得られる。

## 研究史と文献案内

Tarskiの1955年論文 [TAR55] は完備格子上の単調写像の不動点集合を扱う基準文献です。現在
Knaster–Tarski定理と呼ばれる系譜にはKnasterとの先行研究と後世の標準化があるため、1955年論文だけへ
名称全体を単純帰属させません。プログラム意味論における最小不動点は後の領域理論章、最大不動点と
余帰納は次章で、それぞれ追加構造を導入して扱います。

## 問題

### 最小不動点証明の二度の単調性を追う

`operatorLeastBelowLeast` と `leastBelowOperatorLeast` を通常の集合記法へ翻訳してください。各証明で
比較する二集合、単調性へ渡す包含、前不動点性を使う位置を表にします。単調性を削除したとき最初に
型付けできなくなる推論を特定し、単なる記号の反転でないことを説明すれば完了です。

### 帰納的生成を別の規則へ移す

偶数を零と二加算で生成する作用素、二進木を葉と節点で生成する作用素を述語集合上に定義してください。
単調性を証明し、最小不動点に属する代表値を帰納法で示します。任意の前不動点を受け取る形へ証明を
一般化し、生成規則ごとの帰納仮定がどこに現れるかを示せば完了です。
偶数作用素の最小不動点に奇数が入らない逆向きも証明し、生成の十分性と必要性を分けてください。

### 最大不動点を直接に特徴づける

最大側の四定理について、最小側から反転した語と包含方向を列挙してください。その上で一つの後不動点を
具体的に選び、`greatestFixedPoint` の和へ入る証人を構成します。`νF⊆F(νF)` と逆包含で単調性が
別々にどう使われるかを証明項から説明できれば完了です。
最小側の証明を機械的に反転しただけでは型が合わない箇所を一つ示し、その原因を量化から説明してください。
-/

end FormalLab.Recursion.FixedPoints