一階述語論理の項モード技法

1. デバッグ：一階述語論理特有の対話テクニック

① Placeholder (`_`) と「値」の推論

存在記号の導入 ⟨_, _⟩ では、1つ目の穴には「具体的な値」を入れますが、Leanに推論を任せられる場合があります。

具体例: h : P a がある状態で ∃ x, P x を示す

example (a : U) (h : P a) : ∃ x, P x :=
  ⟨_, h⟩ -- 1つ目を _ にすると、Infoviewに「Expected: U」と出ますが、
         -- h の型 (P a) を見て、Leanが自動的に _ = a と解釈してくれます。

② インライン `by apply?` の強力さ

全称記号の除去などで、どの順番で引数を渡せばいいか混乱した時、(by apply?) は「値」と「証明」を適切に並べた項を提案してくれます。

2. 磨き上げ：Mathlibスタイル（一階述語論理版）

ここが最も「熟練者」の差が出る部分です。

① 存在記号のフラット化（Nested ⟨ ⟩）

「かつ ()」と同様、多重の存在記号もフラットに書けます。

Before: ⟨x, ⟨y, ⟨z, hpxyz⟩⟩⟩
After: ⟨x, y, z, hpxyz⟩

意図: 「という証拠品と、その性質の証明」という一連のデータを一塊として扱います。

② ドット記法による「全称記号の除去」

全称記号 h : ∀ x, P x は関数なので、通常 h a と書きますが、Mathlibではドット記法を組み合わせて鎖（Chain）のように書くことがあります。

例: (h x).left

意味: 「にを適用して得られた『かつ』の証明の、左側を取り出す」

③ 無名引数 `‹ ›` による「値」の参照

‹ › は命題だけでなく、その型に属する値も拾えます。

具体例:

variable (U : Type) (P : U → Prop)
example (a : U) (h : ∀ x, P x) : P a :=
  h ‹U› -- 今コンテキストにある U 型の要素（つまり a）を探して適用せよ

※ ただし、コンテキストに同じ型の値が複数あるとエラーになるため、値（）については明示的に名前を書く方が一般的です。

3. 一階述語論理の「黄金のルーチン」拡張版

一階述語論理での「磨き上げ」の最終形は、以下のようになります。

-- 演習 9.7.2 より：(∀ x, A x ∧ B x) → ∀ x, A x
example (h : ∀ x, A x ∧ B x) : ∀ x, A x :=
  fun x ↦ (h x).left

Skeleton: fun x ↦ _
Inspect: _ の位置で Expected type: A x を確認。
Refine: 手元の h は ∀ なので、とりあえず x を食わせる → h x は A x ∧ B x 型。
Polish: (h x).left で完成。

1. `exact?`：一階述語論理での凄み

命題論理では exact? は単なるパズルのピース探しでしたが、一階述語論理では**「適切な値（証拠品）を自動で見つけてきてくれる」**ツールに進化します。

具体例: h : P a があるとき、ゴール ∃ x, P x に対して exact? を使う。
Leanの提案: exact ⟨a, h⟩
凄さ: 「どの値を使えばこの述語が成り立つか」という、人間が頭を使うべき「実例の選定」を、Leanがコンテキストから推論して提示してくれます。

2. 暗黙の引数 `{ }` と `@`：数学的構造の解剖

一階述語論理でよく使う「反射律 rfl」や「推移律 trans」などは、実は大量の暗黙の引数を持っています。

通常時: Eq.refl x
@ をつけた時: #check @Eq.refl → ∀ {α : Sort u} (a : α), a = a （実は「どの型（宇宙）の話をしているか」という {α} が隠れています）

デバッグでの活用シーン： 「見た目は同じ x = x なのに、なぜか証明が通らない！」という時、@ をつけて表示させると、片方の x は Nat（自然数）型で、もう片方の x は Int（整数）型だった……というような型の食い違い（型不一致）を暴くことができます。

3. 一階述語論理の「項モード」で差が出る `@` の使い所

一階述語論理の定理を引数として渡す際、Leanの推論が賢すぎて、逆に困ることがあります。

例: Int.add_comm は ∀ x y, x + y = y + x です。
通常は Int.add_comm a b と書けばになります。
しかし、**「この定理自体を変形させたい（高階の操作）」**ときなどは、@Int.add_comm と書いて、まだが適用されていない「真っさらな関数状態」であることを明示する必要があります。

💡 初級者から熟練者への「項モード」視点

一階述語論理を項モードで書くことは、「証明を組み立てる」というより「データを整理する」感覚に近いです。

ツール	中級者（命題論理）	熟練者（一階述語論理）
`exact?`	定理の名前を思い出す	証拠品（値）の組み合わせを教えてもらう
`_` (ホール)	命題の証明を保留する	具体的な値（や）の選定をLeanに丸投げする
`@`	型をチラ見する	数式がどの集合（型）の上で定義されているかを厳密にチェックする

実践してみましょう！

この「暗黙の引数」や「推論」のパワーを体感するために、演習 9.7.1 を項モードの最短コードで書いてみます。

-- 演習 9.7.1
variable (A : Type) (f : A → A) (P : A → Prop)
variable (h : ∀ x, P x → P (f x))

example : ∀ y, P y → P (f (f y)) :=
  fun y hy ↦ h (f y) (h y hy)

この一行の解説（対話の跡）:

fun y hy ↦ _ と書いて、Expected type: P (f (f y)) を見る。
手元の h は「ある値 x とその証明 P x」を渡すと P (f x) をくれる関数。
P (f (f y)) を作るには、h の x 部分に f y を入れれば良さそうだ。
h (f y) _ と書くと、次の穴は Expected: P (f y) になる。
P (f y) は、再び h に y と hy を渡せば手に入る。
完成！

💡 一階述語論理版：磨き上げのチェックリスト

Exists.intro を ⟨ ⟩ に置き換えたか？
多重の ∃ は ⟨x, y, ...⟩ とまとめたか？
h x の結果に対して直接 .left や .right を繋げたか？
不要な show や have を削って一行（One-liner）にできないか検討したか？

1. 「等号の流し込み」： `▸` 記法（Substitution Macro）

等号の置換則 Eq.subst や Eq.ndrec を直接書くのは非常に苦痛です。そこで熟練者は ▸ ( \t または \triangle で入力) というマクロを愛用します。

使い方: h_eq ▸ h_proof
意味: 「証明 h_proof の中に現れる等式の左辺を、等号 h_eq を使って右辺に書き換えろ」

example (x y : U) (h : x = y) (px : P x) : P y :=
  h ▸ px  -- subst を使うより圧倒的に短く、かつ「x を y に変えた」という意図が明確

2. 存在記号の「パターンマッチ」分解

存在記号 h : ∃ x, P x から値と証明を取り出す際、Exists.elim は関数を入れ子にするためインデントが深くなりがちです。これを match や let ⟨ ⟩ で「構造分解」するのが Mathlib スタイルです。

テクニック: ゴールを作る直前で分解する。

example (h : ∃ x, A x ∧ B x) : ∃ x, A x :=
  let ⟨x, ha, _⟩ := h  -- 一気に x と A x (ha) を取り出す
  ⟨x, ha⟩              -- 新たなペアを作る

熟練者の視点: let ⟨ ⟩ を使うと、Infoview の Context に x と ha が直接現れるため、_ を使ったデバッグが非常にやりやすくなります。

3. 全称量化子の「部分適用」

全称記号 h : ∀ x y, R x y があるとき、すべての引数を一度に渡す必要はありません。

テクニック: 「だけ固定した命題」を新しい関数として扱う。

variable (h : ∀ x y, x = y → P x y)
#check h a      -- 型は ∀ y, a = y → P a y
#check h a b    -- 型は a = b → P a b

このように、h a と書くだけで「をに具体化した新しい定理」が手に入ります。これを別の関数の引数に放り込むのが項モードの醍醐味です。

4. `fun` と `forall` の同一視（Definitional Equality）

Lean において、∀ x, P x という型を持つデータの正体は「関数」です。したがって、「関数を作る fun」と「全称記号」は、Lean 内部では同じものとして扱われます。

熟練者の技: ゴールがでなくても、中身が関数的な構造（ならばなど）であれば fun を使って一気に引数を導入します。

5. 高階関数としての定理： `.` によるチェイン

一階述語論理の定理自体が「関数」であることを利用して、ドット記法を数珠つなぎにします。

具体例: h : ∀ x, A x ∧ B x から B a を導く

example (h : ∀ x, A x ∧ B x) (a : U) : B a :=
  (h a).right

h a で A a ∧ B a という「データ」を作る。
そのデータに対して .right メソッドを呼び出す。

これにより、一時的な have や let を一切使わずに、左から右へ流れるような証明（One-liner）が書けます。

💡 一階述語論理：項モードの「極意」まとめ

一階述語論理の項モードを極めるということは、「論理式を、型を持つデータ構造として扱う」 ということです。

h ▸ px：等号は「型を変換する魔法の杖」として使う。
let ⟨x, hx⟩ := ...：存在記号は「中身が詰まったカプセル」として開ける。
(h x).left：全称記号は「値を引数に取るメソッド」として連鎖させる。

これらを組み合わせると、9.7.7 のような複雑な問題も、驚くほどスッキリとした一行のコードになります。

-- 9.7.7 の一部
-- (∃ x, A x ∧ B x) → (∀ x, B x → C x) → ∃ x, A x ∧ C x
fun h1 h2 ↦
  let ⟨x, ha, hb⟩ := h1
  ⟨x, ha, h2 x hb⟩

🛠️ 項モード：最後の仕上げテクニック

1. `absurd` による矛盾の提示

「とが揃ったから矛盾だ」と言いたいとき、False.elim よりも直感的な関数があります。

使い方: absurd h_p h_np
意味: 証拠 h_p とその否定 h_np を渡すと、任意のゴールを導けます。

example (hp : P) (hnp : ¬P) : Q := absurd hp hnp

2. インラインでの型指定 (`(term : type)`)

Leanの推論が複雑すぎて迷子になったとき、または可読性を上げたいとき、項の途中で型を明示できます。

使い方: f (hx : P x)
メリット: _ でデバッグする際に、Leanに対して「ここはであるべきだ」とヒントを与えることで、エラー箇所を特定しやすくなります。

3. `match` による条件分岐の項表現

存在記号だけでなく、「または ()」の除去も match で書けます。これは Or.elim よりも Mathlib で好まれる傾向にあります。

example (h : A ∨ B) : C :=
  match h with
  | .inl ha => _ -- Aの場合の項
  | .inr hb => _ -- Bの場合の項

4. `Section` と `Variable` によるコンテキスト管理

項モードを短く保つためには、証明そのものよりも「外側」の整理が重要です。共通の仮定を variable に括り出すことで、関数の引数を極限まで減らします。

🗺️ 項モード・テクニック全地図（総まとめ）

カテゴリ	必須テクニック	熟練者の道具
全称 () / ならば ()	`fun x ↦ ...`, `h x`	`(h x).1`, `f ‹P›`
存在 () / かつ ()	`⟨x, hx⟩`	`let ⟨x, hx⟩ := ...`
または ()	`.inl`, `.inr`	`match h with
等号 ()	`rfl`	`h ▸ proof`
否定 () / 偽 ()	`fun h ↦ ...`	`absurd h1 h2`, `h.elim`
デバッグ・効率化	`_` (ホール), `exact?`	`@` (暗黙引数露出), `show_term`

1. 項モードでの `rfl` パターン

項モードでは、match 文のパターンとして rfl を記述します。

-- 項モードでの rfl パターンの例
example (x y : U) (h : x = y) (ha : A x) : A y :=
  match h with
  | rfl => ha -- ここで x = y が代入され、ha : A x が A y の証明として通用するようになる

この match h with | rfl => ... という書き方は、タクティクモードの rintro rfl と全く同じ論理的・内部的な動作をしています。

2. 「関数のパターンマッチ」でも使える！

先ほど練習した「fun を使わない書き方」でも、rfl パターンは非常に強力です。

-- 最も Mathlib らしい項モードの書き方
example : ∀ (x y : U), x = y → A x → A y
  | x, _, rfl, ha => ha

ここでの動き：

引数として x, y, x = y の証明, A x の証明を受け取ります。
3番目の引数に rfl パターンを指定します。
その瞬間、Lean は内部で **y を x に書き換え（代入）**します。
すると、最後の引数 ha の型が A x から A y（つまりゴールそのもの）に一致し、そのまま返せるようになります。

3. タクティクモード vs 項モード

どちらのモードでも、rfl パターンが担っている役割は 「等式のコンストラクタ Eq.refl に対するパターンマッチ」 です。

場所	書き方
タクティクモード	`rintro rfl` / `rcases h with rfl` / `obtain rfl := h`
項モード	`match h with
関数パターンマッチ	`

4. 練習問題：等号の「合同性」を項モードで

この rfl パターンの威力を実感するために、次の問題を**項モードのパターンマッチ（| ... => ...）**で書いてみてください。

問題： x = y → y = z → x = z （推移律）

example {x y z : U} : x = y → y = z → x = z
  | rfl, rfl => rfl

↑ これがなぜ動くのか、今のあなたなら説明できるはずです！

1つ目の rfl で y が x になり、
2つ目の rfl で z が x になり、
ゴールが x = x になったので、右側の rfl で解決。

一階述語論理の項モード技法

1. デバッグ：一階述語論理特有の対話テクニック

① Placeholder (_) と「値」の推論

② インライン by apply? の強力さ