apply_assumption
apply_assumption
は、ゴールが ⊢ head
であるときに、... → ∀ _, ... → head
という形の命題をローカルコンテキストから探し、それを用いてゴールを書き換えます。
variable (P Q R : Prop)
example (hPQ : P → Q) : ¬ Q → ¬ P := by
intro hQn hP
-- 矛盾を示したい
show False
-- 自動で `hQn` を適用
apply_assumption
show Q
-- 自動で `hPQ` を適用
apply_assumption
show P
-- 自動で `hP` を適用
apply_assumption
-- 証明終わり
done
タクティクを繰り返すことを指示するタクティク repeat
と組み合わせると、「ローカルコンテキストにある仮定を適切に選んで apply
, exact
することを繰り返し、ゴールを閉じる」ことができます。
example (hPQ : P → Q) (hQR : Q → R) (hQ : P) : R := by
repeat apply_assumption