関数・含意・全称命題: intro，apply，specialize

含意 P → Q や全称命題 ∀ x, P x を示すときは，intro で仮定や変数を導入します． ゴールが P → Q なら intro hP は hP : P をローカルコンテキストに追加し，ゴールを Q に変えます． ゴールが ∀ x : α, P x なら intro x は任意の x : α を導入し，ゴールを P x に変えます．

example (P Q : Prop) (hQ : Q) : P → Q := by
  intro _hP
  exact hQ

example (P : Nat → Prop) (h : ∀ n : Nat, P n) : P 0 := by
  exact h 0

apply は，現在のゴールを証明するために使えそうな定理や仮定を適用します． ゴールが R で，hQR : Q → R があるとき，apply hQR により新しいゴールは Q になります． より一般には，結論が現在のゴールと一致するような定理を後ろ向きに使い，その定理の前提を新しいゴールとして残します．

example (P Q R : Prop) (hPQ : P → Q) (hQR : Q → R) (hP : P) : R := by
  apply hQR
  apply hPQ
  exact hP

全称命題を具体的な値に適用したいときは，関数適用のように書けます． specialize は，全称命題の仮定を特定の値に特殊化して，仮定そのものを書き換える tactic です． 次の例では，h : ∀ n, P n → Q n が specialize h 3 によって h : P 3 → Q 3 に変わります．

example (P Q : Nat → Prop) (h : ∀ n : Nat, P n → Q n) (hP : P 3) : Q 3 := by
  specialize h 3
  exact h hP

演習

intro と exact だけで証明してください． 余裕があれば，term-style proof でも同じ命題を書いてください．

example (P Q : Prop) (hQ : Q) : P → Q := by
  sorry