/-!
# 第8章：述語・全称量化・存在量化

「自然数は偶数である」は一つの命題ですが、「`n` は偶数である」は `n` によって内容が
変わる述語です。数学では、全ての `n` について同じ方法を与えることと、条件を満たす
具体的な `n` を一つ示すことを、全称量化と存在量化で区別します。

本章では述語を値から命題への関数として導入し、`∀` を任意の入力へ証明を返す依存関数、
`∃` を証人と根拠を保持する命題として読みます。量化子の順序とスコープが情報の依存関係を
変えることまで追跡し、後の依存積・依存和へ橋を架けます。

## 個別の値から命題の族へ

領域 `A` 上の一項述語を `P(x)` と書きます。全称・存在量化の導入規則は、証明で使える
情報を次のように区別します。

$$
\frac{\Gamma,x:A\vdash p(x):P(x)}
     {\Gamma\vdash \lambda x.p(x):\forall x:A.P(x)}
\;(\forall\mathrm I)
\qquad
\frac{\Gamma\vdash a:A\qquad\Gamma\vdash p:P(a)}
     {\Gamma\vdash \langle a,p\rangle:\exists x:A.P(x)}
\;(\exists\mathrm I).
$$

全称の除去は関数適用です。存在の除去では、証人を特定の値と仮定せず、その証人と根拠だけから
証人に依存しない共通の結論を導きます。

$$
\frac{\Gamma\vdash f:\forall x:A.P(x)\qquad\Gamma\vdash a:A}
     {\Gamma\vdash f(a):P(a)}
\;(\forall\mathrm E)
$$

$$
\frac{\Gamma\vdash e:\exists x:A.P(x)\qquad
      \Gamma,x:A,p:P(x)\vdash r:R}
     {\Gamma\vdash \mathsf{unpack}(e,x,p.r):R}
\;(\exists\mathrm E),
$$

ここで結論 $R$ は取り出した $x$ に依存しません。この制約により、存在する証人がどの値かを外側へ
漏らすのではなく、その値に依存しない帰結だけを得ます。

命題 `P : Prop` は一つの主張です。Leanで述語 `p : α → Prop` は各 `x : α` から命題 `p x`
を作る関数です。したがって、述語は真偽値を返す検査関数とは限りません。`p x` は
`Bool` ではなく命題であり、それを成立させるには証明が必要です。

* `∀ x : α, p x` の証明は、任意の `x` から `p x` の証明を返す関数。
* `∃ x : α, p x` の証明は、ある証人 `x` と `p x` の証明。

この二つは「すべて」「ある」という日本語だけでなく、証明が保持する情報の形で理解
します。全称証明はどの入力にも応答できる手続きです。存在証明は実例を内部に持ちます。
ただし存在証明を使う側は、証人が特定の値だと決めつけず、取り出した任意の証人と
その性質だけから結論を作らなければなりません。


-/

namespace FormalLab.Logic.Quantifiers

universe u

/-!
## 値から命題を作る型族

`Nat → Prop` は、自然数を受け取ると命題を返す関数の型です。たとえば「偶数である」
「ある数より小さい」は、対象を一つ入れるまで主張が完成しません。この未完成の主張を
**述語**（predicate）と呼びます。`IsSuccessor` 自体は命題ではなく述語、
`IsSuccessor 1` は命題です。
-/

/-- `0` では偽、後者では真になる、計算で定義した述語です。 -/
def IsSuccessor : Nat → Prop
  | 0 => False
  | _ + 1 => True

/-- `1` は後者なので、定義を計算すると目標は `True` になります。 -/
theorem oneIsSuccessor : IsSuccessor 1 :=
  True.intro

/-!
## 全称量化：任意の入力へ応答する

`∀ x : α, p x` は、より基本的には依存関数型 `(x : α) → p x` です。出力の型が入力
`x` に依存する点だけが、通常の関数型 `α → β` と異なります。

* **導入**：任意の `x` を受け取り、`p x` を証明する関数を作る。
* **除去**：全称証明へ具体的な `a : α` を適用し、`p a` を得る。

「任意の `x`」を証明するとき、`x` に特別な性質を仮定してはいけません。反対に、
全称証明を使うときは必要な値を引数として渡します。次の二つの関数適用
`transform x` と `allP x` が、それぞれ全称証明を特殊化しています。
-/

/-- 各点で `p x → q x` があれば、全称証明を `p` から `q` へ移せます。 -/
theorem mapForall {α : Type u} (p q : α → Prop)
    (transform : ∀ x, p x → q x) (allP : ∀ x, p x) : ∀ x, q x :=
  fun x => transform x (allP x)

/-- 自然数を一つ受け取ってから、その数自身との等式を構成します。 -/
theorem everyNatEqualsItself : ∀ n : Nat, n = n :=
  fun _ => rfl

/-- 全称証明を `2` に適用すると、一つの具体的な命題の証明になります。 -/
example : (2 : Nat) = 2 :=
  everyNatEqualsItself 2

/-!
## 存在量化：証人と根拠を一緒に保持する

`∃ x : α, p x` を証明するには、証人 `witness : α` と、その証人が条件を満たす証明
`proof : p witness` を組にします。`⟨witness, proof⟩` はこの導入規則の記法です。

存在証明を使うときは `⟨x, hx⟩` と分解します。ここで得る `x` は未知ですが、`hx : p x`
との対応は失われません。この依存関係こそ、単に「何かがある」と印を付けるだけではない
存在証明の内容です。
-/

/-- 証人を保ち、その証人についての証明だけを変換します。 -/
theorem mapExists {α : Type u} (p q : α → Prop)
    (transform : ∀ x, p x → q x) : (∃ x, p x) → ∃ x, q x :=
  fun ⟨witness, proof⟩ => ⟨witness, transform witness proof⟩

/-- 証人 `1` を明示して、後者が存在することを示します。 -/
theorem existsSuccessor : ∃ n : Nat, IsSuccessor n :=
  ⟨1, oneIsSuccessor⟩

/-!
`mapExists` を行ごとに読むと、次の情報の流れになります。

1. 入力の存在証明から `witness` と `proof : p witness` を取り出す。
2. `transform witness proof` により、同じ証人について `q witness` を得る。
3. `witness` と新しい証明を再び存在証明に包む。

変換に必要なのは性質の証明だけなので、新しい証人を探索する必要はありません。

## 量化子の順序は情報の依存関係を変える

`∀ n, ∃ m, R n m` では、`n` を見てから `m` を選べます。したがって証人は `n` に依存
して構いません。一方、`∃ m, ∀ n, R n m` では、すべての `n` に先立って一つの `m` を
固定します。一般に両者は同値ではありません。
-/

/-- 各 `n` を見た後なら、それより大きい証人 `n + 1` を選べます。 -/
theorem existsLargerForEveryNat : ∀ n : Nat, ∃ m : Nat, n < m :=
  fun n => ⟨n + 1, Nat.lt_succ_self n⟩

/-- すべての自然数より大きい自然数を一つ先に選ぶことはできません。 -/
theorem noLargestNat : ¬∃ m : Nat, ∀ n : Nat, n < m := by
  intro ⟨m, largerThanEveryNat⟩
  exact Nat.lt_irrefl m (largerThanEveryNat m)

/-- 先に一つの共通証人を持てるなら、各入力に同じ証人を選べます。 -/
theorem commonWitnessGivesPointwiseWitness {α β : Type u} (relation : α → β → Prop) :
    (∃ y, ∀ x, relation x y) → ∀ x, ∃ y, relation x y :=
  fun ⟨witness, allRelated⟩ x => ⟨witness, allRelated x⟩

/-!
## 限定量化は既知の結合子へ分解できる

Leanで「`S` に属するすべての `x`」は、しばしば `∀ x, S x → p x` と書きます。
条件を満たす入力を受け取った場合だけ結論を返す、という意味です。「`S` に属する
ある `x`」は `∃ x, S x ∧ p x` と書き、証人が二つの条件を同時に満たすと記録します。
量化子と含意・連言の役割を入れ替えないことが重要です。

$$
(\forall x\in S.\,P(x))\;\overset{\mathrm{def}}{=}\;
\forall x.\,S(x)\to P(x),
\qquad
(\exists x\in S.\,P(x))\;\overset{\mathrm{def}}{=}\;
\exists x.\,S(x)\land P(x).
$$
-/

/-- `3` 未満の自然数は `3` 以下です。限定全称を含意で表しています。 -/
theorem belowThreeIsAtMostThree : ∀ n : Nat, n < 3 → n ≤ 3 :=
  fun _ h => Nat.le_of_lt h

/-- `3` 未満で、かつ偶数である自然数の具体例として `2` を選びます。 -/
example : ∃ n : Nat, n < 3 ∧ n % 2 = 0 :=
  ⟨2, by decide, by decide⟩

/-! ## 否定と量化 -/

/-- 存在の否定と全称否定の同値は構成的です。 -/
theorem notExistsIffForallNot {α : Type u} (p : α → Prop) :
    (¬∃ x, p x) ↔ ∀ x, ¬p x := by
  constructor
  · intro noWitness x proof
    exact noWitness ⟨x, proof⟩
  · intro allNot ⟨x, proof⟩
    exact allNot x proof

#check fun (p : Nat → Prop) => ∀ n, p n
#check fun (p : Nat → Prop) => ∃ n, p n

/-!
## 量化が保持する情報

`¬∃ x, p x ↔ ∀ x, ¬p x` は構成的です。一方、一般の
`¬(∀ x, p x) → ∃ x, ¬p x` は古典的原理なしには導けません。全称証明を否定するだけでは、
反例となる具体的な証人を計算できるとは限らないからです。また「一意に存在する」
`∃!` は証人同士の等式を含むため、等式を導入する次章で定義します。

Leanの `Exists` は `Prop` に属します。したがって本章で「証人を保持する」とは、存在証明の内部で証人と根拠が
対応しているという論理的意味です。証人を一般の計算データとして外へ返せるという主張ではありません。
計算に使う依存対 `Sigma` とのsortと除去規則の差は、第31章で比較します。

## 要点

この章の核は、量化を真偽の飾りではなく証明の入出力として読むことです。

* 述語は、値を入れると命題になる関数である。
* 全称証明は任意の入力を受け取る依存関数である。
* 存在証明は証人と、その証人に依存する根拠を保持する。
* 量化子の順序は、後で選ぶ情報が前の情報に依存できるかを決める。

## 研究史と文献案内

Fregeの1879年の *Begriffsschrift* [FRE79] は、量化と多重一般性を独自の二次元記法で扱います。
現在の一階述語論理の記号をそのまま用いてはいません。Heytingの1930年の体系 [HEY30] は
直観主義述語論理の形式化です。依存積としての全称量化と依存和・存在の関係は [ML84]、
現代論文の判断記法は [PFPL16] を参照してください。

## 問題

### 全称量化を依存する関数として追跡する

`mapForall` の全変数と仮定に型を書き、任意の `x` に対する `allP x`、`transform x`、`transform x (allP x)` の型を順に導いてください。
この導出を「任意の値を受け取る」段階と「その値で特殊化した証拠を受け取る」段階へ分け、依存関数の入出力として説明します。

`¬∃ x, p x → ∀ x, ¬p x` の証明項を同じ方法で構成し、任意の `x` と `p x` の証拠から、否定された存在証明をどのように作って矛盾を得るかを記述します。
古典原理を使わずに完成したことが、使用した構成子と関数の一覧から確認できれば完了です。

### 存在証明の証人を保存して性質だけを変換する

`mapExists` の入力を、存在証明の分解、証人の保存、証拠の変換、新しい存在証明の構成という四段階に分けてください。
各段階で手元にある項とその型を表にし、新しい証人を探索する操作が一度も現れないことを示します。

その構造を使って `(∃ x, p x ∧ q x) → ∃ x, q x ∧ p x` をterm modeとtactic modeの両方で証明します。
存在証人、連言の二成分、再構成された証拠の対応を明記し、二つの記法が同じ情報変換を表すことを示してください。

### 量化子の順序と限定量化の論理形を反例で固定する

`∀ n : Nat, ∃ m : Nat, n < m` と `∃ m : Nat, ∀ n : Nat, n < m` について、証明が提供しなければならないデータをそれぞれ関数型と対型の言葉で書いてください。
前者には `m := n + 1` を与え、後者には任意の候補 `m` に対する反例 `n := m` を与え、真偽の差が量化子の順序だけから生じることを示します。

最後に、限定全称 `∀ x, S x → p x` と `∀ x, S x ∧ p x` を比較します。`S` を満たさない値が存在する最小の型と述語を選び、
後者が集合外の値にも `S x` を要求するため過強であることを反例で検証してください。
-/

end FormalLab.Logic.Quantifiers