From 64526c2b1c695ab0384f6424b9d1791bf6195fd7 Mon Sep 17 00:00:00 2001 From: Seasawher Date: Thu, 14 Nov 2024 22:52:15 +0900 Subject: [PATCH] =?UTF-8?q?`apply`=20=E3=81=A8=20`exact`=20=E3=81=AE?= =?UTF-8?q?=E9=81=95=E3=81=84=20Fixes=20#1073?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- LeanByExample/Reference/Tactic/Apply.lean | 38 ++++++++++++++++------- 1 file changed, 26 insertions(+), 12 deletions(-) diff --git a/LeanByExample/Reference/Tactic/Apply.lean b/LeanByExample/Reference/Tactic/Apply.lean index 4a673880..14d786f5 100644 --- a/LeanByExample/Reference/Tactic/Apply.lean +++ b/LeanByExample/Reference/Tactic/Apply.lean @@ -1,8 +1,6 @@ /- # apply `apply` は含意 `→` をゴールに適用するタクティクです。ゴールが `⊢ Q` で、ローカルコンテキストに `h : P → Q` があるときに、`apply h` を実行するとゴールが `⊢ P` に書き換わります。 - -「十分条件でゴールを置き換える」タクティクであると言えますが、十分条件がローカルコンテキストに存在しない場合は [`suffices`](./Suffices.md) の使用も検討してください。 -/ variable (P Q : Prop) @@ -15,17 +13,13 @@ example (h : P → Q) (hP : P) : Q := by exact hP -/- 注意点として、`h : P → Q` は `P` の証明を受け取って `Q` の証明を返す関数でもあるので、上記の例は `apply` を使わずに `exact h hP` で閉じることもできます。-/ - -example (h : P → Q) (hP : P) : Q := by - exact h hP +/- 「十分条件でゴールを置き換える」タクティクであると言えますが、十分条件がローカルコンテキストに存在しない場合は [`suffices`](./Suffices.md) の使用も検討してください。-/ -/- さらに [`exact`](./Exact.md) の代わりに `apply` を使うこともできます。-/ +/- ## 特殊な用途 -example (h : P → Q) (hP : P) : Q := by - apply h hP - -/- また、Lean では否定 `¬ P` は `P → False` として実装されているため、ゴールが `⊢ False` であるときに `hn : ¬P` に対して `apply hn` とするとゴールが `⊢ P` に書き換わります。 -/ +### 仮説から否定を消去する +Lean では否定 `¬ P` は `P → False` として実装されているため、ゴールが `⊢ False` であるときに `hn : ¬P` に対して `apply hn` とするとゴールを `⊢ P` に書き換えることができます。 +-/ -- P の否定は、「P を仮定すると矛盾する」ということに等しい example : (¬ P) = (P → False) := by rfl @@ -35,7 +29,27 @@ example (hn : ¬ P) (hP : P) : False := by show P exact hP -/- ## 補足 +/- ### exact の強力版として + +[`exact`](./Exact.md) の代わりに `apply` を使うこともできます。-/ + +example (hP : P) : P := by + apply hP + +example (h : P → Q) (hP : P) : Q := by + apply h hP + +/- また仮定に全称命題の証明 `h : ∀ a, P a` があってゴールが `P a` であるとき、`exact h` は失敗しますが `apply h` であれば成功します。これは「`exact` では通りそうで通らないが `apply` では通る例」であると言えるかもしれません。-/ + +variable {α : Type} + +example (a : α) (P : α → Prop) (h : ∀ a, P a) : P a := by + -- `exact h` は失敗する + fail_if_success exact h + + apply h + +/- ## 舞台裏 一般に、`apply` は関数適用を逆算するタクティクです。手元に関数 `f : A → B` があって型 `B` の型を作りたいとき、`A` の項を構成すれば `f` に適用することで `B` の項が得られる…といった推論を行います。 -/