import FormalLab.TypeTheory.SimplyTypedLambdaCalculus

/-!
# 第12章：弱化・交換・縮約・代入

型判断の規則を使って一つの導出を作れても、その導出を別の文脈へ安全に移せるとはまだ限りません。
未使用の仮定を加える、仮定の順序を入れ替える、同じ仮定をまとめる、変数を同じ型の項で置き換える。
これらは項の計算ではなく、文脈と導出を変換する操作です。

本章ではこの四操作を**構造規則**と代入として定式化します。型を添字に持つ項をLeanで構成し、
型の合わない変数変換や代入をそもそも記述できない形にします。外在的な型判断の証明を、内在的に
型付けされた構文へ写すことで、後の保存定理が依存する補題の情報の流れを明らかにします。

## 文脈に所属する変数を型で索引づける

文脈 `Γ` に型 `A` の変数があるという判断を `Var Γ A` で表します。先頭の変数は `zero`、
一つ外側の変数は `succ` です。単なる自然数添字と違い、変数自身が所属する文脈と型を保持します。

$$
\frac{}{A,\Gamma\ni 0:A}\;(\mathsf{zero})
\qquad
\frac{\Gamma\ni x:A}{B,\Gamma\ni x+1:A}\;(\mathsf{succ}).
$$

添字だけなら任意の自然数を書けますが、`Var Γ A` の値は上の規則で到達できる位置だけを表します。
文脈外の位置や異なる型の位置は構成できません。
-/

namespace FormalLab.TypeTheory.StructuralRules

open FormalLab.TypeTheory.SimplyTypedLambdaCalculus

inductive Var : Context → SimpleType → Type where
  | zero : Var (A :: Γ) A
  | succ : Var Γ A → Var (B :: Γ) A

inductive Tm : Context → SimpleType → Type where
  | var : Var Γ A → Tm Γ A
  | app : Tm Γ (A ⇒ B) → Tm Γ A → Tm Γ B
  | lam : Tm (A :: Γ) B → Tm Γ (A ⇒ B)

def identity (A : SimpleType) : Tm [] (A ⇒ A) :=
  .lam (.var .zero)

def constant (A B : SimpleType) : Tm [] (A ⇒ B ⇒ A) :=
  .lam (.lam (.var (.succ .zero)))

/-!
`Tm Γ A` の項は、構成された時点で `Γ ⊢ t : A` の導出を含みます。適用の入力型が合わない項は
`Tm` の構成子へ渡せません。この表現は型検査の必要を消したのではなく、型判断を構文の添字へ
移したものです。元章の `HasType Γ t A : Prop` が外から型を割り当てる**外在的構文**であるのに対し、
本章の `Tm Γ A : Type` は整形式な項だけを作る**内在的構文**です。

## 名前変更は型を保つ変数写像である

文脈 `Γ` から `Δ` への名前変更は、各型 `A` について `Γ` の `A` 型変数を `Δ` の `A` 型変数へ
送ります。型を保存するという条件が関数の型に現れるため、原子型の変数を関数型の変数へ誤って
送る写像は定義できません。
-/

def Renaming (Γ Δ : Context) : Type :=
  ∀ {A}, Var Γ A → Var Δ A

/-!
数式では型を保つ名前変更と代入を

$$
\mathsf{Ren}(\Gamma,\Delta)
=\prod_A\mathsf{Var}(\Gamma,A)\to\mathsf{Var}(\Delta,A),
$$

$$
\mathsf{Sub}(\Gamma,\Delta)
=\prod_A\mathsf{Var}(\Gamma,A)\to\mathsf{Tm}(\Delta,A)
$$

と書けます。二式の終域だけが変数と項で異なります。`rename` と `substitute` はこの写像を
変数位置だけでなく項の構文全体へ持ち上げる作用です。
-/

def liftRenaming {Γ Δ : Context} {A : SimpleType} (ρ : Renaming Γ Δ)
    {B : SimpleType} (v : Var (A :: Γ) B) : Var (A :: Δ) B :=
  match v with
  | .zero => .zero
  | .succ rest => .succ (ρ rest)

def rename {Γ Δ : Context} (ρ : Renaming Γ Δ) {A : SimpleType} : Tm Γ A → Tm Δ A
  | .var v => .var (ρ v)
  | .app function argument => .app (rename ρ function) (rename ρ argument)
  | .lam body => .lam (rename (liftRenaming ρ) body)

def weakenFront {Γ : Context} {A B : SimpleType} (term : Tm Γ A) : Tm (B :: Γ) A :=
  rename (fun v => .succ v) term

def swapFront {Γ : Context} {A B C : SimpleType} :
    Var (A :: B :: Γ) C → Var (B :: A :: Γ) C
  | .zero => .succ .zero
  | .succ .zero => .zero
  | .succ (.succ rest) => .succ (.succ rest)

def exchangeFront {Γ : Context} {A B C : SimpleType} (term : Tm (A :: B :: Γ) C) :
    Tm (B :: A :: Γ) C :=
  rename swapFront term

def contractFront {Γ : Context} {A C : SimpleType} :
    Var (A :: A :: Γ) C → Var (A :: Γ) C
  | .zero => .zero
  | .succ .zero => .zero
  | .succ (.succ rest) => .succ rest

def contraction {Γ : Context} {A C : SimpleType} (term : Tm (A :: A :: Γ) C) :
    Tm (A :: Γ) C :=
  rename contractFront term

/-!
`weakenFront` は新しい仮定を先頭へ加え、既存の変数を一段外へ移します。`exchangeFront` は先頭二仮定を
交換し、それを参照する二変数も交換します。`contraction` は同型の二仮定を一つへまとめ、どちらの
参照も同じ変数へ送ります。文脈の列だけを書き換えるのではなく、項中の変数参照を同時に変えることが
構造変換の本体です。

これらは `Tm` の新しい構成子ではありません。既存の導出を変換して得られる**許容規則**です。
線形型理論では弱化や縮約を無条件に許さないため、全ての型体系に共通する構文規則とはみなしません。

## 代入は変数を同じ型の項へ送る

代入 `Substitution Γ Δ` は、`Γ` の各 `A` 型変数へ `Δ` で型 `A` を持つ項を割り当てます。
名前変更が変数から変数への写像だったのに対し、代入は変数から項への写像です。ラムダの下へ入るとき、
新しく束縛された変数は自分自身へ、外側の変数に対応する置換項は弱化して一段外へ送ります。
-/

def Substitution (Γ Δ : Context) : Type :=
  ∀ {A}, Var Γ A → Tm Δ A

def liftSubstitution {Γ Δ : Context} {A : SimpleType} (σ : Substitution Γ Δ)
    {B : SimpleType} (v : Var (A :: Γ) B) : Tm (A :: Δ) B :=
  match v with
  | .zero => .var .zero
  | .succ rest => weakenFront (σ rest)

def substitute {Γ Δ : Context} (σ : Substitution Γ Δ) {A : SimpleType} :
    Tm Γ A → Tm Δ A
  | .var v => σ v
  | .app function argument => .app (substitute σ function) (substitute σ argument)
  | .lam body => .lam (substitute (liftSubstitution σ) body)

def topSubstitution {Γ : Context} {A B : SimpleType} (argument : Tm Γ A)
    (v : Var (A :: Γ) B) : Tm Γ B :=
  match v with
  | .zero => argument
  | .succ rest => .var rest

def substituteTop {Γ : Context} {A B : SimpleType} (argument : Tm Γ A) :
    Tm (A :: Γ) B → Tm Γ B :=
  substitute (topSubstitution argument)

example {A : SimpleType} (argument : Tm [] A) :
    substituteTop (B := A) argument (.var .zero) = argument := rfl

example {A C : SimpleType} (argument : Tm [] A) :
    substituteTop (B := C ⇒ A) argument (.lam (.var (.succ .zero))) =
      .lam (weakenFront (B := C) argument) := rfl

/-!
最初の等式はβ簡約で恒等関数の本体へ引数を代入する場合です。二つ目ではラムダの下へ引数を運ぶため、
自由変数を捕獲しない `weakenFront` が現れます。結果の型がもとの結論型 `B` のままであることは、
後から証明した性質ではなく `substituteTop` の戻り型が保証しています。これは代入補題

$$
\frac{\Gamma,x:A\vdash t:B\qquad\Gamma\vdash u:A}
     {\Gamma\vdash t[x:=u]:B}.
$$

の内在的な実装です。外在的構文では同じ主張を `HasType` の導出について帰納法で証明します。
内在的構文はその帰納の型保存部分をLeanの型検査へ移しますが、どの代入が構文上の置換に対応するかという
正当性まで自動的に与えるわけではありません。

## 要点

* 弱化・交換・縮約は、文脈だけでなく変数参照も変換する許容規則である。
* 名前変更は同じ型の変数へ、代入は同じ型の項へ各変数を送る。
* ラムダの下では新しい束縛変数を固定し、外から運ぶ項を弱化して捕獲を避ける。
* 内在的構文では型保存を関数の入出力型に記録できるが、外在的導出との対応は別に証明する。
* 構造規則を無制限に許すかどうかは型体系の設計事項であり、線形性などの表現力に関わる。

## 研究史と文献案内

弱化・交換・縮約とcutはGentzenの構造的な証明体系を読む中心語です [GEN35]。ただし本章の
`Renaming` と内在的なde Bruijn構文を原論文へ帰属させません。ラムダ計算の変数表現は [DB72]、
型安全性証明で用いる名前変更・代入補題の現代的な展開は [TAPL02] と [PFPL16] を参照してください。
線形論理では構造規則の制御自体が論理の意味を変えるため、後の線形型の章で再検討します。

## 問題

### 四つの変換を導出木として復元する

`weakenFront`、`exchangeFront`、`contraction`、`substituteTop` の型を、文脈付き型判断の推論規則へ
書き戻してください。各変換で文脈のどの位置が変わり、項中の各de Bruijn添字がどこへ送られるかを
三変数の例で表にします。文脈だけを交換した誤った実装を一つ作り、どの変数の型が変わるか示せば完了です。

### ラムダの下の代入を一段ずつ追跡する

外側の自由変数と内側の束縛変数を一つずつ含む項を `Tm` で構成し、`liftSubstitution` が各変数を
どう送るか計算してください。弱化を除いた素朴な代入なら自由変数がどの束縛子に捕獲されるかを示します。
正しい結果について、代入前後の文脈と型が一致する導出木を再構成し、各再帰呼出しの不変条件を説明します。

### 構造規則を制限した体系を比較する

交換を許すが弱化と縮約を許さない変数使用規則を設計し、`K = λx. λy. x` と
`W = λf. λx. f x x` のどちらが型付けできなくなるか調べてください。単に構成子を削るのではなく、
失われる導出を仮定の使用回数から説明します。通常のSTLC、アフィン型、線形型の差を表にします。
最後に各体系で許容される名前変更の型を比較し、制限がどこへ現れるか示せば完了です。
-/

end FormalLab.TypeTheory.StructuralRules