import FormalLab.Foundation.Universes
import FormalLab.Mathematics.FunctionProperties
import FormalLab.Mathematics.Orders

/-!
# 第25章：有限性・可算性・基数・無限

自然数と偶数にはどちらも無限に多くの要素があります。偶数は自然数の一部分ですが、写像
`n ↦ 2n` によって自然数全体と一対一に対応します。一方、自然数から真偽値列全体への列挙を
どのように選んでも、その一覧に現れない列を対角線上の値を反転して構成できます。

本章では要素数を数値へ還元せず、単射・全射・全単射の存在によって型の大きさを比較します。
有限、可算以下、可算無限を区別し、Cantorの対角線論法を`Bool`値関数についてLeanで証明します。
最後に、基数としての大きさとLeanの宇宙レベルが異なる分類であることを明確にします。

## 大きさを写像で比較する

型 `A` から `B` への単射があれば、`A` の異なる要素を潰さず `B` の中へ配置できます。このとき
`|A| ≤ |B|` と読みます。全単射があれば `|A| = |B|` と読みますが、これは`A = B`という型の
等式ではありません。大きさが同じでも、要素の意味や演算は異なり得ます。

$$
\begin{aligned}
|A|\le |B|&\;:\!\Longleftrightarrow\;\exists f:A\to B.\;\mathsf{Injective}(f),\\
|A|=|B|&\;:\!\Longleftrightarrow\;\exists f:A\to B.\;\mathsf{Bijective}(f).
\end{aligned}
$$

有限性は、ある自然数 `n` に対して`A`が`0, …, n-1`と全単射になることです。本章では標準の
`Fin n`を再実装せず、必要な比較を関数の性質として直接表します。
-/

namespace FormalLab.Mathematics.Cardinality

universe u v

open FormalLab.Mathematics.FunctionProperties

def CardinalLE (A : Type u) (B : Type v) : Prop :=
  ∃ f : A → B, IsInjective f

def Equinumerous (A : Type u) (B : Type v) : Prop :=
  ∃ f : A → B, IsBijective f

/-- ある有限順序型 `Fin n` と全単射である、という有限性です。 -/
def IsFinite (A : Type u) : Prop :=
  ∃ n : Nat, Equinumerous A (Fin n)

def AtMostCountable (A : Type u) : Prop :=
  CardinalLE A Nat

def CountablyInfinite (A : Type u) : Prop :=
  Equinumerous A Nat

def boolToFin : Bool → Fin 2
  | false => 0
  | true => 1

theorem boolToFinBijective : IsBijective boolToFin where
  injective := by
    intro a b equal
    cases a <;> cases b <;> simp [boolToFin] at equal ⊢
  surjective := by
    rintro ⟨value, bound⟩
    have alternatives : value = 0 ∨ value = 1 := by omega
    rcases alternatives with rfl | rfl
    · exact ⟨false, rfl⟩
    · exact ⟨true, rfl⟩

theorem boolIsFinite : IsFinite Bool :=
  ⟨2, boolToFin, boolToFinBijective⟩

/-! ## 偶数は自然数と同じ基数を持つ -/

def EvenNat := {n : Nat // n % 2 = 0}

def toEven (n : Nat) : EvenNat :=
  ⟨2 * n, by simp⟩

def fromEven (n : EvenNat) : Nat :=
  n.val / 2

theorem toEvenInjective : IsInjective toEven := by
  intro a b equal
  have values : 2 * a = 2 * b := congrArg Subtype.val equal
  exact Nat.mul_left_cancel (by decide) values

theorem fromEvenToEven (n : Nat) : fromEven (toEven n) = n := by
  simp [fromEven, toEven]

theorem toEvenFromEven (n : EvenNat) : toEven (fromEven n) = n := by
  apply Subtype.ext
  exact Nat.mul_div_cancel' (Nat.dvd_of_mod_eq_zero n.property)

theorem evenCountablyInfinite : CountablyInfinite EvenNat := by
  refine ⟨fromEven, ⟨leftInverseGivesInjective toEvenFromEven, ?_⟩⟩
  intro n
  exact ⟨toEven n, fromEvenToEven n⟩

theorem evenAtMostCountable : AtMostCountable EvenNat := by
  refine ⟨Subtype.val, ?_⟩
  intro a b equal
  exact Subtype.ext equal

/-!
`fromEvenToEven` と `toEvenFromEven` は、二つの関数が互いに逆であることを各向きに証明します。
したがって `evenCountablyInfinite` は自然数と偶数の全単射を実際に構成しています。両方向の
単射から全単射を得るCantor–Schröder–Bernstein定理は一般には別の証明を要し、任意の二単射が
互いの逆になるわけではありません。

有限集合が真部分集合と同じ大きさを持たないのに対し、自然数は偶数という真部分集合と同じ大きさを
持ちます。この性質は無限性の一つの特徴づけですが、基礎理論によってDedekind無限と他の無限概念の
関係には選択原理が関与します。ここでは「無限」を無条件に一つの定義へ固定しません。

## 対角線上で列挙から逃れる

`α → Bool` は、`α`で添字づけられた真偽値列です。関数`table : α → (α → Bool)`を、各`a`に
一行の真偽値列を割り当てる表とみなします。対角列`diagonal a = !(table a a)`は、行`a`と位置`a`で
必ず異なります。したがってどの行とも等しくありません。
-/

def diagonal {α : Type u} (table : α → α → Bool) : α → Bool :=
  fun a => !(table a a)

theorem diagonalDiffers {α : Type u} (table : α → α → Bool) (a : α) :
    diagonal table ≠ table a := by
  intro equal
  have point := congrFun equal a
  simp [diagonal] at point

theorem noSurjectionToBoolPowers {α : Type u} :
    ¬ ∃ table : α → (α → Bool), IsSurjective table := by
  rintro ⟨table, surjective⟩
  obtain ⟨a, equal⟩ := surjective (diagonal table)
  exact diagonalDiffers table a equal.symm

/-!
この証明は「無限だから大きい」という印象に依存しません。型`α`が有限でも無限でも、
`α → Bool`を`α`で全射的に列挙することはできません。各候補行へ一か所で異なる列を同じ表から
構成するためです。`Bool`値関数は部分集合の特性関数に相当しますが、一般の`Prop`値述語と
`Bool`を同一視せず、ここでは計算可能な反転を使うため`Bool`を選んでいます。

## 可算以下と可算無限を区別する

`AtMostCountable A`は`A`から自然数への単射を要求します。空型や有限型も可算以下です。
`CountablyInfinite A`は自然数との全単射を要求するため、有限型を除外します。「可算」という語は
文献によって有限を含む場合と可算無限だけを指す場合があるので、本書では二語を使い分けます。
-/

theorem emptyAtMostCountable : AtMostCountable Empty := by
  refine ⟨(fun impossible : Empty => nomatch impossible), ?_⟩
  intro a _b _equal
  nomatch a

theorem boolAtMostCountable : AtMostCountable Bool := by
  refine ⟨fun b => if b then 1 else 0, ?_⟩
  intro a b equal
  cases a <;> cases b <;> simp at equal ⊢

/-!
## 基数と宇宙レベルは異なる

`Type u`の宇宙レベルは、型式をどのsortへ分類するかを管理します。基数はある型の要素が別の型へ
単射・全単射で対応するかを測ります。同じ宇宙に異なる基数の型が多数あり、宇宙レベルが高い型でも
要素を一つしか持たない場合があります。したがって`Type 1`を「Type 0より要素数が大きい型」とは読みません。

宇宙は全ての小さい型を型検査上どこへ置くかという問題に答え、基数は固定した二型の要素対応に
答えます。Cantorの定理から冪型が元の型より真に大きいことを論じる際にも、その命題を述べる宇宙と、
比較対象の基数を別々に追跡します。

## 要点

* 型の大きさは単射で比較し、全単射で同じ基数であることを表す。
* 可算以下は有限型を含み、可算無限は自然数との全単射を要求する。
* 無限型は真部分型と全単射になり得るが、無限概念間の同値には基礎理論上の仮定が関与する。
* 対角線論法は任意の列挙候補から、その一覧にない対象を構成する。
* 基数は要素対応、Leanの宇宙レベルは型式の分類であり、同じ尺度ではない。

## 研究史と文献案内

Cantorの1874年論文 [CAN74] は代数的数の可算性と実数の非可算性を扱います。本章の一般化された
真偽値列の対角線証明や、後世の基数算術を同論文の記法へそのまま帰属させません。Dedekindの
無限系 [DED88]、Zermeloの集合論公理化 [ZER08] とも基礎づけの役割を分けて読みます。

## 問題

### 単射・全射・全単射で三種類の比較を作る

`Bool`、`Nat`、`EvenNat`の各組について単射または全射を具体的に構成し、全単射まで得られる組を
判定してください。関数の始域・終域を省略せず、同じ式でも終域を変えると全射性が変わる例を含めます。
「部分集合だから小さい」という推論が無限の場合に不十分な理由を`toEven`から説明します。

### 対角線証明を表として追跡する

三行三列の有限な真偽値表を一つ作り、対角成分を反転した列を書いてください。その列が各行と異なる
位置を一つずつ示します。次に`diagonalDiffers`の`congrFun`がこの一点比較へ対応することを説明し、
有限表では新しい列が表の列数を越えるだけで、一般定理の論理が有限性に依存しないことを確認します。

### 可算性と宇宙を別々の判断へ戻す

`Nat : Type`、`Type : Type 1`、`AtMostCountable Nat`を三つの異なる主張として展開してください。
宇宙レベルを一段持ち上げた`ULift Nat`と`Nat`の間に全単射を構成し、宇宙が変わっても要素対応が
保存される例を示します。[CAN74]の実数非可算性と本章の`Bool`冪型定理の論証形式も比較します。
-/

end FormalLab.Mathematics.Cardinality