import FormalLab.Logic.Equality

/-!
# 付録A：数学的記法とLean表現の対照

数学・論理学・型理論の論文では、式の意味だけでなく、どのレベルの言語で書かれた記号かを
判別する必要があります。本付録は数学的な定義・判断・推論規則をLean 4の宣言へ翻訳するための
参照表です。個々の記号を暗記するより、同じ構造を二つの表記で往復してください。

## 対象言語、メタ言語、判断

型付け判断

```text
Γ ⊢ t : A
```

は「文脈 `Γ` の下で項 `t` は型 `A` を持つ」という**判断**（judgment）です。通常、
`⊢` は対象言語の項ではなく、形式体系について述べるメタ言語の記号です。Leanソースでは
kernelが宣言を検査する場面と、対象言語の判断を帰納的な命題として表す場面を区別します。

```lean
#check fun x : Nat => x
-- Lean自身が右の項の型を報告するメタレベルのコマンド

-- STLCなどを研究するときは、HasType Γ t A : Prop のように
-- 対象言語の判断をLean内の命題として定義できる。
```

論文で頻出する判断には次があります。

| 数学的記法 | 読み | Leanで対応するもの |
|---|---|---|
| `Γ ctx` | `Γ` は整形式な文脈 | 文脈を表す型と整形式性の述語 |
| `Γ ⊢ A type` | `A` は型 | `A : Type u`、または対象体系の形成判断 |
| `Γ ⊢ t : A` | `t` は `A` の項 | Lean自身の型検査、または `HasType Γ t A` |
| `Γ ⊢ t ≡ u : A` | 定義的に等しい | kernelの変換可能性。一般には項として保持しない |
| `Γ ⊢ p : t = u` | 等式命題の証明 | `p : t = u` |

## 束縛、関数、依存積

| 数学的記法 | Lean 4 | 意味 |
|---|---|---|
| `λx : A. t` | `fun x : A => t` | ラムダ抽象 |
| `f a` | `f a` | 関数適用 |
| `A → B` | `A → B` | 非依存関数型 |
| `Π(x : A). B(x)` | `(x : A) → B x` | 依存関数型・Π型 |
| `∀x : A. P(x)` | `∀ x : A, P x` | 終域が `Prop` のΠ型 |
| `t[x := a]` | Leanが適用・代入で処理 | 捕獲を避ける代入 |

関数の導入規則は次の推論規則で表せます。

```text
Γ, x : A ⊢ t : B(x)
────────────────────────  Π-introduction
Γ ⊢ λx : A. t : Π(x : A). B(x)
```

Leanでは前提の導出をラムダ本体として書き、規則名を明示せず構文で導入します。
-/

namespace FormalLab.Appendix.Notation

universe u v

/-- ラムダ式 `λx : A. x` と同じ項です。 -/
def paperIdentity {A : Type u} : A → A :=
  fun x : A => x

/-- ラムダ式 `λf. λg. λx. f (g x)` と束縛順を対応させます。 -/
def paperCompose {A : Type u} {B : Type v} {C : Type}
    (f : B → C) (g : A → B) : A → C :=
  fun x => f (g x)

/-!
## 依存対、存在、部分型

| 数学的記法 | Lean 4 | 保持する情報 |
|---|---|---|
| `Σ(x : A). B(x)` | `Sigma fun x : A => B x` | `x` と `B x` の計算データ |
| `∃x : A. P(x)` | `∃ x : A, P x` | 命題内の証人と証明 |
| `{x : A ∣ P(x)}` | `{x : A // P x}` | 値 `x` と証明 `P x` |
| `A × B` | `A × B` | 非依存な二成分 |

論文によって `{x : A ∣ P(x)}` は集合の内包表記を意味し、値と証明を持つ型を意味しない
場合があります。本文が集合論・型理論・プログラミング言語理論のどのメタ理論を採用して
いるか確認します。本書では述語集合 `A → Prop` とLeanの `Subtype` を明示的に区別します。

## 論理結合子と証明項

| 論文の式 | Leanの型 | 証明の標準形 |
|---|---|---|
| `P ⇒ Q` | `P → Q` | `fun p => q` |
| `P ∧ Q` | `P ∧ Q` | `⟨p, q⟩` |
| `P ∨ Q` | `P ∨ Q` | `Or.inl p` または `Or.inr q` |
| `¬P` | `¬P`、定義上 `P → False` | `fun p => contradiction` |
| `P ⇔ Q` | `P ↔ Q` | 二方向の含意 |
| `⊤`, `⊥` | `True`, `False` | `True.intro`、構成子なし |

自然演繹の導入・除去規則は、Leanでは帰納型の構成子と再帰・場合分けに対応します。たとえば
連言除去 `P ∧ Q ⊢ P` は第一射影です。
-/

theorem conjunctionElimination {P Q : Prop} : P ∧ Q → P :=
  fun proof => proof.1

/-!
## 三種類の「同じ」

論文を読む際に最も重要な区別の一つです。

| 記法 | 典型的意味 | Lean |
|---|---|---|
| `t ≡ u`、`t ≡β u` | 定義展開・簡約による変換可能性 | kernelの定義的等しさ |
| `t =_A u`、`t = u : A` | 型 `A` 内の同一性命題 | `t = u` |
| `P ↔ Q`、`P ⇔ Q` | 論理的同値 | `P ↔ Q` |

著者によって `=` をメタレベルの構文同一性、定義的等しさ、対象理論内の等式のいずれにも
使うため、冒頭のnotation節を確認します。本書は定義的等しさを説明文では `≡`、命題的
等しさをLeanと同じ `=` で表します。
-/

example : (fun n : Nat => n + 1) 2 = 3 := rfl

example {A : Type u} (x y : A) (h : x = y) (P : A → Prop) : P x → P y :=
  fun px => h ▸ px

/-!
## 推論規則とLeanの帰納的定義

推論規則

```text
premise₁    premise₂
────────────────── name
    conclusion
```

は「前提の導出から結論の導出を作る」構成子として読めます。規則が複数あれば帰納型の
構成子が複数あり、導出についての証明はその証拠に対する帰納法になります。この対応は
構文論・操作的意味論・型システムの論文をLeanへ移す基本手順です。

## 集合、関係、関数

| 数学的記法 | 読み | 本書のLean表現 |
|---|---|---|
| `x ∈ S` | `x` は `S` に属する | `S x`（`S : A → Prop`） |
| `S ⊆ T` | 包含 | `∀ ⦃x⦄, S x → T x` |
| `f[S]` | `S` の像 | `fun y => ∃ x, S x ∧ f x = y` |
| `f⁻¹[T]` | `T` の逆像 | `fun x => T (f x)` |
| `x R y`、`R(x,y)` | 二項関係 | `R x y`（`R : A → A → Prop`） |
| `f : A ↪ B` | 単射（流儀による） | `f : A → B` と単射性の証明 |
| `f : A ≃ B` | 同値・全単射（文脈依存） | 関数と逆・法則を持つ構造 |

## 圏論と普遍性

| 数学的記法 | 読み | `Type` と関数での実例 |
|---|---|---|
| `f : A → B`、`A \xrightarrow{f} B` | 射 | 関数 `f : A → B` |
| `g ∘ f` | 先に `f`、次に `g` | `g ∘ f` |
| `1_A`、`id_A` | 恒等射 | `id` |
| `Hom_C(A,B)`、`C(A,B)` | 射の集まり | `A → B` |
| `A × B` | 積対象 | 射影と対化を伴う直積型 |
| `A + B`、`A ⨿ B` | 余積対象 | 入射と余対化を伴う直和型 |
| `Cᵒᵖ` | 反対圏 | 射の向きと合成順を反転した圏 |

可換図式は、同じ始域と終域を持つ二つの合成が等しいという方程式の集まりです。図の形だけを
読むのではなく、各経路を合成式へ直し、Leanでは関数等式または射の等式として証明します。

## 宇宙と暗黙の前提

論文の `Type`、`𝒰`、`Set` は体系により意味が違います。Leanでは
`Prop = Sort 0`、`Type u = Sort (u + 1)` です。宣言

```lean
def id {A : Type u} (x : A) : A := x
```

には宇宙引数 `u` と暗黙の型引数 `A` があります。`#check @id` のように `@` を付けると
暗黙引数を観察できます。論文でも「任意の宇宙」「小さい型」「局所的に小さい圏」などの
サイズ条件を定理の仮定として数えます。

## 読解の手順

1. 記号の属するレベルを判定する：対象言語の項か、判断か、メタ定理か。
2. 束縛子のスコープと各変数の領域を補う。
3. 定義的等しさ、命題的等しさ、同値を区別する。
4. 推論規則を「前提の証拠から結論の証拠を作る関数」として読む。
5. 暗黙の宇宙・型・構造引数を列挙する。
6. 数式の各成分をLean宣言の引数・結果型・証明本体へ対応させる。
7. Leanで検査した後、コードを隠して数学的定義と導出を再構成する。
-/

end FormalLab.Appendix.Notation