/-!
# 第6章：命題・証明・含意

「二は偶数である」という主張と、その主張を正当化する証明は同じものではありません。
型理論ではこの差を、命題 `P` とその型を持つ項 `p : P` の差として表します。すると含意の
証明は証明を別の証明へ変換する関数となり、仮定を置くことは入力を束縛することになります。

本章では `Prop`、証明項、含意、真と偽を、前章までの型・関数・帰納型から組み立てます。
証明項そのものと、それを作るtactic記法も分けます。この読み方が、結合子、量化、等式、
そして命題＝型対応の全体を貫きます。

## 真理値ではなく証拠を要求する

自然演繹では、命題が整形式であることと、その命題が証明されたことを区別します。文脈 $\Gamma$ の下で

$$
\Gamma\vdash P\;\mathsf{prop}
\qquad\text{と}\qquad
\Gamma\vdash p:P
$$

は、それぞれ「$P$ は命題である」と「$p$ は $P$ の証明である」を表します。

propositions-as-typesの読みでは命題 `P` を型、判断 `p : P` を「`p` は `P` の証明」と
解釈します。
命題を宣言しただけでは証明になりません。その型の項を構成して初めて証明になります。

## `Prop`と`Bool`は異なる問いに答える

`Bool` の値 `true` と `false` は計算で分岐するためのデータです。判断 $b:\mathsf{Bool}$ は
$b$ を計算すれば二値のいずれかを得ることを述べます。これに対して $P:\mathsf{Prop}$ は
証明されるべき主張を分類し、一般には $P$ を実行して真偽値へ評価するとは考えません。

決定可能な命題では両者を結ぶ仕組みを作れますが、最初から同じものではありません。
この区別により、数学的推論とプログラムの条件分岐を必要な箇所だけ接続できます。

## 証明とは型を満たす構成である

命題を型として読むと、証明規則をデータの規則と同じ三側面で整理できます。

* **導入規則**：その命題の証明をどう作るか。
* **除去規則**：得た証明から何を取り出せるか。
* **計算規則**：導入直後に除去したとき何へ簡約するか。

これは「真である命題には適当な値を割り当てる」という符号化ではありません。命題の意味を、
その証明の構成法と使用法によって与えます。

含意 `P → Q` は関数型です。証明は `P` の証明を入力として `Q` の証明を返します。
この対応は比喩ではなく、Leanが検査する項そのものです。

自然演繹における含意の導入・除去規則は、関数の抽象・適用規則と同じ形を持ちます。

$$
\frac{\Gamma,p:P\vdash q:Q}{\Gamma\vdash (\lambda p.q):P\to Q}
\;(\to\mathrm{I})
\qquad
\frac{\Gamma\vdash f:P\to Q\qquad\Gamma\vdash p:P}
     {\Gamma\vdash f\,p:Q}
\;(\to\mathrm{E}).
$$

導入直後に除去すれば、仮引数へ実引数を代入して簡約します。

$$
(\lambda p.q)\,a\equiv q[a/p].
$$

$q[a/p]$ は、$q$ に自由に現れる $p$ を $a$ で置き換え、束縛変数の捕獲を避けた項です。

非型付きラムダ計算と並べると、対応する操作は三つあります。仮定 `p : P` の下で
`q : Q` を構成して仮定を閉じることはラムダ抽象、含意の証明を前件の証明へ使うことは
関数適用、適用した抽象を代入で簡約することは証明の正規化です。構文が似ているから
対応するのではなく、導入・除去・計算の三規則が揃って対応します。

## 文脈と仮定

証明中の `p : P` は「`P` を無条件に証明した」という宣言ではなく、現在の文脈で使える
仮定です。`fun p => q` または `intro p` はその仮定を導入し、最終的に `P → Q` の証明へ
閉じます。自然演繹で仮定を解除する操作と、関数のラムダ抽象が対応しています。

真と偽も構成法と使用法によって特徴づけられます。真には引数なしの導入があり、偽には導入規則が
ありません。偽の証明を仮定した場合に限り、任意の命題を結論としてよいという除去規則があります。

$$
\frac{}{\Gamma\vdash \mathsf{trueIntro}:\mathsf{True}}
\qquad
\frac{\Gamma\vdash h:\mathsf{False}}{\Gamma\vdash
\mathsf{falseElim}(h):P}.
$$


-/

namespace FormalLab.Logic.Propositions

/-! ## 含意を証明の変換として構成する -/

/-- `P` の証明を受け取り、同じ証明を返します。 -/
theorem identityProof (P : Prop) : P → P :=
  fun proofOfP => proofOfP

/-- 含意とその前件から後件を得るmodus ponensです。 -/
theorem modusPonens (P Q : Prop) (implication : P → Q) (proofOfP : P) : Q :=
  implication proofOfP

/-!
`modusPonens` では新しい証明原理を呼んでいません。`implication` はすでに関数なので、
`proofOfP` へ適用すれば `Q` の証明になります。論理の除去規則が関数適用そのものです。
-/

/-- 二つの含意を証明変換として合成する。 -/
theorem composeImplications (P Q R : Prop) : (P → Q) → (Q → R) → P → R :=
  fun pq qr p => qr (pq p)

/-!
上の証明は `:=` の右へ項を直接書く**term mode**です。`:= by` から始める
**tactic mode**では、現在の目標を段階的に変形します。まず次の二語だけを使います。

* `intro h`：含意の前件を仮定 `h` として導入する。
* `exact p`：現在の目標と同じ型を持つ項 `p` を渡して閉じる。

tactic modeは別種の証明ではありません。tacticが途中目標を操作して、最後にはterm modeで
書ける証明項を生成します。kernelが検査するのはtacticの実行履歴ではなく生成された項です。
-/

/-- 同じ恒等証明をtactic modeで書いたものです。 -/
theorem identityProofTactic (P : Prop) : P → P := by
  intro proofOfP
  exact proofOfP

/-! ## 常に真である命題と、構成子を持たない命題 -/

/-- `True` の基本構成子です。 -/
theorem truth : True :=
  True.intro

/-- `False` の証明を仮定すると、任意の命題を導けます。 -/
theorem falseElimination (P : Prop) : False → P :=
  fun impossible => False.elim impossible

/-- 同じ命題の二つの証明は等しい。Leanの証明無関係性の直接の帰結です。 -/
theorem proofsEqual (P : Prop) (first second : P) : first = second :=
  Subsingleton.elim first second

#check Prop
#check True.intro
#check False.elim

/-!
`False` から何でも導けることは、`False` の証明を作れたという意味ではありません。
`False` は構成子を持たず、`falseElimination` は到達不能な入力の使用法だけを定めます。

`True` と `False` は真理値の二値データではありません。`True` は引数なしの構成子
`True.intro` を持つため常に証明でき、`False` は構成子を持たないため閉じた証明を作れません。
この構成子の有無が、それぞれの導入・除去規則を決めます。

## 証明を一行ずつ読む

`composeImplications` の型は三つの矢印を右結合して読みます。二つの証明変換 `pq` と `qr` を
受け取った後、`p : P` を仮定します。`pq p : Q`、続いて `qr (pq p) : R` です。最後の式の型が
目標と一致するため証明が完了します。論理記号を消しても、先に学んだ関数合成と同じ型の流れです。

## `Prop`の証明無関係性とtacticの役割

`P : Prop` はLeanのsortに属する命題で、`p : P` はその証明項です。Leanの `Prop` では
証明無関係性がkernelの設計に組み込まれています。一方、`by` 以下のtactic列は論理規則そのもの
ではなく、最終的な証明項を構成するためのelaborator上の記法です。したがって本文では、命題の
内容をtactic名で定義せず、tacticを用いた場合も生成される仮定と結論を別に説明します。

`#check Prop` の結果に現れる `Prop : Type` は、命題と計算データが同一だという主張ではありません。
Leanでは `Prop` は `Sort 0` の表記であり、それ自身の型は `Sort 1`、すなわち `Type` です。この宇宙上の
位置づけと、`Prop` の項に対する証明無関係性や除去制限とは別の規則です。

## 命題・証明・計算データを区別する

Leanでは同じ命題の二つの証明は証明無関係性によって等しいものとして扱われます。
しかし異なる計算データは一般に等しくありません。`Prop` の証明と `Type` のデータの
差は、存在命題とΣ型、部分型を比較するときに再び使います。

命題＝型対応は、全ての型を命題と呼ぶ主張でも、全てのプログラムを数学的証明と呼ぶ主張でも
ありません。`P : Prop` は証明を要求する命題であり、`Nat : Type` は計算に使う自然数の型です。
両者は項を型で分類するという形を共有しますが、証明から計算データを取り出せる範囲は同じではありません。

## 要点

命題は `Prop` の項、証明はその命題を型に持つ項です。含意の形成・導入・除去・計算は関数型の
規則であり、真と偽の振舞いは構成子の有無から導かれます。tacticは証明項を組み立てる方法です。
`Bool` の計算、`Prop` の宇宙上の位置、証明無関係性は互いに異なる側面として区別します。

## 研究史と文献案内

命題を型、証明を項として読む見方は後にCurry–Howard対応と呼ばれます。Curryの1934年の
組合せ論理での結果 [CUR34] と、Howardの1969年原稿・1980年刊行論文 [HOW80] は対象範囲が
異なります。Brouwer、Heyting、Kolmogorovの仕事をまとめる “BHK” も後世の呼称です
[HEY30; KOL32]。自然演繹・正規化・型の対応は [GLT89]、Leanの証明無関係な `Prop` の
固有仕様は [LEAN-REF] を参照してください。

## 問題

### 命題とその証明を異なるsortの対象として読む

`P : Prop` と `p : P` に現れる二つのコロンを分析し、左辺と右辺の役割をそれぞれ書いてください。
`Bool` の値 `true`、`false` と、`Prop` に属する命題、その命題を型として持つ証明項を三列の表にし、それぞれに可能な観察を示します。

次に、同じ命題の二つの証明に対するLeanの証明無関係性と、二つの自然数の等式を比較します。
両者に同じ論法を適用できない理由を、項が属するsortと、証明から計算データを取り出すことへの制約を指して説明してください。

### tactic状態をラムダ抽象と関数適用へ戻す

`by intro p; exact p` の実行前、`intro p` の後、`exact p` の後のゴール状態を書き、証明項 `fun p => p` の構文へ一対一に対応させてください。
その後、`(P → Q) → (Q → R) → P → R` について、外側から順に入力を導入し、各時点で利用できる仮定と目標型を記録します。

解答はterm modeとtactic modeの両方を提示します。両方から得られる最終的なラムダ項を示し、
tacticが証明の代替物ではなく、同じ証明項を構成する対話的な記法であることを検証します。

### 爆発原理の仮定を隠さずに追跡する

`falseElimination : False → P` を「あらゆる命題 `P` を証明する関数」と読むだけでは不十分です。この関数を呼び出すために必要な入力を明記し、
`False` の証明を持たない状態では何も導けないことを型から説明してください。

仮定 `h : False` を明示的に置いた文脈で、異なる二命題 `P`、`Q` を導く証明項を構成し、どの部分だけが共通の矛盾を消費しているかを示します。
最後に定理の型から `h` を消すことができない理由を述べれば、爆発原理と `False` の証明を混同していないことを検証できます。
-/

end FormalLab.Logic.Propositions