import FormalLab.Logic.Equality

/-!
# 第20章：集合を述語として読む

集合を扱う最小の操作は、ある要素がその集合に属するかを問うことです。母集団を型 `A` として
固定すれば、部分集合 `S` は各 `x : A` に所属命題 `x ∈ S` を対応させる述語として読めます。
この見方では、包含は含意、共通部分は連言、和集合は選言へ分解されます。

本章では集合論全体を型理論へ置き換えるのではなく、固定した母型上の**述語集合**を構成します。
集合演算と外延性を既知の論理から導き、集合としての述語と、その述語を満たす値を保持する
部分型を区別します。後の像・逆像、関係、篩型を読むための共通語彙をここで整えます。

## 集合を要素が満たす条件で表す

母集団 `A` の部分集合 `S` は、各 `x ∈ A` について所属命題 `x ∈ S` を定めます。本章では
この特性述語を直接表現し、型 `α` 上の集合を述語 `α → Prop` として形式化します。`s x` は「`x` が `s` に属する」
という命題です。ここで `α` は議論する要素の**母型**です。集合だけを単独で持つのでは
なく、どの型の要素を集めているかが常に型に現れます。集合演算は論理結合子を点ごとに
使うだけです。

$$
\mathcal P(A)\;\widehat{=}\;A\to\mathsf{Prop},
\qquad
x\in S\;\widehat{=}\;S(x).
$$

ここで帽子付き等号は、Zermelo–Fraenkel集合論の冪集合と同一だという主張ではなく、本章で使う
固定母型上の述語表現を示します。この表現の下で包含と演算は

$$
S\subseteq T\;\Longleftrightarrow\;\forall x:A.\,S(x)\to T(x),
$$

$$
(S\cup T)(x)\;\Longleftrightarrow\;S(x)\lor T(x),
\quad
(S\cap T)(x)\;\Longleftrightarrow\;S(x)\land T(x)
$$

と読めます。

| 集合概念 | 要素ごとの論理式 |
|---|---|
| `s ⊆ t` | `∀ x, s x → t x` |
| `s ∪ t` | `fun x => s x ∨ t x` |
| `s ∩ t` | `fun x => s x ∧ t x` |
| `sᶜ` | `fun x => ¬s x` |


-/

namespace FormalLab.Mathematics.Sets

universe u

/-!
## 所属を述語の適用として表す

この表現では「集合を作る」ことは「所属条件を書く」ことです。列挙できない無限集合でも、
`fun n : Nat => n % 2 = 0` のように条件を述べられます。反対に、同じ型 `α` 上でも
異なる所属条件は異なる集合を定めます。
-/

/-- `α` の集合を、その所属述語として表す本章の定義です。 -/
def PredSet (α : Type u) :=
  α → Prop

/-- `s` の全要素が `t` にも属することを包含と定義します。 -/
def Subset {α : Type u} (s t : PredSet α) : Prop :=
  ∀ ⦃x⦄, s x → t x

/-- どの要素にも偽を返す空集合です。 -/
def Empty {α : Type u} : PredSet α :=
  fun _ => False

/-- どの要素にも真を返す全体集合です。 -/
def Universal {α : Type u} : PredSet α :=
  fun _ => True

/-- 所属を選言で定める和集合です。 -/
def Union {α : Type u} (s t : PredSet α) : PredSet α :=
  fun x => s x ∨ t x

/-- 所属を連言で定める共通部分です。 -/
def Intersection {α : Type u} (s t : PredSet α) : PredSet α :=
  fun x => s x ∧ t x

/-- 所属を否定して得る補集合です。 -/
def Complement {α : Type u} (s : PredSet α) : PredSet α :=
  fun x => ¬s x

/-- 指定した一点だけを含む一元集合です。 -/
def Singleton {α : Type u} (chosen : α) : PredSet α :=
  fun x => x = chosen

/-- 自然数上の偶数全体を、所属条件で直接定めます。 -/
def EvenNumbers : PredSet Nat :=
  fun n => n % 2 = 0

example : EvenNumbers 4 := rfl
example : ¬EvenNumbers 3 := by
  change ¬(3 % 2 = 0)
  decide

/-!
## 法則：論理の証明を集合の証明として再利用する

包含 `Subset s t` は、集合を新しい値へ変換する関数ではありません。`s x` という所属証明を
受け取るたびに `t x` を返す、要素ごとの含意です。このため包含の反射性は恒等関数、
推移性は証明関数の合成と同じ形になります。
-/

/-- 集合包含の反射性です。 -/
theorem subsetReflexive {α : Type u} (s : PredSet α) : Subset s s :=
  fun {_} membership => membership

/-- 集合包含の推移性です。 -/
theorem subsetTransitive {α : Type u} {s t u : PredSet α}
    (st : Subset s t) (tu : Subset t u) : Subset s u :=
  fun {_} membership => tu (st membership)

/-- 一元集合が `s` に含まれることと、その一点が `s` に属することは同値です。 -/
theorem singletonSubset_iff {α : Type u} {chosen : α} {s : PredSet α} :
    Subset (Singleton chosen) s ↔ s chosen := by
  constructor
  · intro subset
    exact subset rfl
  · intro membership _ equality
    cases equality
    exact membership

/-- 要素ごとの所属が同値なら、二つの述語集合は等しい。 -/
theorem extensionality {α : Type u} {s t : PredSet α}
    (sameMembers : ∀ x, s x ↔ t x) : s = t := by
  funext x
  exact propext (sameMembers x)

/-- 和集合の交換性は選言の交換性です。 -/
theorem unionCommutative {α : Type u} (s t : PredSet α) : Union s t = Union t s := by
  apply extensionality
  intro x
  constructor
  · intro membership
    exact Or.elim membership Or.inr Or.inl
  · intro membership
    exact Or.elim membership Or.inr Or.inl

/-- 共通部分の交換性は、所属証明の二成分を入れ替えて示します。 -/
theorem intersectionCommutative {α : Type u} (s t : PredSet α) :
    Intersection s t = Intersection t s := by
  apply extensionality
  intro x
  constructor <;> intro membership
  · exact ⟨membership.2, membership.1⟩
  · exact ⟨membership.2, membership.1⟩

/-!
`unionCommutative` の証明は、集合の等式を二段階で分解します。まず `funext` に対応して任意の
要素 `x` を固定し、次に `propext` に対応して二つの所属命題の同値を示します。その内部は
選言の交換だけです。この「集合等式 → 所属同値 → 命題論理」という翻訳が、述語集合を
使う際の基本手順です。

De Morgan則のうち、和集合の補集合は構成的に共通部分へ分配できます。
-/

theorem complementUnion {α : Type u} (s t : PredSet α) :
    Complement (Union s t) = Intersection (Complement s) (Complement t) := by
  apply extensionality
  intro x
  constructor
  · intro notEither
    exact ⟨fun sx => notEither (Or.inl sx), fun tx => notEither (Or.inr tx)⟩
  · intro ⟨notS, notT⟩ either
    exact either.elim notS notT

/-- 排中律を使えば、集合とその補集合の和は全体集合になります。 -/
theorem unionComplement {α : Type u} (s : PredSet α) :
    Union s (Complement s) = Universal := by
  apply extensionality
  intro x
  constructor
  · intro _
    exact True.intro
  · intro _
    exact Classical.em (s x)

/-!
## 述語集合と集合論

集合の外延性は、所属が同値なら述語として等しいという `funext` と `propext` の合成です。
また補集合の定義 `¬s x` 自体は構成的ですが、`s ∪ sᶜ = Universal` のような法則は
全ての所属命題について排中律を使います。演算の定義と法則の論理的強さを分けます。

mathlibの `Set α` も述語を基礎にしますが、ここでは所属の仕組みを定義から追えるよう
`PredSet` を使います。

述語集合 `PredSet α` と、後に扱う篩型 `{x : α // s x}` も区別します。前者は所属を尋ねる
述語、後者は要素と所属証明を組にした型です。集合の要素を実際の入力として要求する段階で、
この二つの見方を橋渡しします。

## 要点

* 型 `α` 上の集合は所属述語 `α → Prop` として表せる。
* 包含は要素ごとの含意、和・共通部分・補集合は選言・連言・否定である。
* 集合の等式は、各要素について所属命題が同値であることへ分解する。
* 集合演算の定義が構成的でも、特定の法則が古典論理を要求する場合がある。
* 述語としての集合と、所属証明を持つ要素の型は同じ対象ではない。

## 研究史と文献案内

集合論はCantorとDedekindの1870年代以後の研究から発展し、Zermeloは1908年に公理化を
提示しました [ZER08]。本章の `PredSet α` は一つの既定の型の部分を特性述語で表すもので、
Zermelo集合論の累積的な集合宇宙ではありません。歴史的展開は付録Cの二次文献、型理論内の
集合・型・setoidの差は [ML84] を参照してください。

## 問題

### 集合演算を論理式へ翻訳する

`Subset s t` と `Intersection s (Union t u) x` を、集合記号を使わない量化・含意・連言・選言の
式へ翻訳せよ。次に積集合の交換性を連言の交換から証明し、集合の証明が要素を固定した命題の
証明へ還元される順序を示す。

同じ方法で `Subset (Singleton x) s ↔ s x` をLeanで証明する。数式中の各推論が、関数適用、
等式による書換え、含意のどれとして現れるかを対応づけること。

### 外延性が重ねて使われる箇所を追う

二つの述語 `s t : α → Prop` が同じ集合を表すための条件を述べ、関数外延性と命題外延性を
どの順に使えば `s = t` が得られるかを導出せよ。要素ごとの同値、命題の等式、関数の等式を
混同せず、三段階に分けて書くこと。

Leanの集合が述語として表現されることから従う実装上の説明と、数学における集合外延性の原理を
区別する。どの段階がLeanの表現選択に依存するかを指摘できれば完了である。

### 補集合と古典論理の境目を特定する

`s ∪ sᶜ = Universal` の通常の証明を要素ごとの命題へ展開し、排中律を用いる正確な一行を指せ。
一方、`s ∩ sᶜ = Empty` は同じ古典原理なしに証明できることを示し、否定の導入と排中律の違いを
説明する。

最後に、構成的に証明できる包含関係と、古典論理を仮定して初めて等号まで強められる関係を一つ
ずつ挙げる。古典性を集合記号の見かけではなく、対応する論理式から判定すること。
-/

end FormalLab.Mathematics.Sets