一階述語論理のタクティク・モード技法

1. 構築の設計：Forward & Backward の融合

熟練者は、ゴールから逆算する（Backward）だけでなく、specialize を使って手持ちの「強力な全称命題」を「使いやすい具体的な事実」へと前向き（Forward）に作り変えます。

example (h : ∀ x y, P x → Q y → R x y) (ha : P a) (hb : Q b) : R a b := by
  -- ① specialize で全称仮定を「今必要な形」に具体化する
  specialize h a b  -- h が (P a → Q b → R a b) に書き換わる
  -- ② あとは命題論理と同じ。ならば(→)の除去
  apply h
  · exact ha
  · exact hb

ここでのテクニック：

• specialize: 複雑な ∀ を、今目の前にある具体的な値（a や b）に固定することで、Infoview をスッキリさせ、思考の迷いを防ぎます。

---

2. デバッグ：メタ変数（?m.1）との対話

一階述語論理で最も多い「詰まり」は、apply した瞬間にゴールが ⊢ P ?m.1（何かよくわからない値について を示せ）となる現象です。

• 原因: ゴールを示すために「ある値」が必要だが、Lean がまだその値を特定できていない状態。
• デバッグのアクション:

1. 値を教える: apply h (x := a) のように引数を明示して apply する。
2. 順序を変える: use a を先に打って、値を確定させてから apply する。
3. 放置して進める: 他の仮定を exact していくうちに、Lean が「あ、この ?m.1 は a のことだったんだな」と自動で解決してくれるのを待つ。

---

3. 構築のテクニック：obtain と rintro の深掘り

Mathlib 流の最も強力な効率化は、導入と分解の**「一括処理」**です。

-- ❌ 初心者：バラバラに打つ
intro h
rcases h with ⟨x, hx⟩
rcases hx with ⟨ha, hb⟩

-- ✅ 熟練者：rintro で一撃
rintro ⟨x, ha, hb⟩

ここでのテクニック：

• Nested Patterns: ⟨x, ha, hb⟩ のように書くことで、存在記号の「値」と「複数の性質」を一度にコンテキストに展開します。
• obtain: 証明の途中で「～であるような が存在するはずだ」という中間ステップを作るとき、have よりも obtain を使うほうが、存在記号の構造を即座に分解できるため効率的です。

---

4. 自動化によるショートカット：aesop と positivity

一階述語論理特有の「値の範囲」や「論理構造」を自動で見抜かせるテクニックです。

• aesop: 量化子が絡むパズル（ の適用順序など）を自動で探索してくれます。
• positivity: 数値の範囲（ など）が絡む一階述語論理において、自明な不等式を解決します。
• show_term の再利用: show_term { aesop } とすることで、複雑な量化子の受け渡しを項モードでどう書くべきか、Lean から「模範解答」を奪い取ることができます。

---

5. 等号のデバッグ：nth_rewrite と conv

ゴールの中に同じ値（例：）が複数ある時、特定の だけを書き換えたい場合があります。

• nth_rewrite: 「2番目の だけ書き換えろ」という精密な操作。
• conv モード: ゴールの中を探索し、ピンポイントでその場所（サブターム）だけにタクティクを適用する「手術モード」です。

example (x : ℕ) : x + x = x + x := by
  conv =>
    lhs      -- 左辺 (Left Hand Side) に集中
    arg 2    -- 2番目の引数（2つ目の x）へ移動
    -- ここで何か書き換えができる

---

ありがとうございます。それでは、一階述語論理の証明を「Mathlibスタイル」の高みへと引き上げる、高度な磨き上げ（Polish）と効率化のテクニックを解説します。

---

1. 「値」の構築と「証明」の分離

熟練者は、存在記号の証明において「何を使うか」を先に宣言し、その後に「なぜそれが正しいか」を記述します。

• use の拡張: 複数の値を一度に指定できます。
• **構造化された use**: exact ⟨t, ht⟩ を使うことで、use と exact の往復を減らします。

-- ✅ Mathlib流：一気に値を提示し、証明のサブゴールを作る
example : ∃ x y, x + y = 5 := by
  refine ⟨2, 3, ?_⟩ -- 値を先に埋め、証明を「?_（プレースホルダ）」で後回しにする
  rfl

---

2. 定理の「逆算適用」：apply の精密制御

一階述語論理では、apply する定理が「どの変数に対してのものか」を明示することで、Leanの迷いを断ち切ります。

• apply ... (x := t): 特定の変数に値を指定して適用。
• apply ... using t: 証拠品 t を使いながら定理を適用。

-- ゴールが P b のとき、h : ∀ x, x = a → P x を使いたい
apply h (x := b)
-- これにより、ゴールが直ちに b = a になり、推論が安定します。

---

3. 仮定の「インライン分解」：obtain の真価

obtain は存在記号だけでなく、等号を含む複雑な構造をその場で解体するのに最適です。

• テクニック: 等号の書き換えと分解を一行で行う。

-- h : ∃ x, f x = y ∧ P x
obtain ⟨x, rfl, hpx⟩ := h
-- 「f x = y」が「rfl」というパターンでマッチされることで、
-- コンテキスト内の y がすべて f x に自動的に書き換わります（subst効果）。

---

4. calc ブロックのタクティク内統合

一階述語論理の多くは「変形」です。タクティクの途中で calc を使うことで、論理の透明性が劇的に向上します。

example (x y : ℤ) : (x + y)^2 = x^2 + 2*x*y + y^2 := by
  calc
    (x + y)^2 = (x + y)*(x + y) := by rw [pow_two]
    _         = x^2 + 2*x*y + y^2 := by ring -- 数値計算用タクティク

Mathlibスタイルのコツ: calc の各行の右側に by ... を添えることで、どのステップでどの性質（全称命題など）を使ったかを明示します。

---

5. 高度な一括処理：congr と convert

「ほぼ同じ形をしているが、一箇所だけ違う」というゴールを扱う、熟練者の「横着」テクニックです。

• congr: ゴール を に分解します。
• convert h: 手持ちの仮定 h がゴールと「微妙に違う」時、その差分だけを新しいサブゴールとして抽出します。

-- ゴール：⊢ P (x + 0)
-- 手持ち：h : P x
convert h
-- ゴールが ⊢ x + 0 = x に変わる（あとは加法の定義で解決）

---

💡 Mathlib スタイル：一階述語論理の「美学」まとめ

1. 名前付けを最小限に: rcases や rintro で無名引数 ⟨...⟩ を使い、h1, h2, h3 といった無意味な名前の羅列を避ける。
2. 前向き推論を混ぜる: specialize や have を使い、複雑な ∀ を「今すぐ使える武器」に加工してから戦う。
3. 等号は subst や rfl パターンで消す: 変数は少ないほうが Infoview が読みやすくなります。
4. simp の「香り」を隠さない: simp? で得られた定理リストを simp only [...] として清書し、将来の Mathlib 更新で証明が壊れないようにする。

---

🏆 最終デバッグ・チェックリスト

• intro と cases が連続していないか？（rintro や rcases にまとめられる）
• ∃ の証明で、use の後に rfl や exact が続くなら、exact ⟨t, ht⟩ と書けないか？
• rw が 5回以上続いていないか？（calc や simp で整理できないか）
• コンテキストに「使っていない変数」が残っていないか？（subst で消去する）

---

🛠️ 最後の隠し武器：超・熟練者のテクニック

1. set タクティク（略記の導入）

一階述語論理で、 のような長い式が何度も出てくる場合、一時的に「 と置く」ことができます。

• 効果: set t := f (g (x + y)) with h_def と書くと、式が t に置き換わり、書き換え用の等式 h_def も手に入ります。

2. unfold と定義の展開

定理名ではなく、**「定義そのもの」**に立ち返って証明したい時に使います。

• 例: Prime p（ は素数）という定義を、「 かつ……」という具体的な数式に展開します。

3. exact の「チェイン」

タクティク・モードの中で、最後の一撃に非常に長い「項」を直接叩き込む技です。

• 例: exact ⟨x, ha, h2 x hb⟩ タクティクで一歩ずつ進むより、最後は項モードの「一括構築」で締めるほうが Mathlib では美しいとされます。

4. メタプログラミング・マクロ

tactic1 <|> tactic2 （1がダメなら2を試せ）や、try tactic（失敗してもエラーにせず進め）などの制御構文です。

---

🗺️ 全テクニックのロードマップ（まとめ）

あなたがこれまで学んできたことは、以下の3つの階層に整理されます。

階層	習得した武器	目的
基礎 (Base)	導入則・除去則、intro, cases, exact	論理を正しく進める
応用 (Advanced)	rcases, rintro, ▸, exact?, specialize	効率的・直感的に進める
洗練 (Polish)	obtain, calc, refine, show_term	Mathlib流の美しさを実現する

---

1. 仕組みを解剖する

通常のパターンマッチと rfl パターンの違いを比較してみましょう。

🔹 普通の分解（rcases など）

-- h : x = y という仮定があるとき
rcases h with h_eq
-- コンテキストに「h_eq : x = y」という名前の証拠が残るだけ。
-- x と y はまだ別々の名前として存在し続ける。

🔸 rfl パターン（rintro rfl や match ... with | rfl）

-- h : x = y という仮定があるとき
rintro rfl
-- 1. Leanは「x と y は同じだ」と認識する。
-- 2. コンテキストとゴール内の「y」をすべて「x」に書き換える（代入）。
-- 3. 「x = y」という仮定自体は、もう用済みなので消える。

---

2. なぜ rfl という名前なのか？

これは等号の定義に関係しています。Lean において、等号 a = b の唯一の証明（コンストラクタ）は Eq.refl a（反射律： は と等しい）です。

つまり、x = y という仮定に対して rfl でパターンマッチをするということは、Lean にこう伝えていることになります：

「この x = y という仮定が、唯一のコンストラクタ rfl（反射律）でできているケースだけを考えてくれ！」

すると Lean は、**「それが rfl であるためには、そもそも x と y が同じモノでなければならない」**と逆算し、環境全体を書き換えてくれるのです。

---

3. Mathlib での活用例

Mathlib スタイルでは、obtain と組み合わせて、存在記号から値を取り出しつつ等式を消去する際によく使われます。

-- 「ある x があって、それが a と等しく、かつ P x を満たす」
-- ∃ x, x = a ∧ P x
obtain ⟨x, rfl, hPx⟩ := h
-- この一行で：
-- 1. x を取り出す
-- 2. x = a なので、x を a に書き換える（x は消えて a になる）
-- 3. hPx は「P a」の証明として手元に残る

---

4. まとめ

特徴	普通のパターンマッチ	rfl パターン
対象	∧, ∨, ∃ など	x = y (等式)
動作	構造を分解する	変数を一方に統一（代入）する
結果	仮定の名前が増える	仮定が消え、式がスッキリする

🚀 試してみよう！

この「代入の魔法」を実感するために、以下のコードを Lean に貼り付けて Infoview を眺めてみてください。

example (P : U → Prop) (x y : U) (h_eq : x = y) (h_px : P x) : P y := by
  -- ここで rfl パターンを使う
  rintro rfl
  -- Infoview を見ると、h_px が P y の証明に化けているはずです！
  exact h_px