apply

apply は含意 → をゴールに適用するタクティクです。ゴールが ⊢ Q で、ローカルコンテキストに h : P → Q があるときに、apply h を実行するとゴールが ⊢ P に書き換わります。

「十分条件でゴールを置き換える」タクティクであると言えますが、十分条件がローカルコンテキストに存在しない場合は suffices の使用も検討してください。

variable (P Q : Prop)

/-- `P → Q` かつ `P` ならば `Q` -/
example (h : P → Q) (hP : P) : Q := by
  apply h

  -- ゴールが `P` に変わっている
  show P

  exact hP

注意点として、h : P → Q は P の証明を受け取って Q の証明を返す関数でもあるので、上記の例は apply を使わずに exact h hP で閉じることもできます。

example (h : P → Q) (hP : P) : Q := by
  exact h hP

さらに exact の代わりに apply を使うこともできます。

example (h : P → Q) (hP : P) : Q := by
  apply h hP

また、Lean では否定 ¬ P は P → False として実装されているため、ゴールが ⊢ False であるときに hn : ¬P に対して apply hn とするとゴールが ⊢ P に書き換わります。

-- P の否定は、「P を仮定すると矛盾する」ということに等しい
example : (¬ P) = (P → False) := by rfl

example (hn : ¬ P) (hP : P) : False := by
  apply hn
  show P
  exact hP

補足

一般に、apply は関数適用を逆算するタクティクです。手元に関数 f : A → B があって型 B の型を作りたいとき、A の項を構成すれば f に適用することで B の項が得られる…といった推論を行います。

-- 関数をタクティクを使用して構成する例
def apply {α β : Type} (f : α → β) (a : α) : β := by
  apply f
  exact a