import FormalLab.Mathematics.Orders

/-!
# 第27章：束・完備格子・単調作用素

集合の和と共通部分は、要素を集める二つの演算であるだけでなく、包含順序における最小上界と最大下界です。
有限個の上限・下限だけを持つ順序と、任意の族についてそれらを持つ順序を区別すると、再帰的な定義を
「近似の上限」として扱う準備が整います。

本章では束と完備格子を順序による普遍性から定義します。述語集合 `A → Prop` が包含順序で完備格子を
なすことを、任意和・任意共通部分の定理として検査します。次に単調作用素、前不動点、後不動点を導入し、
どの条件が不動点の存在証明に使われるかを具体例と反例から明らかにします。

## 二項の上限と下限が束を作る

半順序 `(L,≤)` で二要素 `a,b` の上限 `a∨b` は、`a≤a∨b` と `b≤a∨b` を満たす最小の要素です。
下限 `a∧b` は双対に、両方以下である最大の要素です。演算記号だけでなく、上界・下界と最小性・最大性の
法則を合わせて束と呼びます。

$$
\begin{aligned}
a\le a\vee b,\quad b\le a\vee b,\quad
&\bigl(a\le u\land b\le u\bigr)\to a\vee b\le u,\\
a\wedge b\le a,\quad a\wedge b\le b,\quad
&\bigl(l\le a\land l\le b\bigr)\to l\le a\wedge b.
\end{aligned}
$$
-/

namespace FormalLab.Recursion.Lattices

universe u

abbrev PredSet (A : Type u) := A → Prop

def Subset {A : Type u} (left right : PredSet A) : Prop :=
  ∀ ⦃x⦄, left x → right x

def BinaryJoin {A : Type u} (left right : PredSet A) : PredSet A :=
  fun x => left x ∨ right x

def BinaryMeet {A : Type u} (left right : PredSet A) : PredSet A :=
  fun x => left x ∧ right x

theorem leftBelowJoin {A : Type u} (left right : PredSet A) :
    Subset left (BinaryJoin left right) :=
  fun _ membership => Or.inl membership

theorem meetBelowLeft {A : Type u} (left right : PredSet A) :
    Subset (BinaryMeet left right) left :=
  fun _ membership => membership.1

theorem joinLeast {A : Type u} {left right upper : PredSet A}
    (leftBelow : Subset left upper) (rightBelow : Subset right upper) :
    Subset (BinaryJoin left right) upper := by
  intro x membership
  cases membership with
  | inl inLeft => exact leftBelow inLeft
  | inr inRight => exact rightBelow inRight

theorem meetGreatest {A : Type u} {left right lower : PredSet A}
    (belowLeft : Subset lower left) (belowRight : Subset lower right) :
    Subset lower (BinaryMeet left right) :=
  fun _ membership => ⟨belowLeft membership, belowRight membership⟩

/-!
`joinLeast` と `meetGreatest` が普遍性です。同じ型の二項演算があるだけでは束になりません。たとえば常に
左引数を返す演算は型が `L→L→L` でも、比較不能な二要素の共通上界にはなりません。

## 任意の上限と下限が完備格子を作る

族 `𝒮 : (A→Prop)→Prop` に属する全ての述語の上限は和、下限は共通部分です。

$$
\begin{aligned}
(\bigvee\mathcal S)(x)&\;:\!\Longleftrightarrow\;\exists S.\;\mathcal S(S)\land S(x),\\
(\bigwedge\mathcal S)(x)&\;:\!\Longleftrightarrow\;\forall S.\;\mathcal S(S)\to S(x).
\end{aligned}
$$

空族の和は空集合、空族の共通部分は全体集合になります。したがって完備格子は最下元と最上元も持ちます。
-/

def Supremum {A : Type u} (family : PredSet (PredSet A)) : PredSet A :=
  fun x => ∃ set, family set ∧ set x

def Infimum {A : Type u} (family : PredSet (PredSet A)) : PredSet A :=
  fun x => ∀ set, family set → set x

theorem supremumIsLeastUpperBound {A : Type u} (family : PredSet (PredSet A)) :
    FormalLab.Mathematics.Orders.IsSupremum Subset family (Supremum family) := by
  constructor
  · intro set inFamily x membership
    exact ⟨set, inFamily, membership⟩
  · intro upper upperBound x membership
    rcases membership with ⟨set, inFamily, inSet⟩
    exact upperBound inFamily inSet

theorem infimumIsGreatestLowerBound {A : Type u} (family : PredSet (PredSet A)) :
    FormalLab.Mathematics.Orders.IsInfimum Subset family (Infimum family) := by
  constructor
  · intro set inFamily x membership
    exact membership set inFamily
  · intro lower lowerBound x membership set inFamily
    exact lowerBound inFamily membership

def Bottom {A : Type u} : PredSet A := fun _ => False
def Top {A : Type u} : PredSet A := fun _ => True

theorem emptySupremumIsBottom {A : Type u} :
    Supremum (fun _ : PredSet A => False) = Bottom := by
  funext x
  apply propext
  constructor
  · rintro ⟨_, impossible, _⟩
    exact impossible
  · intro impossible
    exact False.elim impossible

theorem emptyInfimumIsTop {A : Type u} :
    Infimum (fun _ : PredSet A => False) = Top := by
  funext x
  apply propext
  constructor <;> intro
  · trivial
  · intro set impossible
    exact False.elim impossible

/-!
空族の二定理は空虚な全称量化と不可能な存在量化の差を示します。完備性は「全要素が互いに比較できる」
ことではありません。述語集合には比較不能な要素が多数ありますが、その任意族には上限と下限があります。

## 単調作用素は包含を保存する

作用素 `F : L→L` が単調であるとは `x≤y` から `F(x)≤F(y)` が従うことです。述語集合では、入力集合へ
要素を追加しても出力要素が失われないことを意味します。
-/

def Monotone {A : Type u} (operator : PredSet A → PredSet A) : Prop :=
  ∀ ⦃left right⦄, Subset left right → Subset (operator left) (operator right)

def Prefixpoint {A : Type u} (operator : PredSet A → PredSet A)
    (set : PredSet A) : Prop :=
  Subset (operator set) set

def Postfixpoint {A : Type u} (operator : PredSet A → PredSet A)
    (set : PredSet A) : Prop :=
  Subset set (operator set)

def FixedPoint {A : Type u} (operator : PredSet A → PredSet A)
    (set : PredSet A) : Prop :=
  Subset (operator set) set ∧ Subset set (operator set)

def addSeed {A : Type u} (seed : PredSet A) (operatorInput : PredSet A) : PredSet A :=
  fun x => seed x ∨ operatorInput x

theorem addSeedMonotone {A : Type u} (seed : PredSet A) :
    Monotone (addSeed seed) := by
  intro left right inclusion x membership
  cases membership with
  | inl seeded => exact Or.inl seeded
  | inr inLeft => exact Or.inr (inclusion inLeft)

def complement {A : Type u} (set : PredSet A) : PredSet A :=
  fun x => ¬set x

theorem complementNotMonotone : ¬Monotone (complement : PredSet Bool → PredSet Bool) := by
  intro monotone
  let empty : PredSet Bool := fun _ => False
  let full : PredSet Bool := fun _ => True
  have inclusion : Subset empty full := fun _ impossible => False.elim impossible
  have imageInclusion := monotone inclusion
  have inComplementFull :=
    imageInclusion (show complement empty true by simp [complement, empty])
  exact (show ¬complement full true by simp [complement, full]) inComplementFull

/-!
補集合は包含の向きを反転するため単調ではなく反単調です。作用素が不動点を偶然持つことと、全ての入力で
順序を保存することは別です。次章の一般定理は単調性を使って前不動点全体の下限と後不動点全体の上限を
再び前・後不動点にするため、この仮定を省けません。

## 要点

* 束の二項上限・下限は演算だけでなく最小上界・最大下界の普遍性を満たす。
* 完備格子は任意の族の上限と下限を持ち、空族から最下元・最上元を得る。
* 述語集合は包含順序、任意和、任意共通部分により完備格子をなす。
* 単調作用素は順序を保存し、反単調な補集合とは区別される。
* 前不動点 `F(X)⊆X`、後不動点 `X⊆F(X)`、不動点 `F(X)=X` は別の条件である。

## 研究史と文献案内

束の抽象理論は19世紀末から20世紀前半の順序・代数研究を経て形成されました。完備格子と不動点定理の
標準的な関係は [TAR55] を次章と合わせて参照してください。本章の述語集合は集合論的冪集合と同じ記法上の
役割を持ちますが、Leanでは `A→Prop` として表現し、基礎集合論の公理化そのものとはみなしません。

## 問題

### 二項演算から普遍性を復元する

`BinaryJoin` と `BinaryMeet` について、上界・下界条件と最小性・最大性を四本の推論規則に分けてください。
積集合や和集合の具体的要素を使う証明と、順序記法だけの証明を並べます。常に左引数を返す偽のjoinが
どの規則を破るかを比較不能な述語二つで示せば完了です。
最後に、外延的に同じ上限候補が反対称性によって等しくなる一意性証明を加えてください。

### 空族を含む任意上限・下限を計算する

三つの自然数述語から成る族を選び、`Supremum` と `Infimum` の所属条件を量化記号へ戻してください。
一要素族、空族、全述語から成る族について上限と下限を計算します。空虚な全称と存在不能をLean証明の
各分岐へ対応づけ、最上元と最大元を混同していないことを説明すれば完了です。
族の要素数ではなく量化範囲が普遍性を決めることも、各場合の定義展開から確認してください。

### 作用素の単調性を正例と反例で判定する

二項関係 `step` に対し `F(X)={start}∪{y∣∃x∈X.step(x,y)}` を定義し、単調性を証明してください。
補集合、集合差、定数作用素についても判定し、失敗するものには包含 `X⊆Y` と出力要素の反例を与えます。
前不動点と後不動点を一つずつ計算し、単調性とは異なる量化であることを示せば完了です。
-/

end FormalLab.Recursion.Lattices