import FormalLab.Mathematics.Relations
import FormalLab.Mathematics.Sets

/-!
# 第24章：順序・上限・下限・極大原理

自然数の `≤` では二数を比較できます。しかし「ある集合の全要素以上である」「そのような上界のうち
最小である」「これ以上大きい要素がない」は、いずれも別の量化を持つ主張です。たとえば集合
`{2, 5}` の最大元は `5` ですが、実数の開区間 `{x ∣ x < 1}` には上限 `1` があっても最大元はありません。

本章では半順序を前提に、上界・下界、最大元・極大元、上限・下限を順に定義します。述語集合を
包含で順序づける具体例では、和集合が上限、共通部分が下限になります。最後にZornの補題の主張を
分解し、有限探索で最大元を見つけることと、選択原理を用いる一般定理を混同しないようにします。

## 上にあることと、最も上にあること

半順序 `(A, ≤)` と部分集合 `S` を固定します。`u` が `S` の**上界**であるとは、全ての
`x ∈ S` について `x ≤ u` が成り立つことです。上限 `s` は上界であるだけでなく、任意の上界
`u` に対して `s ≤ u` を満たします。

$$
\begin{aligned}
\mathsf{UpperBound}(S,u)
  &\;\Longleftrightarrow\;\forall x:A.\;x\in S\to x\le u,\\
\mathsf{IsSupremum}(S,s)
  &\;\Longleftrightarrow\;\mathsf{UpperBound}(S,s)\land
    \forall u:A.\;\mathsf{UpperBound}(S,u)\to s\le u.
\end{aligned}
$$

最大元は集合自身に属する上界です。極大元は、自分より真に大きい集合内の要素がない点です。
全順序では両者の差が見えにくい一方、部分順序では複数の互いに比較不能な極大元が存在できます。
-/

namespace FormalLab.Mathematics.Orders

universe u

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

def UpperBound {α : Type u} (le : α → α → Prop) (s : PredSet α) (u : α) : Prop :=
  ∀ ⦃x⦄, s x → le x u

def LowerBound {α : Type u} (le : α → α → Prop) (s : PredSet α) (l : α) : Prop :=
  ∀ ⦃x⦄, s x → le l x

def IsSupremum {α : Type u} (le : α → α → Prop) (s : PredSet α) (a : α) : Prop :=
  UpperBound le s a ∧ ∀ u, UpperBound le s u → le a u

def IsInfimum {α : Type u} (le : α → α → Prop) (s : PredSet α) (a : α) : Prop :=
  LowerBound le s a ∧ ∀ l, LowerBound le s l → le l a

def IsMaximum {α : Type u} (le : α → α → Prop) (s : PredSet α) (a : α) : Prop :=
  s a ∧ UpperBound le s a

def IsMaximal {α : Type u} (le : α → α → Prop) (s : PredSet α) (a : α) : Prop :=
  s a ∧ ∀ ⦃b⦄, s b → le a b → le b a

/-!
最大元は上限の条件を自動的に満たします。最大元 `a` 自身が `S` に属するため、任意の上界
`u` に上界性を `a` で適用すれば `a ≤ u` が得られるからです。極大性も従いますが、こちらは
比較 `a ≤ b` を仮定した後、最大性から逆向き `b ≤ a` を得ます。
-/

/-- 最大元は、その集合の上限でもあります。 -/
theorem maximumIsSupremum {α : Type u} {le : α → α → Prop}
    {s : PredSet α} {a : α} (maximum : IsMaximum le s a) :
    IsSupremum le s a :=
  ⟨maximum.2, fun _ upper => upper maximum.1⟩

/-- 最大元は極大元です。逆向きは一般の半順序では成り立ちません。 -/
theorem maximumIsMaximal {α : Type u} {le : α → α → Prop}
    {s : PredSet α} {a : α} (maximum : IsMaximum le s a) :
    IsMaximal le s a := by
  constructor
  · exact maximum.1
  · intro b hb _
    exact maximum.2 hb

/-- 反対称な関係では、同じ集合の上限は一意です。 -/
theorem supremumUnique {α : Type u} {le : α → α → Prop}
    (antisymmetric : FormalLab.Mathematics.Relations.IsAntisymmetric le)
    {s : PredSet α} {a b : α}
    (ha : IsSupremum le s a) (hb : IsSupremum le s b) : a = b :=
  antisymmetric (ha.2 b hb.1) (hb.2 a ha.1)

/-! ## 述語集合の包含順序では和集合が上限になる -/

def Subset {α : Type u} (s t : PredSet α) : Prop :=
  ∀ ⦃x⦄, s x → t x

def Union {α : Type u} (family : PredSet (PredSet α)) : PredSet α :=
  fun x => ∃ s, family s ∧ s x

def Intersection {α : Type u} (family : PredSet (PredSet α)) : PredSet α :=
  fun x => ∀ s, family s → s x

/-!
述語集合の包含は次の式で定義します。

$$
S\subseteq T\;:\!\Longleftrightarrow\;\forall x.\,x\in S\to x\in T.
$$

この順序では、任意の集合族 $\mathcal F$ について

$$
\sup \mathcal F=\bigcup\mathcal F,
\qquad
\inf \mathcal F=\bigcap\mathcal F
$$

となります。以下の二証明は、この等式を要素ごとの含意へ展開したものです。
-/

theorem unionIsSupremum {α : Type u} (family : PredSet (PredSet α)) :
    IsSupremum Subset family (Union family) := by
  constructor
  · intro s hs x hx
    exact ⟨s, hs, hx⟩
  · intro upper upperBound x
    rintro ⟨s, hs, hx⟩
    exact upperBound hs hx

theorem intersectionIsInfimum {α : Type u} (family : PredSet (PredSet α)) :
    IsInfimum Subset family (Intersection family) := by
  constructor
  · intro s hs x hx
    exact hx s hs
  · intro lower lowerBound x hx s hs
    exact lowerBound hs hx

/-!
`unionIsSupremum` の前半は、各集合 `s` が和集合に含まれることを示します。後半は、族の全てを
含む任意の集合 `upper` が和集合も含むことを示します。これが「上界」と「最小の上界」の二条件です。
和集合の具体的な要素表現は証明に使いますが、上限の定義自体は要素の格納方法を要求しません。

空でない有限集合の最大値を計算する関数と、任意の半順序で上限が存在するという命題は別です。
上の定理が成立するのは、述語集合の包含順序が任意の和・共通部分を持つからです。自然数の通常順序では、
自然数全体に自然数値の上界はありません。

## 最大元と極大元を反例で分ける

二つの真偽値の対を成分ごとに順序づけると、`(true,false)` と `(false,true)` は比較不能です。
部分集合から最上点 `(true,true)` を除けば、この二点はどちらも極大ですが最大元ではありません。
「極大」は局所的に先へ進めないこと、「最大」は全ての要素以上であることを表します。
-/

def BoolLe : Bool → Bool → Prop
  | false, _ => True
  | true, true => True
  | true, false => False

def PairLe (x y : Bool × Bool) : Prop :=
  BoolLe x.1 y.1 ∧ BoolLe x.2 y.2

def Boundary : PredSet (Bool × Bool) :=
  fun p => p ≠ (true, true)

example : IsMaximal PairLe Boundary (true, false) := by
  constructor
  · simp [Boundary]
  · intro b hb hab
    rcases b with ⟨b₁, b₂⟩
    cases b₁ <;> cases b₂ <;> simp [PairLe, BoolLe, Boundary] at hb hab ⊢

example : ¬ IsMaximum PairLe Boundary (true, false) := by
  intro maximum
  have comparison := maximum.2 (show Boundary (false, true) by simp [Boundary])
  exact comparison.2

/-!
最大元なら極大元ですが、上の境界集合では逆が失敗します。この正例と反例により、定義中の
全称量化の位置が実際に異なることが分かります。名称の「max」だけで証明を選ばず、比較対象が
任意の集合内要素なのか、自分以上の要素だけなのかを読みます。

## 鎖とZornの補題

部分集合 `C` が**鎖**であるとは、任意の二要素が比較可能であることです。Zornの補題は、空でない
半順序集合で全ての鎖が上界を持つなら極大元が存在すると述べます。結論は最大元でも全順序でも
ありません。また「各有限鎖の上界」ではなく、任意の鎖の上界を仮定します。
-/

def IsChain {α : Type u} (le : α → α → Prop) (s : PredSet α) : Prop :=
  ∀ ⦃x⦄, s x → ∀ ⦃y⦄, s y → le x y ∨ le y x

def ZornConclusion {α : Type u} (le : α → α → Prop) : Prop :=
  (∃ _x : α, True) →
  (∀ chain : PredSet α, IsChain le chain → ∃ u, UpperBound le chain u) →
  ∃ m, IsMaximal le (fun _ => True) m

/-!
半順序を仮定したZornの補題の現代的な形は、次の含意です。

$$
\left[
  A\ne\varnothing\;\land\;
  \forall C\subseteq A.\;
    \mathsf{Chain}(C)\to\exists u:A.\;\mathsf{UpperBound}(C,u)
\right]
\Longrightarrow
\exists m:A.\;\mathsf{Maximal}(A,m).
$$

`ZornConclusion` は仮定と結論の形をLeanで記録しただけで、証明ではありません。一般のZornの補題を
証明するには、選択公理と同値な原理をどこで利用するかを明示する必要があります。有限型の探索で
極大元を見つけられることを、その一般定理の証明と取り違えません。

## 要点

* 上界は集合の全要素以上、上限は全ての上界以下である上界である。
* 最大元は集合に属する上界、極大元は集合内で真に上へ進めない要素である。
* 述語集合の包含順序では、任意和が上限、任意共通部分が下限になる。
* 鎖は任意の二要素が比較可能な部分集合であり、半順序全体が全順序である必要はない。
* Zornの補題は鎖の上界から極大元を得る選択原理で、有限探索とは別である。

## 研究史と文献案内

Zornの1935年論文 [ZOR35] は極大原理を超限代数の方法として提示しました。現在の教科書でいう
Zornの補題と選択公理の同値性は、採用する集合論と定式化を明示して読む必要があります。
順序・上限・完備格子の標準的定式化は [MAC98] の順序的議論および後の不動点章へ接続します。

## 問題

### 上限の二条件を別々に検査する

自然数の有限部分集合を一つ選び、上界を三つ挙げ、そのうち上限だけが満たす追加条件を書いてください。
次に空集合と自然数全体について上界・上限の有無を調べます。空虚に成立する量化と、候補となる自然数が
存在しない場合を分け、`UpperBound` と `IsSupremum` のどちらの成分で失敗するかを示します。

### 最大と極大の差を有限半順序で可視化する

`Boundary` の四候補をHasse図に描き、各点が極大・最大・最小のどれかを判定してください。
別の三要素半順序をLeanで定義し、極大元が二つある例と最大元が一つある例を作ります。偽の判定には
比較不能な二点を具体的に挙げ、反対称性の失敗と混同していないことも確認します。最後に、全順序なら
有限部分集合の極大元が最大元になることを証明し、どの段階で比較可能性を使ったかを示せば完了です。

### Zornの仮定を有限性で弱めてはならない理由を述べる

`ZornConclusion` の各量化を通常の数式へ戻し、空でないこと、鎖、上界、極大元の役割を説明します。
有限半順序では極大元を探索できる証明を帰納法で与え、その証明が無限の場合に停止しない箇所を特定します。
[ZOR35] の主張と現代的定式化を比較し、歴史的原文と後世の同値定理を区別してください。
-/

end FormalLab.Mathematics.Orders