apply(Lean)

含意 → をゴールに適用するタクティク

「モーダスポネンスのような推論規則を適用するタクティク」という説明も正確ではないけれど近い説明になりそう

$ \frac{P→Q\quad P}{Q}

使い方

apply h2 at h1なら仮定h2を仮定h1に適用する

code:memo

h1: x = 37

h2: x = 37 → y = 42

↓ apply h2 at h1

h2: x = 37 → y = 42

h1: y = 42

apply succ_inj at hなら仮定hのsuccを除去する

succ(a) = succ(b)→a = b

code:memo

h: succ (succ 0) = succ (succ (succ 0))

↓ apply succ_inj at h

h: succ 0 = succ (succ 0)

apply succ_injならゴールに適用する

$ A \to (B \land C), (B \land C) \to \lnot D \vDash A \to \lnot D の証明

code:lean

example (A B C D : Prop)

(h1 : A → (B ∧ C))

(h2 : (B ∧ C) → ¬D)

: A → ¬D := by

intro ha -- a → ¬dが ha : a と ⊢ ¬d に分かれる

apply h2 -- ¬dを(b ∧ c)で置き換えて、ゴールが ⊢ (b ∧ c)になる

-- 含意(→)の左側、十分条件部分でゴールを置き換えている

apply h1 -- ゴールが ⊢ aになる

exact ha -- ha : aと ⊢ aを比較?して証明完了

applyでよくわからなくなったらapply?を試すとよい

現在のゴールに適用可能なmathlibの定理(もしくは定義)を探すタクティク

code:lean

example Group G Group H (f : G →* H) (a b : G) :

f (a * b) = f a * f b := by

-- apply?を使うと「Try this: exact MonoidHom.map_mul f a b」というメッセージが出る(!!)

exact MonoidHom.map_mul f a b