import FormalLab.TypeTheory.DependentTypes

/-!
# 第34章：部分型と篩型

自然数全体ではなく正の自然数だけを受け取る関数を考えます。呼び出すたびに `0 < n` を
仮定として渡す代わりに、値 `n` と条件の証明を一つの型へまとめれば、検査済みという事実を
関数の入口で再利用できます。この「値の集合を述語で絞る」発想には、基礎理論と型検査方式の
異なる複数の篩型（refinement type）があります。

本章ではLeanの `Subtype` を値成分と証明成分から構成し、検査前の値から安全に移る境界を
`Option` で表します。その後、一般の篩型、述語集合、Σ型、添字付き帰納族との違いを比較します。
この比較により、Leanの部分型を篩型研究全体と同一視しない基準を得ます。

## 値とその値が満たす条件を一つの型にする

型 $A$ と述語 $P:A\to\mathsf{Prop}$ から、条件を満たす値だけを集める型を

$$
\{x:A\mid P(x)\}
$$

と書きます。この記号が集合の内包表記か篩型かは文献の基礎理論に依存します。
型理論的には項を作るために `a : A` と `p : P(a)` の両方が必要です。

Leanの `{x : A // P x}` は `Subtype P` の記法です。項は `val : A` と
`property : P val` を持ち、第二成分は `Prop` の証明です。

「篩う」とは、元の値を実行時に自動検査して除外することとは限りません。Leanの部分型を
直接構成するときは、値だけでなく条件の証明も渡します。いったん構成できれば、利用側は
条件を再検査せず `property` として使えます。証明責任が消えるのではなく、値を作る境界へ
移動します。


-/

namespace FormalLab.TypeTheory.SubtypesAndRefinements

/-!
## 値と条件の証明を同時に構成する

部分型の形成・導入・除去を分けて読みます。

* **形成**：`α : Type` と `p : α → Prop` から `{x : α // p x}` を作る。
* **導入**：`value : α` と `proof : p value` から `⟨value, proof⟩` を作る。
* **除去**：`n.val` で元の値、`n.property` でその値に対応する証明を得る。

第二成分の型に第一成分が現れるため、誤った値と正しい証明を別々に組み合わせることは
できません。

形成・導入・二つの射影は、通常の記法では次の判断として表せます。

$$
\frac{A:\mathsf{Type} \qquad P:A\to\mathsf{Prop}}
     {\{x:A\mid P(x)\}:\mathsf{Type}}
\qquad
\frac{a:A \qquad p:P(a)}
     {\langle a,p\rangle:\{x:A\mid P(x)\}}
$$

$$
\pi_1\langle a,p\rangle \equiv a
\qquad
\pi_2\langle a,p\rangle : P(\pi_1\langle a,p\rangle).
$$

記号 $\equiv$ は、ここでは射影を計算すると定義展開だけで同じ項へ簡約されることを表します。Leanでは
$\pi_1$ が `.val`、$\pi_2$ が `.property`、対 $\langle a,p\rangle$ が `⟨a, p⟩` に対応します。
-/

/-- 正であるという証明を伴う自然数です。 -/
def PositiveNat :=
  {n : Nat // 0 < n}

/-- 値 `1` と `0 < 1` の証明を組にします。 -/
def one : PositiveNat :=
  ⟨1, Nat.zero_lt_succ 0⟩

/-- 値を増やすと同時に、正値性も保存します。 -/
def succ (n : PositiveNat) : PositiveNat :=
  ⟨n.val + 1, Nat.zero_lt_succ n.val⟩

/-- 通常の自然数を検査し、証明できた場合だけ正の自然数へ精密化します。 -/
def toPositive? (n : Nat) : Option PositiveNat :=
  if h : 0 < n then some ⟨n, h⟩ else none

/-- 入力 `n` の正値性検査について、成功値または0である証明を保持します。 -/
inductive PositiveClassification (n : Nat) where
  | positive (value : PositiveNat) (sameValue : value.val = n)
  | zero (proof : n = 0)

/-- 検査失敗時にも、入力が0だったという証明を残します。 -/
def classifyPositive (n : Nat) : PositiveClassification n :=
  if h : 0 < n then
    .positive ⟨n, h⟩ rfl
  else
    .zero (Nat.eq_zero_of_not_pos h)

#eval (toPositive? 3).map Subtype.val
#eval (toPositive? 0).map Subtype.val

/-!
`toPositive?` は外部から未検証の値を受け取る境界の一例です。`if h : 0 < n` は条件を判定
するだけでなく、真の分岐へ証明 `h` を導入します。任意の `Prop` が自動的に判定可能な
わけではないので、この変換は一般の部分型について常に書けるわけではありません。

`Option` の `none` は失敗理由を保持しません。`classifyPositive` は成功側に証明付きの値と元の入力との等式を、
失敗側に `n = 0` の証明を返します。自然数では「正でない」と「0」が一致するために書ける分類です。一般の型と述語では、
否定側に返せるのは通常 $\neg P(a)$ であり、さらに具体的な理由が得られるとは限りません。
-/

/-! ## 入力型に事前条件を持たせる -/

/-- 正値性は入力の `.property` から再利用できます。 -/
theorem positiveProperty (n : PositiveNat) : 0 < n.val :=
  n.property

/-- 正の入力だけを受け取るため、関数内部に失敗分岐がありません。 -/
def predecessor (n : PositiveNat) : Nat :=
  n.val - 1

example : predecessor one = 0 := rfl

/-- 上界未満という条件を引数化した部分型です。 -/
def Below (bound : Nat) :=
  {n : Nat // n < bound}

def zeroBelowSucc (bound : Nat) : Below (bound + 1) :=
  ⟨0, Nat.zero_lt_succ bound⟩

/-! ## 証明成分ではなく値成分が部分型の同一性を決める -/

/-- 値成分が等しい二つの部分型の項は等しい。 -/
theorem ext {m n : PositiveNat} (sameValue : m.val = n.val) : m = n :=
  Subtype.ext sameValue

/-!
`Subtype.ext` が証明成分の等しさを要求しないのは、`Prop` の証明無関係性によります。
ただし、条件 `p` が不要だという意味ではありません。値を構成し利用可能な操作を制限する
役割は型検査時に果たし、同じ値に付いた証明の作り方だけを同一性から無視します。
-/

#eval one.val
#eval (succ one).val
#check (bound : Nat) → Below (bound + 1)

/-!
## `Subtype`の等式と証明無関係性

Leanの `{x : α // p x}` は `Subtype p` の記法で、値フィールド `val` と `Prop` に属する
証明フィールド `property` を持ちます。`Subtype.ext` が値成分の等式だけを要求するのは、
一般の篩型という語の定義からではなく、Leanの `Prop` における証明無関係性から
従います。自動的な制約解消やSMTによる型検査も `Subtype` 自体の機能ではありません。

## 部分型と一般の篩型

一般の篩型システムには、決定可能な述語だけを許す設計、SMTで条件を自動証明
する設計、実行時検査を挿入する設計などがあります。Leanの `Subtype` は任意の
`Prop` の**証明項を利用者が構成する**依存型です。自動化の有無や実行方式まで含めて
同一だとはしません。

条件を型へ移すと利用側は安全になりますが、構成側は証明を要求されます。これは情報を
消す最適化ではなく、証明責任を境界へ移動する設計です。

部分型は既存の型から値を選ぶので、後の添字付き帰納族のようにデータの構成方法そのものを
再設計するわけではありません。また述語集合 `α → Prop` は所属条件だけですが、部分型は
実際の値とその所属証明を項として持ちます。

## 述語・部分型・存在命題・依存対を分ける

同じ記号を似た目的で使えても、次の四つは所属するsortと除去規則が異なります。

| 表現 | Leanでの代表形 | 属するsort | 項が保持するもの |
|---|---|---|---|
| 述語 | `P : α → Prop` | 関数型 | 値ごとの命題を返す規則 |
| 部分型 | `{x : α // P x}` | `Sort (max 1 u)` | 実行時の値 `x` と、消去される証明 |
| 存在命題 | `∃ x : α, P x` | `Prop` | 命題が真である証拠。一般のデータへ証人を取り出せない |
| 依存対 | `Σ x : α, B x` | `Type` | 第一成分と、それに依存する計算上のデータ |

述語 $P$ は「どの値を選ぶか」を記述しますが、それ自体は選ばれた値ではありません。部分型は射影
$\pi_1:\{x:A\mid P(x)\}\to A$ を持つため、項から元の値を計算に使えます。存在命題は命題全体が `Prop` に属し、
Leanの制限付き除去により、一般のデータ型へ証人を取り出すプログラムは定義できません。

依存対 $\Sigma x:A.\,B(x)$ では第二成分 $B(x)$ も計算上のデータです。部分型では第二成分が `Prop` の証明なので、
Leanのコンパイラはそれを消去し、実行時には基底型の値と同じ表現を使います。このゼロオーバーヘッド性と
`Subtype.ext` の等式原理はLean固有の `Prop` とコンパイル規則に由来し、篩型一般の定義からは従いません。

## 仕様として強くしても値は増えない

二つの述語 $P,Q:A\to\mathsf{Prop}$ が全ての $x$ について $Q(x)\to P(x)$ を満たすとします。このとき、
より強い条件 $Q$ の部分型から $P$ の部分型へ、値を変えずに写せます。
-/

/-- より強い条件の部分型を、値を保ったまま弱い条件の部分型へ写します。 -/
def weakenSubtype {α : Type} {p q : α → Prop}
    (implies : ∀ x, q x → p x) : Subtype q → Subtype p
  | ⟨x, hx⟩ => ⟨x, implies x hx⟩

theorem weakenSubtype_preserves_value {α : Type} {p q : α → Prop}
    (implies : ∀ x, q x → p x) (x : Subtype q) :
    (weakenSubtype implies x).val = x.val :=
  rfl

/-!
数学的には、含意 $\forall x.\,Q(x)\to P(x)$ が部分型間の忘却写像を誘導します。Leanの `weakenSubtype` では
値成分をそのまま保ち、証明成分だけを含意で変換します。逆向きには一般に写せません。弱い条件 $P(x)$ から強い
条件 $Q(x)$ は導けないからです。篩型の「精密さ」は値へ新しい計算を施す順序ではなく、要求する述語の強さに
よる順序として現れます。

## 要点

* 部分型 `{x : α // p x}` の項は値 `x` と、その値についての証明 `p x` を持つ。
* 条件を入力型へ移すと、利用側は証明済みの事前条件を再利用できる。
* 未検証値から部分型を作るには証明が必要で、判定可能なら `Option` を返す検査境界も書ける。
* 証明無関係性により、同じ値を持つ部分型の項は証明の作り方によらず等しい。
* 述語集合・部分型・添字付き帰納族は、似た不変条件を異なる位置に持たせる。

## 研究史と文献案内

Freeman–Pfenningの1991年の篩型 [FP91] は、MLのdatatypeを精密化する体系です。
Leanの `Subtype` と同じ型形成・推論方式ではありません。その後の篩型研究には
決定手続き、制約生成、SMT連携など複数の設計があります。型精密化を言語体系の中で比較する
には [PFPL16]、Leanの `Subtype` と証明無関係性の現行仕様は [LEAN-REF] を参照します。

## 問題

### 値と性質を一つの項として構成する

`one : PositiveNat` の値成分と証明成分を指し、`PositiveNat` を `Nat` へ射影したとき何が失われるか
を説明せよ。二つの正の自然数の和を再び `PositiveNat` として返す関数を定義し、値の計算と閉性の
証明を分けて記述する。

対照として `{n : Nat // n < 0}` の項を構成しようとし、失敗が自然数の値の不足ではなく証明成分の
不可能性に由来することを構成子の型から示す。

### 検査から精密な型へ移す

`toPositive?` の成功・失敗の各分岐で得られる仮定を展開し、実行時の比較結果が後続の証明でどう
使われるかを追え。入力が正なら証明付きの値を返し、そうでなければ失敗の理由を返す改良版を設計し、
結果型が保持する情報を比較する。

述語を判定することと、述語の証明を型の成分として保存することを区別せよ。全ての述語が計算可能な
判定手続きを持つわけではない点も、構成と検証を混同せずに説明すること。

### 三つの精密化表現と研究史を比較する

偶数を、述語集合、Leanの部分型、偶数専用の帰納型で表現し、構成・除去・計算・証明の再利用を
比較せよ。同じ外延を表していても、どの情報を構文へ組み込むかで帰納原理と定義的計算が変わる。

さらに [FP91] の篩型とLeanの `Subtype` を、基礎言語、型検査、証明項の保持の三点で
比較する。「篩型」は広い研究領域の標準訳として用いつつ、特定の体系とLeanの一構成子を同一視
しない記述にすること。
-/

end FormalLab.TypeTheory.SubtypesAndRefinements