import FormalLab.Logic.Connectives
import FormalLab.Logic.Quantifiers

/-!
# 第10章：自然演繹・シーケント計算・証明の正規化

同じ命題 `P → P` でも、証明を一つの完成した式として書く方法と、仮定から結論へ進む
推論の木として書く方法があります。さらに推論規則の左右を揃え、複数の仮定と結論候補の間を
変形する体系もあります。結論が同じだからといって、証明の構造まで同じとは限りません。

本章では含意だけを持つ小さな言語を用い、自然演繹とシーケント計算を別々に定義します。
導入の直後に除去を行う迂回がラムダ項のβ-redexに対応すること、シーケント計算ではcutが
中間命題を受け渡すことを確かめます。完全な正規化定理とcut除去定理を宣言だけで済ませず、
まず一段の簡約を構成して、定理が何を減らさなければならないかを明確にします。

## 推論規則を有限の証拠として読む

命題式を原子命題と含意から生成します。文脈 `Γ` は有限個の仮定を並べたリストです。
自然演繹の判断 `Γ ⊢ A` は、`A` が真かどうかを計算する関数ではありません。仮定規則と
含意の導入・除去規則を有限回組み合わせた導出が存在する、という関係です。

$$
\frac{A\in\Gamma}{\Gamma\vdash A}\;(\mathsf{hyp})
\qquad
\frac{\Gamma,A\vdash B}{\Gamma\vdash A\to B}\;(\to\mathrm I)
\qquad
\frac{\Gamma\vdash A\to B\qquad\Gamma\vdash A}
     {\Gamma\vdash B}\;(\to\mathrm E).
$$

導入規則は仮定 `A` を解除し、除去規則は関数としての証明を引数の証明へ適用します。前章の
Curry–Howard対応により、導出木とラムダ項を同じ情報の二表現として比較できます。
-/

namespace FormalLab.Logic.ProofSystems

inductive Formula where
  | atom : Nat → Formula
  | imp : Formula → Formula → Formula
  deriving DecidableEq, Repr

infixr:55 " ⟶ " => Formula.imp

abbrev Context := List Formula

inductive NaturalDeduction : Context → Formula → Type where
  | hyp {Γ A} : A ∈ Γ → NaturalDeduction Γ A
  | impIntro {Γ A B} : NaturalDeduction (A :: Γ) B → NaturalDeduction Γ (A ⟶ B)
  | impElim {Γ A B} : NaturalDeduction Γ (A ⟶ B) → NaturalDeduction Γ A →
      NaturalDeduction Γ B

/-! ## 恒等導出は仮定を一度使って閉じる -/

def identityDerivation (A : Formula) : NaturalDeduction [] (A ⟶ A) :=
  .impIntro (.hyp (by simp))

def compositionDerivation (A B C : Formula) :
    NaturalDeduction [] ((B ⟶ C) ⟶ (A ⟶ B) ⟶ A ⟶ C) :=
  .impIntro <| .impIntro <| .impIntro <|
    .impElim
      (.hyp (A := B ⟶ C) (by simp))
      (.impElim (.hyp (A := A ⟶ B) (by simp)) (.hyp (A := A) (by simp)))

/-!
`identityDerivation` は仮定 `A` を導入し、その仮定を一度使用してから解除します。
`compositionDerivation` では三つの仮定の位置が異なるため、各 `hyp` の所属証明も導出の一部です。
結論の型だけでなく、どの仮定をどこで消費したかが構成子の入れ子に保存されています。

仮定を一つも使わずに任意の原子命題を導く構成子はありません。したがって規則を列挙しただけで
全命題が証明可能になるわけではありません。導出は必ず、結論の最外結合子か文脈中の仮定に
対応する構成子から始まります。

## 導入直後の除去を一段簡約する

含意導入で作った証明を直ちに除去へ渡すと、仮定へ実際の証明を代入できます。この迂回を
取り除くことが自然演繹の正規化の基本的な一歩です。完全な代入関数には文脈の位置管理が
必要なので、ここでは同じ文脈にある閉じた関数適用を証明項へ写して計算を観察します。
-/

inductive ProofTerm where
  | var : Nat → ProofTerm
  | lam : ProofTerm → ProofTerm
  | app : ProofTerm → ProofTerm → ProofTerm
  deriving DecidableEq, Repr

def shiftAbove (amount cutoff : Nat) : ProofTerm → ProofTerm
  | .var index =>
      if cutoff ≤ index then .var (index + amount) else .var index
  | .lam body => .lam (shiftAbove amount (cutoff + 1) body)
  | .app f a => .app (shiftAbove amount cutoff f) (shiftAbove amount cutoff a)

def shift (term : ProofTerm) : ProofTerm :=
  shiftAbove 1 0 term

def substitute (index : Nat) (argument : ProofTerm) : ProofTerm → ProofTerm
  | .var found =>
      if found < index then .var found
      else if found = index then argument
      else .var (found - 1)
  | .lam body => .lam (substitute (index + 1) (shift argument) body)
  | .app f a => .app (substitute index argument f) (substitute index argument a)

def contractIntroductionElimination? : ProofTerm → Option ProofTerm
  | .app (.lam body) argument => some (substitute 0 argument body)
  | _ => none

example : contractIntroductionElimination? (.app (.lam (.var 0)) (.var 3)) =
    some (.var 3) := rfl

example :
    contractIntroductionElimination? (.app (.lam (.lam (.var 1))) (.var 0)) =
      some (.lam (.var 1)) := rfl

/-!
二つ目の例では、引数に自由に現れる変数が内側のラムダに捕獲されていません。`shiftAbove` は
現在の束縛子を指す添字を保ち、外から持ち込む自由変数だけを動かします。`substitute` はラムダの
下へ入るたび、探す添字と置換項をともに一段持ち上げます。

この関数は全てのredexを探索する正規化器ではありません。最外層が「導入して直ちに除去する」
形のときだけ一段縮約します。正規化定理は、この一段操作が定義できるという主張より強く、
任意の導出から迂回のない導出へ有限回で到達できることを要求します。

## シーケントの左右で規則を揃える

シーケント計算では `Γ ⊢ Δ` の左に利用可能な仮定、右に結論候補を置きます。本章のLeanモデルは
説明を小さく保つため右辺を一命題に限る直観主義的な形です。含意右規則は自然演繹の導入に似ますが、
含意左規則は仮定中の含意を使うために二つの前提を要求します。

$$
\frac{A\in\Gamma}{\Gamma\vdash A}\;(\mathsf{ax})
\qquad
\frac{A,\Gamma\vdash B}{\Gamma\vdash A\to B}\;(\to\mathrm R)
$$

$$
\frac{\Gamma\vdash A\qquad B,\Gamma\vdash C}
     {A\to B,\Gamma\vdash C}\;(\to\mathrm L)
\qquad
\frac{\Gamma\vdash A\qquad A,\Gamma\vdash B}
     {\Gamma\vdash B}\;(\mathsf{cut}).
$$

右辺を一命題に制限したため、このモデルは古典的な多結論シーケントではありません。また文脈をリストとして
具体化しているため、交換・弱化・縮約を暗黙に仮定せず、必要な構造規則は後章で個別に扱います。
-/

inductive Sequent : Context → Formula → Type where
  | ax {Γ A} : A ∈ Γ → Sequent Γ A
  | impRight {Γ A B} : Sequent (A :: Γ) B → Sequent Γ (A ⟶ B)
  | impLeft {Γ A B C} : Sequent Γ A → Sequent (B :: Γ) C →
      Sequent ((A ⟶ B) :: Γ) C
  | cut {Γ A B} : Sequent Γ A → Sequent (A :: Γ) B → Sequent Γ B

def sequentIdentity (A : Formula) : Sequent [] (A ⟶ A) :=
  .impRight (.ax (by simp))

/-- 左文脈の含意とその前件から後件を導きます。 -/
def sequentModusPonens (A B : Formula) : Sequent [A ⟶ B, A] B :=
  .impLeft (.ax (by simp)) (.ax (by simp))

/-! ## cutを構文から除いた導出体系 -/

/-- `Sequent` と終判断を共有し、cut構成子だけを持たない導出です。 -/
inductive CutFree : Context → Formula → Type where
  | ax {Γ A} : A ∈ Γ → CutFree Γ A
  | impRight {Γ A B} : CutFree (A :: Γ) B → CutFree Γ (A ⟶ B)
  | impLeft {Γ A B C} : CutFree Γ A → CutFree (B :: Γ) C →
      CutFree ((A ⟶ B) :: Γ) C

/-- cutなし導出は、同じ終判断を持つ一般のシーケント導出として読めます。 -/
def CutFree.toSequent : CutFree Γ A → Sequent Γ A
  | .ax member => .ax member
  | .impRight derivation => .impRight derivation.toSequent
  | .impLeft left right => .impLeft left.toSequent right.toSequent

/-- 恒等導出はcutを必要としません。 -/
def cutFreeIdentity (A : Formula) : CutFree [] (A ⟶ A) :=
  .impRight (.ax (by simp))

/-!
`cut` は一つ目の導出が作った中間命題 `A` を、二つ目の導出の仮定へ渡します。結論だけを見ると
`A` は消えるため、探索時にどの中間命題を選ぶかが大きな自由度になります。cut除去定理は、cutを
含む任意の導出を同じ終シーケントのcutなし導出へ変換できると述べます。

本章の型でその主張を正確に書けば、全ての `Γ` と `A` に対する
`Sequent Γ A → CutFree Γ A` という変換です。`CutFree.toSequent` は容易な逆向きだけを実装しています。
難しい向きを未証明の定理として宣言せず、何を構成すべきかと、現時点で構成済みの向きを区別します。

自然演繹の正規化とシーケント計算のcut除去は対応しますが、同じ構文上の定理ではありません。
前者は導入・除去の迂回を、後者は中間補題を明示する規則を対象にします。証明には導出の高さや
主式の複雑さに関する帰納が必要であり、本章の一段計算だけから自動的には従いません。

## 要点

* 導出は推論規則を有限回組み合わせた証拠であり、真理値計算ではない。
* 自然演繹は結合子ごとの導入・除去を持ち、含意はラムダ抽象と適用に対応する。
* 導入直後の除去はβ-redexに対応し、正規化はこの種の迂回を体系的に除く。
* シーケント計算のcutは中間命題を受け渡し、cut除去は同じ結論をcutなしで導く。
* 正規化とcut除去は密接に対応するが、対象とする導出構文が異なる。

## 研究史と文献案内

Gentzenの1935年論文 [GEN35] は自然演繹とシーケント計算を同じ研究の中で導入しました。
現在の構成子名や一命題右辺のLeanモデルを原論文へ遡及的に帰属させません。自然演繹の正規化、
シーケント計算のcut除去、型付きラムダ計算との対応を現代的に学ぶには [GLT89] を参照してください。

## 問題

### 一つの含意証明を三表現で再構成する

命題 `(A ⟶ B) ⟶ A ⟶ B` を自然演繹の導出木、`NaturalDeduction` の構成子、ラムダ項の三通りで
書いてください。各仮定が導入される位置、使用される位置、解除される位置へ同じ番号を振ります。
三表現を並べ、構文が違っても保存される情報と、一方だけに明示される情報を説明できれば完了です。

### 正規化前後で結論と仮定を保存する

`(λx. x) u` と、定数関数を直ちに適用する項を `ProofTerm` で作り、一段縮約してください。
縮約前後で自由変数が不意に捕獲されないことを添字ごとに確認します。次に内側だけにredexを持つ項を
作り、本章の関数が縮約しない理由を仕様から説明し、完全な正規化器に必要な探索規則を列挙します。

### cutの便利さと除去可能性を区別する

中間命題 `A` を使う `Sequent.cut` の具体例を一つ構成し、二つの前提導出と終シーケントを書きます。
同じ終シーケントのcutなし導出を作り、cutが誤った規則ではなく証明探索上便利な許容規則であることを
説明してください。[GEN35] と [GLT89] でcut除去の主張を比較し、本章が証明していない帰納測度も特定します。
-/

end FormalLab.Logic.ProofSystems