関数合成の証明スタイル

1. 3つの書き方の比較

同じ「 から を導く証明」を例に、スタイルの違いを見てみましょう。

スタイル	書き方	思考の向き	特徴
適用的 (Standard)	h (f x) (h x h1)	内側から外へ	最も一般的。数学的な の形。
ポイントフリー (∘)	h (f x) ∘ h x	構造の結合	定理の合成。引数を書かず、性質を繋ぐ。
**パイプライン (	>)**	`h1	> h x

---

2. 関数合成 ∘ の深い意味：定理の「連結」

∘ は \comp または \circ で入力します。

f : A → B と g : B → C があるとき、(g ∘ f) は A → C という新しい関数を一つ作り出します。 証明の世界では、これは以下のことを意味します。

• 前提の橋渡し: と を繋いで、 という新しい定理を即席で作る。
• 「?」タクティクとの相性: apply? は、現在のゴール（結論）に合うように、手持ちの定理を ∘ で繋いで「一撃で解ける巨大な定理」を合成して提案することがよくあります。

---

3. なぜ | x => h (f x) ∘ h x でパイプラインが使いにくいのか

あなたが試したパターンマッチング形式（| x => ...）は、「この型を持つ関数そのものを定義する」という宣言です。

• 合成 ∘ が合う理由: 右辺が「関数」のままで良いため。

• h (f x) ∘ h x はそれ自体が P x → P (f (f x)) という「関数」です。

• パイプライン |> が浮く理由: パイプラインは「具体的な値」を「関数」に放り込む動作だから。

• h1 |> h x と書くには、まず h1 という具体的な証明（値）を導入（fun h1 ↦）しなければなりません。

---

4. 実戦での使い分けガイド

Lean 熟練者がどのように使い分けているかの指針です。

1. calc ブロックの中: 可読性が命なので、適用的スタイル h (f x) h2 が好まれます。
2. 短い補題（Lemma）の定義: 簡潔さを求めて ポイントフリースタイル h (f x) ∘ h x が使われます。
3. 項モードでの複雑な変形: 括弧が重なって「閉じ括弧 ))))」が大量発生するのを防ぐため、パイプラインスタイル h1 |> h x |> h (f x) で流れを整理します。

---

🛠️ 「釣り方」の総括

• apply? が ∘ を出してきたら： 「Lean は今、定理を合成してショートカットを作ったんだな」と解釈してください。
• 自分が fun や rintro で引数を手に入れたら： |> を使って、その引数を順に定理に通していくのがスムーズです。

---