一階述語論理のタクティク・モード対応表

🛠️ 一階述語論理のタクティク・モード対応表（量化子編）

論理記号	導入則 (ゴールを分解する)	除去則 (仮定を活用する)
全称 ()	`intro x`	`apply h` または `specialize h t`
存在 ()	`use t` または `exists t`	`cases h with

1. 全称記号 ()：任意の値を固定し、関数として使う

全称記号はタクティク・モードでは「引数を待っている関数」として振る舞います。

導入 (intro x): ゴールのを取り除き、「任意のを固定する」操作です。
除去 (apply h): 「すべてのでが成り立つ」なら、ゴールをその特殊なケースに置き換えます。

-- 導入
example : ∀ x : ℕ, x = x := by
  intro x  -- 任意の自然数 x を固定。ゴールは ⊢ x = x
  rfl

-- 除去
example (h : ∀ x, P x → Q x) (ha : P a) : Q a := by
  apply h  -- ゴールを Q a から P a に変える（x に a を代入）
  exact ha

**💡 Mathlib流テクニック：specialize** 仮定 h : ∀ x, P x を、あらかじめ特定の a についての命題に書き換えておきたい時に便利です。 specialize h a と打つと、h の型が P a に変わります。

2. 存在記号 ()：証拠を提示し、中身を取り出す

存在記号は、もっともタクティクの恩恵を感じる部分です。

導入 (use t): ゴールのに対して、具体的な値を「これだ！」と提示します。
除去 (cases): 「何らかのが存在する」という仮定から、具体的な名前（）とその性質の証明（）を取り出します。

-- 導入 (use)
example : ∃ x : ℕ, x + 1 = 2 := by
  use 1    -- x に 1 を指定。ゴールは ⊢ 1 + 1 = 2
  rfl

-- 除去 (rcases / obtain)
example (h : ∃ x, P x ∧ Q x) : ∃ x, P x := by
  rcases h with ⟨y, hy_p, hy_q⟩ -- 証拠 y と、その性質 hy_p, hy_q を一気に取り出す
  use y
  exact hy_p

3. 量化子と否定の移動 (`push_neg`)

一階述語論理で最も厄介な「」のような形を、「」に一撃で変換します。

push_neg: ゴール内の否定を量化子の内側へ押し込みます。
push_neg at h: 仮定 h 内の否定を整理します。

example (h : ¬ ∀ x, P x) : ∃ x, ¬ P x := by
  push_neg at h -- h を ∃ x, ¬ P x に変換
  exact h

💡 一階述語論理のデバッグ：Infoview の見方

一階述語論理では、Infoview の 「コンテキスト（左側）」 に注目してください。

型（Type）と命題（Prop）の混在: x : U（値）と h : P x（証明）が並びます。apply を打つ前に、「その値を引数として渡せるか？」を常にチェックします。
メタ変数 ?m.1 の出現: use をせずに apply などを行うと、値が決まっていない穴 ?m.1 が出ることがあります。これは「後で値を決める必要がある」というサインです。

🛠️ 一階述語論理のタクティク・モード対応表（等号・計算編）

操作内容	タクティク	補足・Mathlib流
等号による書き換え	`rw [h]`	`rw [← h]` で逆向き、`rw [h1, h2]` で連続書き換え
計算の連鎖	`calc`	タクティク・モード内でもブロックとして使用可能
関数・述語の引数一致	`congr`	を証明するためにをゴールにする
等号の反射律	`rfl`	ゴールがの形なら一撃で終了
仮定による置換	`subst x`	仮定を使って、全てのをに置き換えて消去する

1. 等号の書き換え (`rw`) と代入 (`subst`)

一階述語論理では、「ある値を、等しい値に置き換える」操作が頻発します。

rw [h]: ゴールの中にあるをに書き換えます。
subst x: コンテキストにがある時、全ての場所でをに置き換え、変数自体を消去します。

example (x y : ℕ) (h1 : x = y) (h2 : y = 3) : x = 3 := by
  rw [h1] -- ゴールが ⊢ y = 3 に変わる
  exact h2

example (x : ℕ) (h : x = 3) : x + x = 6 := by
  subst x -- 全ての x が 3 になり、h も消える。ゴールは ⊢ 3 + 3 = 6
  rfl

2. 計算形式の証明 (`calc`)

タクティク・モードの中でも calc は使えます。複雑な数式変形を rw だけで追うと Infoview がぐちゃぐちゃになりがちですが、calc を使うと「人間にとって読みやすい」証明になります。

example (x y z : ℤ) : (x + y) + z = (x + z) + y := by
  calc
    (x + y) + z = x + (y + z) := by rw [add_assoc]
    _           = x + (z + y) := by rw [add_comm y z]
    _           = (x + z) + y := by rw [add_assoc]

💡 一階述語論理：タクティク・モードの「黄金の証明サイクル」

一階述語論理の証明をタクティクで進める時の、最も効率的な思考手順です。

① 「存在」をまずバラす（Elimination First）

仮定に ∃ があるなら、真っ先に obtain や rcases で分解します。

理由: 証拠品（値）が手元にないと、全称記号 ∀ に何を代入すべきか決まらないからです。

② 「全称」の導入と「存在」の提示（Intro & Use）

ゴールが ∀ なら intro。ゴールが ∃ なら use。

注意: use をするタイミングは、「これだ！」という値が手元の武器（仮定）から確信できた時です。

③ 等号による「橋渡し」（Rewrite & Subst）

取り出した値や仮定を rw や subst で結びつけます。

📝 実践例：9.7.7 のような問題をタクティクで解く

「あるがとを満たし、全てのはを導くなら、あるはとを満たす」

variable (U : Type) (A B C : U → Prop)

example (h1 : ∃ x, A x ∧ B x) (h2 : ∀ x, B x → C x) : ∃ x, A x ∧ C x := by
  -- 1. まず存在をバラす（証拠品 x と、性質 ha, hb を得る）
  obtain ⟨x, ha, hb⟩ := h1

  -- 2. ゴールの存在を示すために、見つけた x を使う
  use x

  -- 3. ゴール A x ∧ C x を分割する
  constructor
  · exact ha  -- A x は既に持っている
  · -- C x を証明するために、全称命題 h2 に x を適用する
    apply h2
    exact hb

🛠️ デバッグ：一階述語論理特有の「詰まりどころ」

apply が失敗する: apply h をした時、∀ の引数がうまく推論されないことがあります。その場合は apply h (x := a) のように引数を明示するか、先に specialize h a して仮定を固定してください。
use する値が見つからない: この場合は「まだ仮定の分解が足りない」か「古典論理（背理法）が必要」なサインです。
rw が「ここじゃない場所」を書き換える: rw [h] は最初に見つけた箇所を書き換えます。特定の場所だけ変えたいなら nth_rewrite 2 [h] のように回数を指定するか、rw [h] at h_target で場所を明示します。

🚀 最後に：Lean の「魔法の杖」

もし、一階述語論理のパズルが論理的に正しいはずなのに、タクティクが細かすぎて疲れてしまったら……

aesop: （Mathlibをインポートしていれば）一階述語論理の標準的な問題を自動で探索して解いてくれます。
tauto: 命題論理レベルで自明なものを解決します。

🛠️ Mathlib流：一階述語論理の書き換えガイド

1. 構造分解（Decomposition）の流儀

存在記号 () や「かつ」 () を分解する際、標準の cases はもう使いません。

推奨: rcases または obtain
理由: 入れ子の構造を一気に、かつ名前を指定して展開できるため。

-- ❌ 非推奨（インデントが深くなり、名前も自動生成されて読みにくい）
cases h
case intro x h' =>
  cases h' with | intro ha hb => ...

-- ✅ Mathlibスタイル（一行で意図が明確）
rcases h with ⟨x, ha, hb⟩

-- ✅ Mathlibスタイル（「何を得たか」を強調したい時）
obtain ⟨x, ha, hb⟩ := h

2. 導入（Introduction）の流儀

全称記号 () や「ならば」 () を導入する際、intro を何度も打つのは避け、rintro で一気に片付けます。

推奨: rintro
理由: 値の導入と、その性質の分解（パターンマッチ）を同時に行えるため。

-- ❌ 非推奨
intro x
intro h
cases h with | intro ha hb => ...

-- ✅ Mathlibスタイル
rintro x ⟨ha, hb⟩

3. 等号操作の流儀

Mathlibでは、自明な変形を1行ずつ rw するのを嫌います。

推奨: simp / aesop / calc / ▸
理由: 本質的な論理ステップに集中するため。

-- ✅ 項モードでの Mathlib スタイル ( ▸ を活用 )
example (h : x = y) (px : P x) : P y := h ▸ px

-- ✅ タクティクでの Mathlib スタイル ( 複数の書き換えをまとめる )
rw [h1, h2, ← h3]

💡 演習 9.7.5 を例にした「初心者 vs 熟練者」の比較

問題：ならばであることを示せ。

【初心者スタイル（教科書的）】

一歩ずつ確実に進みますが、コードが長く、途中の状態が分かりにくいです。

example (h : (∃ x, P x) → Q) : ∀ x, P x → Q := by
  intro x
  intro hpx
  apply h
  use x
  exact hpx

【Mathlibスタイル（熟練者）】

論理の「流れ」を重視し、タクティクの合体技や項モードを混ぜます。

example (h : (∃ x, P x) → Q) : ∀ x, P x → Q :=
  -- 項モードで書くのが最も Mathlib らしい (One-liner)
  fun x hpx ↦ h ⟨x, hpx⟩

-- タクティクで書く場合でも：
example (h : (∃ x, P x) → Q) : ∀ x, P x → Q := by
  rintro x hpx
  exact h ⟨x, hpx⟩

4. Mathlib スタイル 4つの鉄則（一階述語論理編）

アノニマス・コンストラクタ ⟨ ⟩ を愛用せよ: Exists.intro や And.intro と書かずに、常に ⟨ ⟩ を使います。
ドット記法をチェーンせよ: (h x).left のように、関数適用と分解を繋げて書きます。
項とタクティクを混ぜろ: 「値の提示」のような簡単な部分は、タクティクの途中で exact ⟨x, ha⟩ のように項として直接書きます。
simp に任せられるところは任せろ: 論理演算の整理（ド・モルガンなど）は push_neg や simp で一気に処理します。

🎁 ボーナス：Mathlib でよく使われる「等号の定理名」

Mathlibスタイルで書くには、頻出する定理名を知っておくと便利です。

ext: 集合や関数の外延性（「中身が等しければ全体も等しい」）を示す。
congrArg:
id_rhs: ゴールの右辺を定義通りに展開する。