import FormalLab.TypeTheory.IndexedFamilies
import FormalLab.TypeTheory.StructuralRules

/-!
# 第36章：一般帰納族・除去規則・厳密正値性

長さ付きベクトルは、構成子の結果添字が `0` または `n+1` になる一つの帰納族でした。構文木、型導出、
整形式な式などを統一して設計するには、各構成子がどのファイバーを作り、再帰的な引数をどの位置に持つかを
一般に読めなければなりません。また、見かけ上は帰納的な方程式でも、再帰対象が関数の入力側に現れると
安全な帰納原理を生成できないことがあります。

本章では自由変数の個数で索引づけた式を完全な例として、形成・導入・除去・計算の四規則を追います。
次に帰納型の形を表す小さなコード言語を定義し、再帰変数が正の位置だけに現れる**厳密正値性**を判定します。
この条件が構文検査の都合ではなく、再帰・帰納の意味を成立させる条件であることを反例から理解します。

## 構成子は作るファイバーを結果型で指定する

`Expr n` を、最大 `n` 個の自由変数を使える算術式の型とします。リテラルと加算は任意の `n` で作れます。
`bound i` は `i : Fin n` を要求します。`letE value body` の本体だけは新しい変数を一つ使えるため
`Expr (n+1)` ですが、let式全体は元の `Expr n` へ戻ります。

$$
\frac{k:\mathbb N}{\mathsf{lit}(k):\mathsf{Expr}(n)}
\qquad
\frac{i:\mathsf{Fin}(n)}{\mathsf{bound}(i):\mathsf{Expr}(n)}
$$

$$
\frac{e_1:\mathsf{Expr}(n)\qquad e_2:\mathsf{Expr}(n)}
     {\mathsf{add}(e_1,e_2):\mathsf{Expr}(n)}
\qquad
\frac{v:\mathsf{Expr}(n)\qquad b:\mathsf{Expr}(n+1)}
     {\mathsf{let}(v,b):\mathsf{Expr}(n)}.
$$
-/

namespace FormalLab.TypeTheory.GeneralInductiveFamilies

inductive Expr : Nat → Type where
  | lit {n} : Nat → Expr n
  | bound {n} : Fin n → Expr n
  | add {n} : Expr n → Expr n → Expr n
  | letE {n} : Expr n → Expr (n + 1) → Expr n

def Env (n : Nat) := Fin n → Nat

def extendEnv {n : Nat} (value : Nat) (environment : Env n) : Env (n + 1) :=
  Fin.cases value environment

def evaluate {n : Nat} (environment : Env n) : Expr n → Nat
  | .lit value => value
  | .bound index => environment index
  | .add left right => evaluate environment left + evaluate environment right
  | .letE value body =>
      evaluate (extendEnv (evaluate environment value) environment) body

def closedExample : Expr 0 :=
  .letE (.lit 4) (.add (.bound 0) (.lit 3))

def emptyEnvironment : Env 0 :=
  fun index => Fin.elim0 index

theorem closedExample_evaluates : evaluate emptyEnvironment closedExample = 7 := rfl

/-!
`evaluate` の戻り型は全ファイバーで `Nat` ですが、letの場合の再帰呼出しでは環境の添字が変わります。
本体 `Expr (n+1)` を評価するには、新しい値を先頭へ追加した `Env (n+1)` が必要です。依存した除去原理は
入力のファイバーに応じて帰納仮定の型も変えるため、この再帰を型の不一致なしに記述できます。

## 名前変更は添字の写像を式全体へ持ち上げる

自由変数の名前変更 `ρ : Fin n → Fin m` を式へ作用させます。let本体の下では新しく束縛された先頭変数を
固定し、外側の変数だけを `ρ` で移します。これは型付きラムダ項の `liftRenaming` と同じ依存構造です。
-/

def liftFin {n m : Nat} (ρ : Fin n → Fin m) : Fin (n + 1) → Fin (m + 1) :=
  Fin.cases 0 (fun index => Fin.succ (ρ index))

def rename {n m : Nat} (ρ : Fin n → Fin m) : Expr n → Expr m
  | .lit value => .lit value
  | .bound index => .bound (ρ index)
  | .add left right => .add (rename ρ left) (rename ρ right)
  | .letE value body => .letE (rename ρ value) (rename (liftFin ρ) body)

def openExample : Expr 1 :=
  .add (.bound 0) (.lit 1)

example : evaluate (fun _ => 5) openExample = 6 := rfl

/-!
`rename` は変数の個数を変えても式の構造を保存します。項を単なる木として走査するだけでなく、束縛子の
下で添字写像を持ち上げることが不変条件です。変数構成子の型が `Fin n` でなければ、範囲外の変数を
作らないという性質を別の述語と証明で維持する必要があります。

## 除去原理はmotiveと構成子ごとの場合を要求する

一般の帰納族 `F : I → Type` に対する依存除去では、各 `i:I` と `x:F i` に結論型
`M i x` を割り当てるmotiveを選びます。各構成子について、再帰的引数の帰納仮定から対応する
`M` の値を作れば、全ての `x:F i` について結論が得られます。

$$
\frac{
  M:\prod_{i:I}F(i)\to\mathcal U
  \qquad
  \text{$F$ の各構成子 $c$ に対する、帰納仮定から $M(i_c,c(\vec a))$ への場合}
}{
  \mathsf{elim}_F:\prod_{i:I}\prod_{x:F(i)}M(i,x)
}.
$$

非依存再帰は `M i x` が結果型だけに依存する特殊例です。帰納法は `M` が命題を返す場合です。
「recursor」と「induction theorem」を別々の魔法として覚えず、motiveの依存度の差として読みます。

## 再帰変数は正の位置にだけ現れなければならない

帰納型方程式の右辺を記述する簡略コードを作ります。`recursive` は定義中の型自身、`sum` と `product` は
和と積、`function` は関数空間を表します。関数の入力側へ入ると極性が反転します。
-/

inductive Shape where
  | unit
  | parameter
  | recursive
  | sum : Shape → Shape → Shape
  | product : Shape → Shape → Shape
  | function : Shape → Shape → Shape
  deriving DecidableEq, Repr

inductive Polarity where
  | positive
  | negative
  deriving DecidableEq

def flip : Polarity → Polarity
  | .positive => .negative
  | .negative => .positive

def recursiveOccurrencesArePositive : Polarity → Shape → Bool
  | _, .unit => true
  | _, .parameter => true
  | polarity, .recursive => polarity == .positive
  | polarity, .sum left right =>
      recursiveOccurrencesArePositive polarity left &&
        recursiveOccurrencesArePositive polarity right
  | polarity, .product left right =>
      recursiveOccurrencesArePositive polarity left &&
        recursiveOccurrencesArePositive polarity right
  | polarity, .function domain codomain =>
      recursiveOccurrencesArePositive (flip polarity) domain &&
        recursiveOccurrencesArePositive polarity codomain

def listShape : Shape :=
  .sum .unit (.product .parameter .recursive)

def branchingShape : Shape :=
  .function .parameter .recursive

def negativeShape : Shape :=
  .function .recursive .parameter

theorem listShape_isPositive :
    recursiveOccurrencesArePositive .positive listShape = true := rfl

theorem branchingShape_isPositive :
    recursiveOccurrencesArePositive .positive branchingShape = true := rfl

theorem negativeShape_isRejected :
    recursiveOccurrencesArePositive .positive negativeShape = false := rfl

/-!
`1 + A × X` はリストの一層を表し、`X` は積の正の位置に現れます。`A → X` も `X` が関数の出力側なので
正です。一方 `X → A` は再帰対象を入力として消費し、極性が反転します。このような負の出現を許して
無条件の最小不動点と除去原理を作ると、単調性が失われ、論理的一貫性や停止性を壊し得ます。

極性を符号 $p\in\{+,-\}$ で書くと、積と和は極性を保存し、関数型の始域だけが反転します。

$$
\mathsf{pol}_p(A\to B)
  =\mathsf{pol}_{-p}(A)\land\mathsf{pol}_{p}(B).
$$

本章のBool判定器は教育用の単純な型コードに対する検査です。Leanの実際のstrict positivity checkerの
完全な仕様ではありません。相互帰納、入れ子、パラメータ、索引を含む現行の受理条件は [LEAN-REF] で
確認し、概念上の厳密正値性と特定実装の判定アルゴリズムを区別します。

## 要点

* 帰納族の構成子は、引数だけでなく結果が属するファイバーを指定する。
* 依存除去のmotiveは添字と値の両方に依存し、構成子ごとの場合と帰納仮定を要求する。
* 束縛を持つ帰納構文の名前変更では、束縛子の下で添字写像を持ち上げる。
* 厳密正値性は再帰対象が関数入力などの負の位置に現れることを禁じる。
* 概念上の正値性判定とLean実装の完全な受理規則を同一視しない。

## 研究史と文献案内

Dybjerの1994年論文 [DYB94] はMartin-Löf型理論における帰納族を、添字・構成子・除去規則を含む
一般的な枠組みで扱います。本章の `Expr` はその理論全体ではなく、束縛を含む一つの代表例です。
帰納定義と型理論の一般的構成は [ML84] を参照してください。プログラミング言語での帰納型と
再帰原理は [PFPL16] が扱います。Lean 4の現行帰納宣言と正値性検査は [LEAN-REF] で確認します。

## 問題

### `Expr` の除去原理を規則から復元する

`Expr.rec` の型を調べる前に、motiveと四構成子の場合の型を通常の依存型記法で予想してください。
その後Leanが生成したrecursorと比較し、let本体の帰納仮定だけが `n+1` のファイバーに属することを
確認します。`evaluate` の各分岐をrecursorの引数へ対応づければ完了です。

### 名前変更と環境評価の可換性を証明する

名前変更 `ρ : Fin n → Fin m` と二環境が `environment₁ i = environment₂ (ρ i)` を満たすとします。
`evaluate environment₂ (rename ρ expression) = evaluate environment₁ expression` を式の帰納法で証明してください。
let分岐で環境拡張間の対応を補題として分離し、束縛変数と外側の変数の二場合を示せば完了です。

### 正値性の境界例を分類する

次の五形を `Shape` で表してください：`X × X`；`A → X`；`X → A`；`(X → A) → A`；
`(A → X) → X`。それぞれの再帰出現について極性を根から追跡します。Bool判定の結果だけでなく、
関数入力を通るたびに符号が反転する経路を
注記します。Leanの実際の帰納宣言として受理されるかを別に調べ、差があれば簡略コードの限界を説明します。
-/

end FormalLab.TypeTheory.GeneralInductiveFamilies