項モード構築テクニック

1. デバッグ：Infoview との対話テクニック

項モードのデバッグの基本は、**「Leanにわざと分からないフリをして、ヒントを喋らせる」**ことです。

① Placeholder (_) の型確認

「次の一手が分からない」時や「今、何が使えるか忘れた」時に使います。

• 具体例: の証明中

example (P Q : Prop) : P ∧ Q → Q ∧ P :=
  fun h ↦ _  -- ここで手を止めて「_」の上にカーソルを置く

• 見えるもの (Infoview):

h : P ∧ Q
⊢ Q ∧ P

これを見て、「あぁ、手元には h があって、作りたいのは Q ∧ P なんだな。じゃあ次は ⟨ ⟩ を書こう」と判断します。

② ドット記法 (.) による探索

「この仮定から何が取り出せるか」を確認する、いわゆる「メソッド探索」です。

• 具体例:

example (h : P ∧ (Q ∨ R)) : Q ∨ R :=
  h. -- ここで「.」を打つと補完リストが出る

• 補完リストの表示:

• left : を取り出す

• right : を取り出す

• アクション: リストから right を選べば h.right で証明が完成することが分かります。

③ 中間変数の導入 (let)

式が長くなりすぎて「今、どのパーツがどの型なのか」混乱した時に、一時的に名前を付けます。

• 具体例: 複雑な合成関数の証明など

example (h : P → Q) (g : Q → R) (hp : P) : R :=
  let hq := h hp  -- ここで一旦 Q を作り、hq という名前を付ける
  g hq            -- hq が Q 型であることを確信して次に進める

hq の上にカーソルを置けば、Leanが hq : Q と教えてくれるので、暗算で型を追う必要がなくなります。

---

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

「項モードで書きたいけれど、具体的な定理名や書き方が分からない」という時の裏技です。

① インライン by と apply?

タクティク・モードの強力な検索機能を、項モードの中に「埋め込み」ます。

• 具体例: 二重否定の除去など

open Classical
example (h : ¬¬P) : P :=
  (by apply?) -- カッコで囲って一時的にタクティクモードにする

• Leanの提案: exact not_not.mp h
• 清書: 提案された not_not.mp h をコピーして、(by apply?) の代わりに書き込めば、純粋な項モードの完成です。

② exact? をヒントにする

apply? は「この定理を使いなさい」と言いますが、exact? は「この項を書きなさい」と教えてくれます。

• 具体例:

example (P : Prop) : P → P := by
  exact? -- 「exact fun a => a」と提案される

これを見れば、「あ、項モードでは fun a ↦ a と書けばいいんだな」と、項モードの書き方そのものを学習できます。

---

ありがとうございます！それでは、中級者から熟練者へのステップアップに欠かせない**「4. 磨き上げ（Mathlibスタイルへの変換）」**のテクニックを具体的に解説します。

これらは、コードを単に「短くする」だけでなく、**「論理の意図を明確にする」**ための設計思想でもあります。

---

3. 磨き上げ：Mathlibスタイルへの変換

① 引数の統合（Curryingの活用）

複数の fun を重ねるのではなく、一行にまとめます。

• Before (初心者風):

fun hp ↦ fun hq ↦ fun hr ↦ ⟨hp, ⟨hq, hr⟩⟩

• After (熟練者風):

fun hp hq hr ↦ ⟨hp, hq, hr⟩

テクニック: Leanでは ⟨a, ⟨b, c⟩⟩ を ⟨a, b, c⟩ とフラットに書けます。引数も同様に並べて受け取ることで、コードの横幅を抑え、可読性を高めます。

---

② 無名引数の活用（フランス引用符 ‹ ›）

「名前を付けるまでもないが、そこにある前提を使いたい」時に使います。

• 具体例: 「 と があれば 」という当たり前の証明

example (h : P) (f : P → Q) : Q :=
  f ‹P›  -- 「今使える仮定の中から、型が P のものを探して使え」という意味

• メリット: 複雑な証明で仮定に h1, h2, h3… と名前が増えすぎると、どれがどれか分からなくなります。‹P› と書けば、名前ではなく「型（意味）」で引数を参照できるため、デバッグが劇的に楽になります。

---

③ ドット記法の徹底と省略

名前空間を省略して、データそのものに語らせる書き方です。

• Before:

And.intro (And.right h) (And.left h)

• After:

⟨h.right, h.left⟩

• さらに高度な省略 (.): ゴールから型が推論できる場合、コンストラクタの名前をさらに削れます。

-- ゴールが A ∨ B のとき
.inl ha   -- Or.inl ha の略

設計のコツ: h.left のように書くと、「h という証拠の左側」という意図が明確になります。

---

④ 暗黙の引数の活用

型を明示せず、Leanの推論に任せることでノイズを減らします。

• 具体例: id 関数など

#check @id      -- @ をつけると隠された型引数 {α : Sort u} が見える
#check id hp    -- 普通は型を言わなくても hp の型から α を推論してくれる

デバッグテクニック: 逆に、推論がうまくいかずにエラーが出る時は、@ をつけてすべての引数を書き出すことで、「どこで型が食い違っているか」を特定できます。

---

💡 項モード構築の「黄金のルーチン」まとめ

最後に、これまでお伝えした全テクニックを統合したワークフローです。

1. Skeleton: fun hp hq ↦ ⟨_, _⟩ と枠だけ書く。
2. Inspect: _ にマウスを乗せ、Infoviewで「求められている型」を確認する。
3. Search: 分からない部品は (by apply?) で探し、提案された項をコピペする。
4. Refine: h.left や f ‹P› を使って穴を埋める。
5. Polish: 引数をまとめ、名前空間（And. 等）を消して美しく仕上げる。

---