/-!
# 第7章：命題論理と構成的・古典的推論

複合命題を理解するには真理表だけでは足りません。`P ∧ Q` の証明は二つの証明を保持し、
`P ∨ Q` の証明はどちらを選んだかを保持します。証明を構成として読むと、論理結合子ごとに
「何を与えれば作れるか」と「作った証明から何を取り出せるか」が決まります。

本章では連言・選言・否定・同値を導入規則と除去規則から調べます。そのうえで、構成的に
証明できるDe Morgan則と、排中律のような古典原理を必要とする向きを証明項から見分けます。
論理法則を名前で暗記せず、入力情報と出力情報の変換として再構成することが目標です。

## 複合命題はどの形の証拠を要求するか

| 命題 | 証明を作る（導入） | 証明を使う（除去） |
|---|---|---|
| `P ∧ Q` | `P` と `Q` を両方与える | 左右の証明を取り出す |
| `P ∨ Q` | 左右どちらかを選んで与える | 両場合から同じ結論を作る |
| `¬P` | `P → False` を作る | `P` へ適用して矛盾を得る |
| `P ↔ Q` | 二方向の含意を与える | 必要な方向の関数を使う |

## 真理表から証拠の形へ

古典的な真理表は複合命題の真理条件を要約します。しかしLeanで証明を構成するには、
「真なら何が手元にあるか」をさらに知る必要があります。`P ∧ Q` の証明は二つの証明を
同時に保持し、`P ∨ Q` の証明はどちらを選んだかという印と、その側の証明を保持します。

したがって連言と選言は、どちらも二命題を組み合わせても証拠の形が異なります。

連言の導入と二つの射影は、次の規則で表せます。

$$
\frac{\Gamma\vdash p:P\qquad\Gamma\vdash q:Q}
     {\Gamma\vdash \langle p,q\rangle:P\land Q}
\qquad
\frac{\Gamma\vdash h:P\land Q}{\Gamma\vdash \pi_1(h):P}
\qquad
\frac{\Gamma\vdash h:P\land Q}{\Gamma\vdash \pi_2(h):Q}.
$$

選言には左右二つの導入があり、除去時には両方の可能性を処理します。

$$
\frac{\Gamma\vdash p:P}{\Gamma\vdash \mathsf{inl}(p):P\lor Q}
\qquad
\frac{\Gamma\vdash q:Q}{\Gamma\vdash \mathsf{inr}(q):P\lor Q}
$$

$$
\frac{\Gamma\vdash s:P\lor Q\qquad
      \Gamma,p:P\vdash r_P:R\qquad
      \Gamma,q:Q\vdash r_Q:R}
     {\Gamma\vdash \mathsf{case}(s,p.r_P,q.r_Q):R}.
$$

この違いが除去規則を決めます。連言からは片側を直接射影できますが、選言から結論を得るには
左右のどちらでも同じ結論へ到達する二つの方法が必要です。

## 否定は新しい原始記号ではない

Leanで `¬P` は `P → False` の記法です。否定の証明は、`P` の証明を受け取ると矛盾へ
変換できる関数です。「`P` が偽という真理値を観察した」という意味ではありません。
この定義から、二重否定の導入 `P → ¬¬P` は構成的に得られます。

$$
\neg P\;\overset{\mathrm{def}}{=}\;P\to\mathsf{False}.
$$


-/

namespace FormalLab.Logic.Connectives

/-! ## 連言と選言の証拠を構成する -/

/-- 連言の二成分を交換します。山括弧は二つの証明を同時に構成します。 -/
theorem swapAnd (P Q : Prop) : P ∧ Q → Q ∧ P :=
  fun proof => ⟨proof.right, proof.left⟩

/-- 選言を使い、左右どちらの場合からも同じ結論 `R` を得ます。 -/
theorem eliminateOr (P Q R : Prop) : (P → R) → (Q → R) → P ∨ Q → R :=
  fun fromP fromQ choice => Or.elim choice fromP fromQ

/-- 連言は選言の各場合へ分配できる。各枝で同じ外側の証明を再利用します。 -/
theorem distributeAndOverOr (P Q R : Prop) :
    P ∧ (Q ∨ R) → (P ∧ Q) ∨ (P ∧ R) := by
  intro proof
  cases proof.right with
  | inl q => exact Or.inl ⟨proof.left, q⟩
  | inr r => exact Or.inr ⟨proof.left, r⟩

/-- 含意を二段階に合成します。 -/
theorem implicationTransitive (P Q R : Prop) : (P → Q) → (Q → R) → P → R :=
  fun pq qr p => qr (pq p)

/-! ## 否定と同値 -/

/-- `P` の証明から、`P` を否定すると矛盾することを構成する。 -/
theorem introduceDoubleNegation (P : Prop) : P → ¬¬P :=
  fun p notP => notP p

/-- 同値は両方向の含意です。 -/
theorem iffReflexive (P : Prop) : P ↔ P :=
  ⟨fun p => p, fun p => p⟩

/-- このDe Morgan則は排中律を使わず構成できます。 -/
theorem notOrIff (P Q : Prop) : ¬(P ∨ Q) ↔ ¬P ∧ ¬Q := by
  constructor
  · intro noChoice
    exact ⟨fun p => noChoice (Or.inl p), fun q => noChoice (Or.inr q)⟩
  · intro bothNot choice
    exact Or.elim choice bothNot.left bothNot.right

/-! ## 古典原理を使う箇所を可視化する -/

/-- 排中律は `Classical.em` を明示して使用します。 -/
theorem excludedMiddle (P : Prop) : P ∨ ¬P :=
  Classical.em P

/-- 二重否定除去は古典原理を明示すれば得られる。 -/
theorem eliminateDoubleNegation (P : Prop) : ¬¬P → P := by
  intro notNotP
  cases Classical.em P with
  | inl p => exact p
  | inr notP => exact False.elim (notNotP notP)

/-- 必要な排中律を引数へ出すと、古典原理への依存箇所を型に表示できます。 -/
theorem notAndToOrNotOfEm (P Q : Prop) (emP : P ∨ ¬P) :
    ¬(P ∧ Q) → ¬P ∨ ¬Q := by
  intro notBoth
  cases emP with
  | inl p =>
      exact Or.inr (fun q => notBoth ⟨p, q⟩)
  | inr notP =>
      exact Or.inl notP

/-!
## 構成的と古典的の境界を証明項で追う

`introduceDoubleNegation` は与えられた `p : P` を使うだけです。一方、一般の
`eliminateDoubleNegation` は `P` の証拠を `¬¬P` から直接取り出せないため、
`Classical.em P` で `P` と `¬P` の分岐を追加します。結論だけでなく、証明項がどの定数へ
依存するかを見ることで、古典原理の使用箇所を局所化できます。

`notAndToOrNotOfEm` はその局所化を定理の型にまで反映します。`emP` を与えた後の本体は、連言・選言・
含意・偽の規則だけで構成されています。古典論理を「証明全体の雰囲気」として分類せず、追加した原理を
引数または定数として特定できます。

## De Morgan則を情報の変換として読む

`¬(P ∨ Q) → ¬P ∧ ¬Q` では、左選択 `Or.inl p` と右選択 `Or.inr q` をそれぞれ否定へ
渡して二つの否定を作ります。逆向きでは、選言がどちらの構成子で作られたかを調べ、対応する
否定を適用します。真理表の一行ではなく、証拠がどう流れるかを追うと構成的である理由が
分かります。

## 構成的証明と古典原理

場合分け `Or.elim` は、すでに与えられた `P ∨ Q` の証明に含まれる分岐を使います。
排中律 `Classical.em P` は、任意の `P` についてその分岐を追加原理として与えます。
両者を「場合分け」と一括りにしません。

`P ↔ Q` と `P = Q` も同じではありません。同値は二方向の証明変換を持つ命題です。
命題そのものの等式へ移すには、次章以降で使う命題外延性 `propext` が必要です。

## 要点

結合子の意味は証明の構成法・使用法・導入直後の計算で読めます。連言は対、選言は側を記録した選択、否定は
`False` への関数、同値は二方向の関数です。構成的証明は入力証拠を規則に沿って変換し、古典的証明は
排中律などの追加原理を定数または明示した仮定として使います。

## 研究史と文献案内

Heytingは1930年に、直観主義論理の形式規則を提示しました [HEY30]。Kolmogorovは1932年に、
命題を問題、証明を解法として解釈しました [KOL32]。両者の仕事を同じ意味論の別表現とはしません。
自然演繹の導入・除去と正規化は [GLT89]、構成的論理と型理論の体系的関係は [ML84] が扱います。
Leanで古典原理がどの定数として加わるかは [LEAN-REF] を参照してください。

## 問題

### 導入規則と除去規則から証明の情報流を作る

連言、選言、否定、同値について、導入時に必要な証拠と除去時に得られる証拠を表にしてください。
表を使い `P ∧ Q → P ∨ Q` の二つの証明項を構成し、連言が持っていたどちらの証拠を選言のタグの中へ残し、どちらを捨てたかを記述します。

`notOrIff` の両方向を同じ表で追跡し、構成子、場合分け、関数適用がどの導入・除去規則に対応するかを行ごとに注記してください。
証明の各中間項に型を与え、情報が消失したり新しく捏造されたりしていないことが検証基準です。

### 分配則を導出木とLeanの場合分けで二重に記述する

`P ∧ (Q ∨ R) → (P ∧ Q) ∨ (P ∧ R)` の導出木を書きます。連言から `P` と `Q ∨ R` を取り出す節点、
選言で二分する節点、各枝で連言と最終的な選言を作る節点を明示してください。二枝が同じ結論型を持たなければ `Or.elim` を完了できないことも型で示します。

次に同じ導出をLeanで実装し、導出木の各節点と証明項の部分項を対応させます。
`Or.elim` と `Classical.em` の両方が二分を作るという外見上の類似だけでなく、前者が必要とする入力証拠と後者が追加する原理の差を述べてください。

### 古典原理を使った一点だけを定理の仮定へ抽出する

`¬(P ∧ Q) → ¬P ∨ ¬Q` の証明において、排中律をどの命題に対して一回だけ使えばよいかを決めます。
その排中律の証拠を関数の引数として外へ出し、残りの証明が構成的な規則だけで書ける定理の型と本体を作ってください。

二重否定導入 `P → ¬¬P` とその逆向きを比較し、証明項を単に「逆にする」操作が定義されない理由を、関数の始域・終域から説明します。
解答の最後に、どの行までが構成的に成立し、どの一行が追加仮定に依存するかを明示します。
-/

end FormalLab.Logic.Connectives