import FormalLab.Bridges.CartesianClosedCategories
import FormalLab.TypeTheory.StructuralRules

/-!
# 第71章：単純型付きラムダ計算の圏論的意味論——判断を射へ移す

単純型付きラムダ計算の判断 `Γ⊢t:A` は、項が文脈 `Γ` の変数を使って型 `A` の値を作ることを述べます。
デカルト閉圏では、文脈を有限積の対象 `⟦Γ⟧`、型を対象 `⟦A⟧`、判断を射

$$
\llbracket t\rrbracket:
\llbracket\Gamma\rrbracket\longrightarrow\llbracket A\rrbracket.
$$

として解釈できます。変数は積の射影、適用は評価射、ラムダ抽象はカリー化になります。項の代入は射の合成へ
移り、β・η等式は指数対象のβ・η則から従います。

本章では最初に `Type` の標準モデルを完全に計算可能な形で実装します。次に一般のデカルト閉圏で各型付け規則を
射として再構成します。構文、型判断、意味対象、意味射の四層を分け、Lean自身の関数を対象言語の項と同一視
しないように進めます。

## 単純型を実際の型へ解釈する

原子型の解釈として型 `Base` を一つ選びます。関数型はLeanの関数型へ再帰的に移します。
-/

namespace FormalLab.Bridges.STLCCategoricalSemantics

open FormalLab.TypeTheory.SimplyTypedLambdaCalculus
open FormalLab.TypeTheory.StructuralRules

universe u

def interpretType (Base : Type u) : SimpleType → Type u
  | .atom => Base
  | A ⇒ B => interpretType Base A → interpretType Base B

def interpretContext (Base : Type u) : Context → Type u
  | [] => PUnit.{u + 1}
  | A :: Γ => interpretType Base A × interpretContext Base Γ

/-!
空文脈は零項積である一元型、拡張文脈 `A::Γ` は `⟦A⟧×⟦Γ⟧` です。Leanの `PUnit.{u + 1}` は
数学的には通常の `Unit` と同じ一元型ですが、解釈する原子型と同じ宇宙 `Type u` に置けます。既存構文では
de Bruijn添字0が文脈の先頭を指すため、環境の第一成分に最も近い変数を置きます。文脈の並びと積の括弧づけは
一つの選択であり、一般圏では結合子と単位子を介して別の選択と同型になります。

## 型付き変数は積の射影になる

`Var Γ A` の導出を再帰的に読むと、環境 `⟦Γ⟧` から成分 `⟦A⟧` を取り出す関数が得られます。
-/

def denoteVar {Base : Type u} {Γ : Context} {A : SimpleType} :
    Var Γ A → interpretContext Base Γ → interpretType Base A
  | .zero => Prod.fst
  | .succ v => denoteVar v ∘ Prod.snd

example {Base : Type u} {Γ : Context} {A : SimpleType} :
    denoteVar (Base := Base) (Var.zero : Var (A :: Γ) A) = Prod.fst := rfl

example {Base : Type u} {Γ : Context} {A B : SimpleType} (v : Var Γ A) :
    denoteVar (Base := Base) (Var.succ (B := B) v) = denoteVar v ∘ Prod.snd := rfl

/-!
`zero` は第一射影です。`succ v` は第二射影で外側の環境へ移ってから、`v` の射影を続けます。変数名や
自然数添字を直接評価するのではなく、型付き所属証明がどの射影を選ぶかを決めます。

## 型付き項を環境から値への関数へ移す

変数、適用、抽象の三構成子を再帰的に解釈します。
-/

def denoteTm {Base : Type u} {Γ : Context} {A : SimpleType} :
    Tm Γ A → interpretContext Base Γ → interpretType Base A
  | .var v => denoteVar v
  | .app fn argument =>
      fun environment => denoteTm fn environment (denoteTm argument environment)
  | .lam body =>
      fun environment value => denoteTm body (value, environment)

def EnvironmentsAgree {Base : Type u} {Γ Δ : Context} (ρ : Renaming Γ Δ)
    (source : interpretContext Base Γ) (target : interpretContext Base Δ) : Prop :=
  ∀ {A : SimpleType} (v : Var Γ A), denoteVar v source = denoteVar (ρ v) target

theorem environmentsAgree_lift {Base : Type u} {Γ Δ : Context} {A : SimpleType}
    {ρ : Renaming Γ Δ} {source : interpretContext Base Γ} {target : interpretContext Base Δ}
    (h : EnvironmentsAgree ρ source target) (value : interpretType Base A) :
    EnvironmentsAgree (liftRenaming ρ) (value, source) (value, target) := by
  intro B v
  cases v with
  | zero => rfl
  | succ rest => exact h rest

theorem denote_rename {Base : Type u} {Γ : Context} {A : SimpleType} (term : Tm Γ A) :
    ∀ {Δ : Context} (ρ : Renaming Γ Δ)
      (source : interpretContext Base Γ) (target : interpretContext Base Δ),
      EnvironmentsAgree ρ source target →
        denoteTm term source = denoteTm (rename ρ term) target := by
  induction term with
  | var v =>
      intro Δ ρ source target h
      exact h v
  | app fn argument fn_ih argument_ih =>
      intro Δ ρ source target h
      change denoteTm fn source (denoteTm argument source) =
        denoteTm (rename ρ fn) target (denoteTm (rename ρ argument) target)
      rw [fn_ih ρ source target h, argument_ih ρ source target h]
  | lam body body_ih =>
      intro Δ ρ source target h
      funext value
      exact body_ih (liftRenaming ρ) (value, source) (value, target)
        (environmentsAgree_lift h value)

theorem denote_weakenFront {Base : Type u} {Γ : Context} {A B : SimpleType}
    (term : Tm Γ A) (value : interpretType Base B) (environment : interpretContext Base Γ) :
    denoteTm (weakenFront term) (value, environment) = denoteTm term environment := by
  symm
  exact denote_rename term (fun v => .succ v) environment (value, environment) (by
    intro C v
    rfl)

/-!
名前変更 `ρ : Renaming Γ Δ` は構文上の変数を移します。二つの環境が `ρ` に沿って一致するとは、`Γ` のどの
型付き変数を射影しても、名前変更後に `Δ` の環境から射影した値と等しいことです。`denote_rename` はこの仮定を
項全体へ持ち上げます。ラムダ抽象の場合に新しい引数を両環境へ同時に加える箇所が、束縛子の下で名前変更を
持ち上げる操作に対応します。弱化の意味保存は、新しい第一成分をどの既存変数も参照しない場合です。
-/

theorem denote_identity (Base : Type u) (A : SimpleType) :
    denoteTm (Base := Base) (identity A) .unit =
      (id : interpretType Base A → interpretType Base A) := rfl

theorem denote_constant (Base : Type u) (A B : SimpleType) :
    denoteTm (Base := Base) (constant A B) .unit =
      (fun a : interpretType Base A => fun _ : interpretType Base B => a) := rfl

/-!
適用では同じ環境を関数項と引数項の双方へ渡します。これは文脈の値を複製できることを使っています。抽象では
新しい引数を環境の先頭へ追加します。型添字により、関数項の入力型と引数項の型、抽象本体の文脈拡張が一致しない
定義は書けません。

## `Type` モデルでβ・ηを計算する

閉じた引数へ恒等関数を適用するβ-redexと、閉じた関数を一度適用して再抽象するη展開を構文として作ります。
-/

def identityRedex {A : SimpleType} (argument : Tm [] A) : Tm [] A :=
  .app (identity A) argument

theorem denote_identityRedex {Base : Type u} {A : SimpleType}
    (argument : Tm [] A) :
    denoteTm (Base := Base) (identityRedex argument) .unit = denoteTm argument .unit := rfl

def etaExpansion {A B : SimpleType} (function : Tm [] (A ⇒ B)) : Tm [] (A ⇒ B) :=
  .lam (.app (weakenFront function) (.var .zero))

theorem denote_etaExpansion {Base : Type u} {A B : SimpleType}
    (function : Tm [] (A ⇒ B)) :
    denoteTm (Base := Base) (etaExpansion function) .unit = denoteTm function .unit := by
  funext value
  exact congrFun (denote_weakenFront function value .unit) value

/-!
最初の等式は関数適用の計算だけで `rfl` になります。ηでは関数外延性を使い、任意の引数で両辺を比較します。
これは二つの項が構文木として同じという主張ではなく、選んだモデルで同じ射を表すという意味論的等式です。

## 意味論的代入は射の合成である

文脈 `Γ` の各変数へ `Δ` での値を与える意味論的代入は、環境を反対向きに送る関数
`⟦Δ⟧→⟦Γ⟧` です。項の意味 `⟦Γ⟧→⟦A⟧` と合成すると、`Δ` の下での項になります。
-/

abbrev SemanticTerm (Base : Type u) (Γ : Context) (A : SimpleType) :=
  interpretContext Base Γ → interpretType Base A

abbrev SemanticSubstitution (Base : Type u) (Γ Δ : Context) :=
  interpretContext Base Δ → interpretContext Base Γ

def semanticSubstitute {Base : Type u} {Γ Δ : Context} {A : SimpleType}
    (substitution : SemanticSubstitution Base Γ Δ)
    (term : SemanticTerm Base Γ A) : SemanticTerm Base Δ A :=
  term ∘ substitution

theorem semanticSubstitute_id {Base : Type u} {Γ : Context} {A : SimpleType}
    (term : SemanticTerm Base Γ A) :
    semanticSubstitute id term = term := by
  funext environment
  rfl

theorem semanticSubstitute_comp {Base : Type u} {Γ Δ Θ : Context} {A : SimpleType}
    (first : SemanticSubstitution Base Γ Δ)
    (second : SemanticSubstitution Base Δ Θ)
    (term : SemanticTerm Base Γ A) :
    semanticSubstitute second (semanticSubstitute first term) =
      semanticSubstitute (first ∘ second) term := by
  funext environment
  rfl

/-!
構文的代入補題の意味論的内容は

$$
\llbracket t[\sigma]\rrbracket
=\llbracket\sigma\rrbracket;\llbracket t\rrbracket.
$$

です。上の二定理は恒等代入と合成代入が恒等射と射の結合律へ移ることを示します。本章の `semanticSubstitute` は
既存の構文関数 `substitute` そのものではありません。両者の対応を完全に示すには、型付き変数代入を環境射へ
再帰的に解釈し、項について帰納する置換補題が要ります。この追加証明義務を、関数合成の定義的等式と混同しません。

## 一般のデカルト閉圏で規則を射へ移す

圏 `C` にデカルト積と内部homがあるとします。文脈拡張を `A⊗Γ` と書けば、最も近い変数と弱化は二射影です。
適用は関数と引数を対にして評価し、抽象はカリー化します。
-/

open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open _root_.CategoryTheory.CartesianMonoidalCategory
open _root_.CategoryTheory.MonoidalClosed

universe uC vC

variable {C : Type uC} [Category.{vC} C]
variable [CartesianMonoidalCategory C] [MonoidalClosed C]
variable {Γ A B : C}

def interpretZeroVariable : A ⊗ Γ ⟶ A := fst A Γ

def interpretWeakening (term : Γ ⟶ B) : A ⊗ Γ ⟶ B :=
  snd A Γ ≫ term

def interpretApplication (function : Γ ⟶ A ⟶[C] B) (argument : Γ ⟶ A) : Γ ⟶ B :=
  lift argument function ≫ (ihom.ev A).app B

def interpretAbstraction (body : A ⊗ Γ ⟶ B) : Γ ⟶ A ⟶[C] B :=
  curry body

example (body : A ⊗ Γ ⟶ B) : uncurry (interpretAbstraction body) = body :=
  uncurry_curry body

example (function : Γ ⟶ A ⟶[C] B) :
    interpretAbstraction (uncurry function) = function :=
  curry_uncurry function

/-!
`interpretApplication` の `lift argument function` は、同じ文脈射から引数と関数を取り出して積へ入れます。
ここに縮約、すなわち文脈を二用途へ複製できるデカルト構造が現れます。`interpretWeakening` は第一成分を捨てるため、
弱化を使います。一般のモノイダル閉圏ではこの二操作を無条件に構成できず、線形ラムダ計算の意味論へ移ります。

## β則は評価、η則は指数対象の一意性である

抽象した本体を拡張文脈で直ちに評価すると元の本体へ戻ります。
-/

theorem categorical_beta (body : A ⊗ Γ ⟶ B) :
    A ◁ interpretAbstraction body ≫ (ihom.ev A).app B = body :=
  whiskerLeft_curry_ihom_ev_app A B body

theorem categorical_eta (function : Γ ⟶ A ⟶[C] B) :
    interpretAbstraction (uncurry function) = function :=
  curry_uncurry function

/-!
β則は「抽象してから適用する」経路が本体の射と一致することを述べます。η則は、関数を評価可能な形へ展開して
再び抽象すると元の射へ戻ることを述べます。両者は随伴 `A×-⊣A⇒-` の三角恒等式です。

## 健全性と完全性を分ける

意味論的健全性は、構文で証明した等式 `t=u` が全てのモデルで `⟦t⟧=⟦u⟧` を導くことです。完全性は逆に、
全モデルで意味が等しい二項の等式を構文体系で導出できると述べます。本章のβ・η計算は健全性証明の構成子場合を
示しますが、任意の等式導出に関する全体定理や、自由デカルト閉圏を使う完全性定理までは自動的に含みません。

構文圏を作ると、対象は単純型、射は文脈付き項をβη等式で割った同値類になります。この圏が与えた原子型上の
自由デカルト閉圏になることが、STLCの内部言語とデカルト閉圏の外部意味論を結ぶ完全性の中心です。商が適切に
定義されること、合成が代入に一致すること、普遍性を満たすことをそれぞれ証明する必要があります。

## 対応表

| STLC | デカルト閉圏 | Leanによる形式化 |
|---|---|---|
| 型 `A` | 対象 `⟦A⟧` | `interpretType` |
| 文脈 `Γ` | 有限積 `⟦Γ⟧` | `interpretContext` |
| 判断 `Γ⊢t:A` | 射 `⟦Γ⟧→⟦A⟧` | `denoteTm` |
| 変数 | 積の射影 | `denoteVar`, `fst`, `snd` |
| 適用 | 対化して評価 | `interpretApplication` |
| 抽象 | カリー化 | `interpretAbstraction` |
| 代入 | 射の合成 | `semanticSubstitute` |
| β・η | 随伴の三角恒等式 | `categorical_beta`, `categorical_eta` |

## 要点

* STLCの型は対象、文脈は有限積、型判断は文脈対象から型対象への射として解釈できる。
* 変数は射影、適用は評価射、ラムダ抽象はカリー化になる。
* `Type` の標準モデルでは解釈を環境から値への関数として再帰的に計算できる。
* 構文的代入は意味論で射の合成へ移り、恒等・合成法則は圏法則へ移る。
* β・η等式の健全性は指数対象の二つの逆法則、または随伴の三角恒等式から従う。
* 健全性、全モデルに対する完全性、構文圏の自由性は異なる定理である。

## 研究史と文献案内

Church [CHU40] の単純型付きラムダ計算と、Curry [CUR34]・Howard [HOW80] に連なる式と型の対応は、圏論的
意味論の構文側の背景です。デカルト閉圏を用いる型付きラムダ計算と高階論理の意味論は Lambek–Scott [LS86] が
標準文献です。構文圏、自由デカルト閉圏、健全性・完全性を区別して読むにも同書を参照してください。
本章の `Tm` は第12章の教育用内在的構文であり、[LS86] の構文圏をそのまま実装したものではありません。
一般圏側の `fst`, `snd`, `lift`, `ihom.ev`, `curry` は [MATHLIB] の現行APIに従います。

## 問題

### 全ての構文的代入について意味論的置換補題を証明する

`Substitution Γ Δ` を環境射 `⟦Δ⟧→⟦Γ⟧` へ再帰的に解釈してください。変数について射影との可換性を示し、
`Tm` の変数・適用・抽象の場合で `⟦substitute σ t⟧=⟦t⟧∘⟦σ⟧` を証明します。抽象の場合に
`liftSubstitution` と文脈積の結合がどう対応するかを明示できれば完了です。

### β・η以外の等式をモデルで検査する

合成関数、定数関数、引数交換を表す閉じた `Tm` を構成し、`denoteTm` を計算してください。同じ型を持つが
βη同値でない二項を有限な原子型モデルで区別し、モデルが項等式の反例を与える仕組みを示します。まず原子型を
`Bool` とし、二項の表示が異なる入力を一つ具体的に与えます。次に原子型を一元型へ変えると、構文の異なる項が
同じ関数を表す場合を探してください。この対比により、一つのモデルで等しいことは構文的等式の証明にならないが、
一つのモデルで異なることは全モデルに対する等式の反例になる、と量化の向きを説明します。各項の型、区別に使う
入力、Leanで検査した不等式、二種類の量化を明記できれば完了です。

### 構文圏の対象・射・合成を設計する

対象を単純型、射 `A→B` を一変数文脈の項 `A⊢t:B` のβη同値類として定義してください。恒等射を変数、合成を
代入で作り、well-definednessと圏法則に必要な補題を列挙します。積と指数対象の候補を構成し、この圏が原子型
一つ上の自由デカルト閉圏になるという普遍性を正確に述べられれば完了です。

### 構造規則が意味射のどこに現れるかを追跡する

弱化を `snd≫f`、縮約を対角射、交換を積の対称性として書いてください。`interpretApplication` が同じ文脈を
関数と引数の双方へ渡す際に縮約を使うことを図式で示します。これらの射を持たないモノイダル閉圏へ移したとき、
通常のSTLCのどの項が解釈できなくなるかを `K`・`W` combinatorで検査できれば完了です。
-/

end FormalLab.Bridges.STLCCategoricalSemantics