import FormalLab.TypeTheory.SystemF
import FormalLab.TypeTheory.Normalization

/-!
# 第18章：論理関係と基本補題

型 `A → B` の二つの関数が「関係している」とは、同じ入力で等しい出力を返すことだけでしょうか。
より一般には、入力間の関係を出力間の関係へ保存することです。この定義を型の構造に沿って反復すると、
型付き項が代入された関連値を関連結果へ送るという一つの帰納原理が得られます。

本章では左右の型が異なってよい二項関係を一つの構造として持ち、関数型の関係を構成します。恒等関数と
合成が任意の関係を保存することをLeanで証明し、型判断についての基本補題へ一般化する際の環境・代入・
全称型の役割を分解します。論理関係を単なる等式の言い換えではなく、型ごとに組み立てる証明装置として
理解することが目標です。

## 関係は左右に異なる型を持てる

関係 `R` は左の型 `R.Left`、右の型 `R.Right`、二要素が関連するという命題を持ちます。同じ型上の
等式は一例ですが、自然数と文字列の対応、実装型と仕様型の間のシミュレーションも関係になります。
-/

namespace FormalLab.TypeTheory.LogicalRelations

universe u

structure Relation where
  Left : Type u
  Right : Type u
  relates : Left → Right → Prop

def equalityRelation (α : Type u) : Relation where
  Left := α
  Right := α
  relates := fun x y => x = y

def graphRelation {α β : Type u} (f : α → β) : Relation where
  Left := α
  Right := β
  relates := fun x y => f x = y

/-!
`graphRelation f` では右要素が左要素の `f` による像であるとき関連します。関数を関係として埋め込む
ことで、関係保存定理から通常の関数方程式を取り出せます。この操作が後のfree theoremで使う橋になります。

## 関数間の関係は入力を反変、出力を共変に使う

入力関係 `R` と出力関係 `S` から関数型の関係 `R ⇒ᵣ S` を作ります。左右の関数 `f`, `g` が関連する
とは、任意の関連入力 `x`, `y` を関連出力 `f x`, `g y` へ送ることです。

$$
(f,g)\in(R\Rightarrow_{\!r}S)
\;:\!\Longleftrightarrow\;
\forall x\,y.\;R(x,y)\to S(f(x),g(y)).
$$
-/

def arrowRelation (R S : Relation) : Relation where
  Left := R.Left → S.Left
  Right := R.Right → S.Right
  relates := fun f g => ∀ ⦃x y⦄, R.relates x y → S.relates (f x) (g y)

infixr:55 " ⇒ᵣ " => arrowRelation

def RelatedFunctions (R S : Relation)
    (f : R.Left → S.Left) (g : R.Right → S.Right) : Prop :=
  (R ⇒ᵣ S).relates f g

theorem identityRelated (R : Relation) :
    RelatedFunctions R R (fun x => x) (fun y => y) := by
  intro x y related
  exact related

theorem compositionRelated (R S T : Relation)
    {f₁ : R.Left → S.Left} {f₂ : R.Right → S.Right}
    {g₁ : S.Left → T.Left} {g₂ : S.Right → T.Right}
    (fRelated : RelatedFunctions R S f₁ f₂)
    (gRelated : RelatedFunctions S T g₁ g₂) :
    RelatedFunctions R T (fun x => g₁ (f₁ x)) (fun y => g₂ (f₂ y)) := by
  intro x y related
  exact gRelated (fRelated related)

/-!
`identityRelated` は関係の証拠をそのまま返します。`compositionRelated` はまず `R` の証拠を `S` へ、
次に `T` へ送ります。これは圏論的な恒等・合成の法則に似ていますが、本章ではまだ関係と関係保存関数の
圏を定義していません。似た式だけから同一の概念と断定せず、後の橋章で構造を比較します。

## 関係環境が型変数の意味を与える

System Fの型変数 `X` を解釈するには、左右の型だけでなくその間の関係を環境から選びます。関数型は
`arrowRelation` で再帰的に解釈します。全称型では、任意の左右型と任意の関係を環境へ追加しても本体が
関連することを要求します。

$$
\begin{aligned}
\llbracket X_i\rrbracket_\rho&=\rho(i),\\
\llbracket A\to B\rrbracket_\rho
  &=\llbracket A\rrbracket_\rho\Rightarrow_{\!r}\llbracket B\rrbracket_\rho,\\
\llbracket\forall X.\,A\rrbracket_\rho
  &:\!\Longleftrightarrow
  \forall\alpha\,\beta\,R\subseteq\alpha\times\beta.\;
  \llbracket A\rrbracket_{R::\rho}.
\end{aligned}
$$

全称型の場合がパラメトリシティの一様性を生みます。型変数を等式関係だけで解釈すると、異なる表現間で
振舞いが対応するという情報を得られません。「任意の関係」まで量化することが本質です。

-/

/-!

## 基本補題は型付き代入が関係を保存すると述べる

項 `Γ ⊢ t : A` を固定します。左右の代入 `σ₁`, `σ₂` が文脈の各変数を、その型の論理関係で関連する
値へ送るなら、代入後の二項 `t[σ₁]`, `t[σ₂]` は `A` の論理関係で関連します。

$$
\frac{\Gamma\vdash t:A\qquad\sigma_1\mathrel{\approx_\Gamma}\sigma_2}
     {t[\sigma_1]\mathrel{\approx_{\llbracket A\rrbracket_\rho}}t[\sigma_2]}
\quad(\text{基本補題}).
$$

証明は型の構造だけでなく型導出について帰納します。変数の場合は代入環境の仮定、抽象の場合は任意の
関連引数、適用の場合は関数関係の除去を使います。型抽象では関係環境を任意の `R` で拡張し、型適用では
全称関係を選んだ型と関係へ特殊化します。

本章の `identityRelated` と `compositionRelated` は基本補題の代表的な意味論的分岐を検査しますが、
System F構文全体に対する基本補題のLean証明ではありません。完全な形式化には型代入と項代入の交換、
関係環境の持ち上げ、全称型の宇宙レベルを同時に管理する必要があります。検査済みの範囲と一般定理を
区別します。

## 正規化に使う単項関係との違い

強正規化証明で用いるreducibilityは、一つの項が計算可能かを型ごとに定める単項述語として提示できます。
パラメトリシティでは二つの解釈と二項関係を比較します。両者は型の構造に沿う基本補題を共有するため
広い意味で論理関係と呼ばれますが、目的と項数を区別します。

## 要点

* 論理関係は左右に異なる型を持ち、等式関係より広い対応を表せる。
* 関数関係は関連入力を関連出力へ送る二関数を関連づける。
* 全称型の解釈は任意の型と任意の関係を量化し、一様性の根拠を与える。
* 基本補題は関連代入が型付き項を関連結果へ送ることを型導出の帰納で証明する。
* 正規化の単項計算可能性とパラメトリシティの二項関係は方法を共有するが目的が異なる。

## 研究史と文献案内

Taitの有限型汎関数の解釈 [TAI67] は正規化に用いる計算可能性の系譜を読む基準点です。Reynoldsの
抽象化定理と型構造に沿う関係解釈は、プログラミング言語におけるパラメトリシティへ重要な役割を
果たしました [REY83]。System Fの論理関係を証明論から読むには [GLT89]、型安全性・表現独立性を含む
教科書的展開は [TAPL02] を参照してください。

## 問題

### 三つの関係を関数型へ持ち上げる

自然数上の等式、自然数から偶数への倍写像のグラフ、大小関係を `Relation` として定義してください。
各関係を入力と出力へ置いた四つの `arrowRelation` について、関連する関数対と関連しない関数対を
一つずつ示します。失敗例では、関係する入力と関係しない出力を具体的な反証証人として挙げてください。

### 基本補題の抽象場合を導出する

`Γ, x:A ⊢ t:B` の帰納仮定から `Γ ⊢ λx.t:A→B` の関係保存を導いてください。任意の関連引数を
左右の代入へ追加し、帰納仮定へ渡す順序を数式で書きます。変数捕獲を避ける持ち上げが必要な位置を
第40章の代入と照合します。帰納仮定が出力関係を返した後、関数関係の全称量化をどの順で畳むかも
明示してください。抽象規則の仮定と結論を一度ずつ使う導出になれば完了です。

### 単項と二項の論理関係を比較する

STLC強正規化の計算可能性とSystem Fパラメトリシティの関係解釈を、項数、型変数環境、全称型、
導かれる定理という四項目で比較してください。どちらにも必要な基本補題の形を書き、一方の証明を
そのまま他方へ転用できない分岐を特定します。共通構造と相違点を一つずつ説明できれば完了です。
-/

end FormalLab.TypeTheory.LogicalRelations