命題論理の項モード対応表

🛠️ 命題論理の項モード対応表：データ構築ガイド

論理記号	導入則 (データを作る)	除去則 (データを使う)
ならば ()	fun h ↦ ...	f h (関数に引数を渡す)
かつ ()	⟨h1, h2⟩	h.left, h.right, h.1, h.2
または ()	.inl h, .inr h	h.elim (fun h1 ↦ ...) (fun h2 ↦ ...)
同値 ()	⟨h_mp, h_mpr⟩	h.mp, h.mpr
否定 ()	fun h ↦ ...	h h_val (矛盾 False を導く)
偽 ()	(なし)	h.elim (爆発原理)

---

1. なれば () と 否定 ()

項モードでは、これらはすべて 「関数」 です。

• 導入 (fun): 「 という材料を渡されたら、どうやって を作るか」というレシピを書きます。
• 除去 (適用): 手持ちの関数（レシピ）に、必要な材料を放り込みます。

-- 導入
def my_proof : A → B := fun ha ↦ _

-- 除去
example (f : A → B) (ha : A) : B := f ha

---

2. かつ () と 同値 ()

項モードでは、これらは 「セット（構造体）」 です。

• 導入 (⟨ ⟩): 必要な証拠をすべて山括弧に詰め込みます。
• 除去 (.): ドット記法を使って、セットの中から必要な証拠を取り出します。

-- 導入
example (ha : A) (hb : B) : A ∧ B := ⟨ha, hb⟩

-- Mathlib流
example (h : A ∧ B) : B ∧ A := ⟨h.2, h.1⟩

-- 除去
example (h : A ∧ B) : A := h.left

---

3. または ()

項モードでは、これらは 「タグ付きの箱」 です。

• 導入 (.inl / .inr): 左の証拠を入れた箱か、右の証拠を入れた箱かを作ります。
• 除去 (.elim): 「もし左の箱だったらこうする」「もし右の箱だったらこうする」という2つの処理関数を渡します。

-- 導入
example (ha : A) : A ∨ B := .inl ha

-- 除去
example (h : A ∨ B) : C :=
  h.elim
    (fun ha ↦ _) -- 左側の場合のレシピ
    (fun hb ↦ _) -- 右側の場合のレシピ

-- パターンマッチ（match文）を使うスタイル
-- (複雑な場合分けではこちらの方が Mathlib では一般的)
example (h : A ∨ B) : C :=
  match h with
  | .inl ha => _
  | .inr hb => _

---

4. 古典論理 (Classical Term mode)

項モードで古典論理（排中律や背理法）を使うには、数学的な「魔法の定数」を呼び出す感覚で記述します。

• 排中律 (Classical.em): 書くだけで A ∨ ¬A という証拠が手に入ります。
• 背理法 (by_contra): 「もし ならば矛盾」という関数を引数に取る関数です。

open Classical

-- 排中律の使用例: ピアースの律
example (P Q : Prop) : ((P → Q) → P) → P :=
  fun h ↦
    (Classical.em P).elim
      (fun hp ↦ hp) -- P が真ならそれを出して終了
      (fun hnp ↦ h (fun hp ↦ (hnp hp).elim)) -- P が偽なら矛盾から Q を作る

-- 背理法の使用例:
example (A : Prop) : A :=
  by_contra (fun hna : ¬A ↦ _ ) -- この穴で False を作れば A が手に入る

---

5. 項モードの設計・デバッグ手法：Skeleton-First（骨組みから書く）

熟練者がいきなり完成した項を書けるのは、頭の中でこのステップを踏んでいるからです。

① トップダウン分解 (Skeletoning)

ゴールの「型」を見て、一番外側の「導入則」をまず書きます。中身はすべて _ (ホール) にします。

• ゴールが なら：fun ha ↦ _
• ゴールが なら：⟨ _ , _ ⟩
• ゴールが なら：⟨ fun h ↦ _ , fun h ↦ _ ⟩

② _ (ホール) との対話

_ にカーソルを置くと、Infoview に Expected type（今作るべき型） と Context（今使える武器） が表示されます。

example (h : A ∧ B) : B ∧ A :=
  ⟨ _ , _ ⟩  -- 1つ目の「_」にカーソルを置くと「Expected type: B」と出る

③ ドット記法による探索

仮定 h の後に . を入力して、その型で可能な「除去則」を一覧表示させます。

• h. と打つと、補完リストに left, right, elim などが出るのを見て、次の一手を決めます。

---

6. 効率化：タクティクとのハイブリッド利用

「純粋な項モード」にこだわりすぎず、構築中だけタクティクの力を借ります。

• **インライン by**: 項の途中で一時的にタクティクモードに切り替えます。

⟨ h.right, (by apply? ) ⟩

• exact? をヒントにする: exact? は、まさに「その穴を埋めるための項」そのものを提案してくれるため、項モードの書き方を学ぶのに最適です。

---

💡 項モードのデバッグ・サイクルまとめ

1. Skeleton: ゴールの導入則を _ 付きで書く。
2. Inspect: _ で要求されている型と、使える引数を Infoview で見る。
3. Refine: 引数を適用（除去則）して穴を埋める。
4. Polish: ドット記法や引数の統合（fun ha hb ↦ ...）で、コードを短く美しくする。

---