タクティク・モード構築テクニック

1. 構築の設計：Backward Reasoning（逆算思考）

熟練者は、まず「ゴールをバラバラにして、何を示せばいいのかを単純化する」ことから始めます。

example (P Q R : Prop) : (P → R) ∧ (Q → R) → (P ∨ Q → R) := by
  -- ① ゴールの → を見て intro で仮定に放り込む
  intro h hPQ
  -- ② ゴール R を見て、どうやって作るか逆算する
  -- ここで手元の h : (P → R) ∧ (Q → R) を分解
  cases h with
  | intro hPR hQR =>
      -- ③ ゴール R は hPR からも hQR からも作れそう。
      -- でも hPQ : P ∨ Q なので、hPQ の「場合分け」を先にすべきだと判断
      cases hPQ with
      | inl hP => _
      | inr hQ => _

ここでのテクニック：

• cases の活用: ∧ や ∨ を見たら即座に分解します。
• intro の一括処理: intro h の後に続けて hPQ と書くことで、ネストした → を一度に処理します。

---

2. デバッグ：Infoview の「時間旅行」

証明の途中で「今、どの仮定が使えるんだっけ？」と混乱したら、カーソルを上下に動かします。

• 具体例: cases hPQ の直後にカーソルを置く。
• Infoview の表示:

hPR : P → R
hQR : Q → R
hP : P
⊢ R

• デバッグのアクション: これを見て、「あ、hPR に hP を適用すれば R になるな！」と確信を得ます。もし仮定が足りなければ、上の行に戻って cases の仕方をやり直したりします。

---

3. 構築のテクニック：情報の整理と管理

サブゴールが増えてきたとき、熟練者はドット · や { } を使って「視界」をクリアにします。

      cases hPQ with
      | inl hP =>
          -- ここで · を打つ
          · apply hPR
            exact hP
      | inr hQ =>
          · apply hQR
            exact hQ

ここでのテクニック：

• · (フォーカス): これを打った瞬間、Infoview から「もう一方のサブゴール（hQ のケース）」が消え、今取り組んでいるケースだけが表示されます。これにより、思考のノイズが劇的に減ります。
• apply による逆算: exact hPR hP と一気に書く代わりに、apply hPR と打ってゴールを P に変えることで、一歩ずつ着実に進みます。

---

4. 自動化によるショートカット

証明が「ほぼ当たり前」の段階に来たら、一文字ずつ打つのをやめて自動化に任せます。

example (P Q R : Prop) : (P → R) ∧ (Q → R) → (P ∨ Q → R) := by
  intro ⟨hPR, hQR⟩ hPQ -- intro の段階で ⟨ ⟩ を使って ∧ を分解（熟練者技）
  cases hPQ with
  | inl hP => exact hPR hP
  | inr hQ => exact hQR hQ

さらに短くするテクニック：

• **aesop や tauto**: このレベルの命題論理なら、by tauto と打つだけで一撃で終了します。
• **デバッグとしての tauto**: 複雑な証明の途中で「ここから先は自明なはずだ」と思ったら tauto を打ち込みます。もしエラーが出れば、自分の論理構成に穴がある（仮定が足りない等）ことが分かります。

結論から言うと、「はい、教えてくれます」。しかも、それを教えてもらうことこそが、Lean上達の近道です。

自動化タクティクが「裏で何をやったか」を暴くための、具体的で実践的な方法を紹介します。

---

1. apply? や exact? の場合

これらは最初から「答え（項）」を提案してくれるツールなので、そのまま**「どう解いたか」**がコードの形で表示されます。

• 表示例: Try this: exact Not.elim h hPa
• 学び: これを見れば、「あ、Not.elim という定理に引数を2つ渡せばよかったんだな」と、項モードの具体的な書き方が一目で分かります。

---

2. show_term を使う（最強の学習ツール）

tauto や aesop、simp などの自動化タクティクが、最終的にどのような「項」を生成したのかをすべて出力させる魔法のコマンドです。

• 使い方: 自動化タクティクの前に show_term を置きます。

example (P : Prop) : P → ¬¬P := by
  show_term tauto

• 効果: Infoviewに Try this: exact fun h hp ↦ h hp のように、自動化が組み立てた**「純粋な証明の正体（項）」**が表示されます。
• メリット: 「魔法」が「具体的な論理の積み重ね」に変わる瞬間が見えるため、非常に勉強になります。

---

3. simp の中身を見る (simp?)

simp は裏で大量の定理を使って式を書き換えます。何を使ったか知りたい時は ? を付けます。

• 使い方: simp?
• 効果: Try this: simp only [add_comm, mul_one] のように、**「どの定理を組み合わせて解決したか」**をリストアップしてくれます。
• 学び: これにより、Mathlibに存在する便利な定理（add_comm など）の名前を自然に覚えることができます。

---

4. aesop? で探索過程を見る

最新の強力な自動探索タクティク aesop も、? を付けることでその思考プロセスを教えてくれます。

• 効果: どの仮定を分解し、どの定理を適用してゴールに辿り着いたのか、ステップバイステップのタクティク構成を提案してくれます。

---

なぜ「中身を見る」ことが重要か

学び始めの段階で自動化を使い、その中身を教えてもらうルーチンを繰り返すと、以下のようなサイクルが生まれます。

1. 自力で挑戦: 構造を考える。
2. 自動化に頼る: とりあえず解かせてみる。
3. 逆引き学習: show_term や ? で答えのコードを見て、「なぜこれで解けるのか？」を自分の手でトレースする。
4. 清書: 自動化を消して、教えてもらった綺麗な項やタクティクで書き直す。

---

5. constructor と repeat の一括処理

ゴールが「かつ（）」や「同値（）」で繋がっており、それぞれの証明が似たような手順で解ける場合に非常に有効です。

• 具体例: A ∧ B ∧ C → B ∧ A

example (A B C : Prop) : A ∧ B ∧ C → B ∧ A := by
  intro h
  constructor -- ゴールを B と A に分ける
  · exact h.right.left -- B を証明
  · exact h.left       -- A を証明

-- 熟練者の効率化（repeat を使用）
example (A B C : Prop) : A ∧ B ∧ C → B ∧ A := by
  intro h
  repeat constructor -- 分解できるだけ分解する
  · exact h.right.left
  · exact h.left

テクニック: repeat constructor と書くことで、複雑に入れ子になった構造を一度にフラットなサブゴールへ分解できます。

---

6. have による「論理の足場固め」

逆算（Backward Reasoning）だけでは、前提条件が複雑になった時に頭がパンクしてしまいます。そこで、**「今分かっていることから、中間結果を固定する」**前向きな推論（Forward Reasoning）を織り交ぜます。

• 具体例: 非常に長い前提から何かを導く時

example (h : 非常に複雑な前提) : ゴール := by
  have h_mid : P := by
    -- P を導くためだけの小さな証明
    ...
  -- これ以降、h_mid : P を「既知の事実」として使える
  apply some_lemma h_mid

デバッグのコツ: have を使うことで、長い証明の中に「チェックポイント」を作ることができます。もし h_mid が証明できなければ、そこまでの論理にミスがあることが即座にわかります。

---

7. rw (rewrite) と nth_rewrite による等式操作

等式（=）や同値（↔）を使って、ゴールや仮定の「見た目」を書き換える強力なテクニックです。

• 具体例: x + y = y + x という知識を使って書き換える

example (x y : Nat) : (x + y) * 0 = 0 := by
  rw [add_comm]   -- ゴールが (y + x) * 0 = 0 に変わる
  rw [mul_zero]   -- ゴールが 0 = 0 になり、自動で解決

デバッグテクニック: rw は**「どこが書き換わるか」**をInfoviewで一行ずつ追うのが基本です。もし意図しない場所が書き換わったら、nth_rewrite 2 [add_comm]（2番目の箇所だけ書き換えろ）のように指定して制御します。

---

8. 構造的なデバッグ：all_goals と any_goals

複数の分岐（cases など）が発生した際、すべての分岐に対して一気にデバッグや修正を行う方法です。

• 具体例:

example : ... := by
  cases h
  all_goals
    simp -- すべてのサブゴールに対してとりあえず単純化を試みる
    try exact assumption -- 解けるものがあれば解いてしまう

設計のコツ: これにより、残った「本当に難しいケース」だけに集中できるようになります。

---

タクティク・モード構築の「黄金のルーチン」完全版

1. Decompose: intro, cases, constructor で問題を最小単位にする。
2. Focus: · や { } でサブゴールを一つずつ隔離する。
3. Synthesize: have で中間結果を作り、武器を増やす。
4. Rewrite: rw でゴールを「すでに知っている形」に変形する。
5. Automate: 詰めの段階で exact? や aesop に解決を任せる。
6. Refactor: 動くようになったら、タクティクを整理して読みやすく清書する。

---