tactic と証明項の対応

tactic は証明を魔法のように作っているわけではありません． 各 tactic は，現在のゴールに対して，最終的には Lean のカーネルが検査できる証明項を構成します． Infoview ではゴールが変形されて見えますが，背後では「どのコンストラクタ，どの関数，どの定理を使って項を作るか」を指定していると考えるとよいです．

Chapter 02 で見た型の構成と対応させると，基本 tactic は次のように整理できます．

ゴールまたは仮定の形	主な tactic	対応する項・定義
P → Q，∀ x, P x を示す	intro	関数 fun h => ...，依存関数
P → Q，∀ x, P x を使う	apply，関数適用	証明を関数として適用する
P ∧ Q を示す	constructor，exact ⟨_, _⟩	And.intro
P ∧ Q を使う	cases，rcases，obtain	And.left，And.right，パターン分解
P ↔ Q を示す	constructor	Iff.intro
P ↔ Q を使う	rw，.mp，.mpr	両方向の含意を field として使う
P ∨ Q を示す	left，right	Or.inl，Or.inr
P ∨ Q を使う	match，cases，rcases	Or のコンストラクタによる場合分け
∃ x, P x を示す	use，exact ⟨x, hx⟩	Exists.intro
False から任意の命題を示す	exfalso，contradiction	False.elim
a = b を示す	rfl，既存補題	Eq.refl や Eq 型の証明
a = b を使う	rw，subst	等式による置換
inductive 型を使う	match，cases，induction	コンストラクタによる場合分け・帰納法
structure の等式を示す	ext	field ごとの等式

この対応を意識すると，tactic が失敗したときにも「いま必要なのは関数を作ることか，コンストラクタを使うことか，既存の等式で書き換えることか」を切り分けやすくなります． 以降の節では，この表の各行を具体例として見ていきます．