タクティク

タクティクは、Lean において証明を対話的に行ったり自動化したりすることを可能にするものです。

なお本書は全部のタクティクを網羅していません。Mathlib の全タクティクのリストが必要であれば Mathlib4 Help を参照してください。

よく使うタクティク早見表

Lean で利用可能なタクティクは多岐にわたるので、ここによく使うタクティクの早見表を載せておきます。

関数と等式系

タクティク	用途
`rw`	`A = B` という等式を使って書き換えを行いたいとき
`rfl`	`A = B` という等式を定義に展開することで示したいとき
`congr`	`f a = f b` を `a = b` に帰着して示したいとき
`calc`	等式を連鎖させて `a = b` を示したいとき

命題論理系

タクティク	用途
`exact`	仮定 `h : A` からゴール `⊢ A` を示したいとき
`assumption`	仮定の中にゴールと同じものがあるとき
`intro`	`A → B` を示したいとき
`apply`	`h : A → B` という仮定や命題を使いたいとき
`constructor`	`A ∧ B` や `A ↔ B` を示したいとき
`obtain`	`h : A ∧ B` という仮定や命題を分解したいとき
`rw`	`h : A ↔ B` という仮定や命題を使って書き換えを行いたいとき
`left`	`⊢ A ∨ B` というゴールを `⊢ A` に帰着したいとき
`right`	`⊢ A ∨ B` というゴールを `⊢ B` に帰着したいとき
`cases`	仮定 `h : A ∨ B` をもとに場合分けしたいとき
`by_cases`	命題 `A` について `A ∨ ¬ A` という場合分けを行いたいとき
`exfalso`	ゴールを矛盾を示すことに帰着したいとき
`contradiction`	`A` と `¬ A` が両方成り立つことからゴールを閉じたいとき
`have`	証明の途中で補題を立てたいとき
`suffices`	ゴールを十分条件に帰着したいとき

述語論理系

タクティク	用途
`intro`	`∀ x, P x` を示したいとき
`exists`	`∃ x, P x` を示したいとき
`obtain`	`h : ∃ x, P x` という仮定や命題を分解したいとき

帰納型と帰納法

タクティク	用途
`induction`	帰納法を行いたいとき
`fun_induction`	関数定義に基づいて帰納法を行いたいとき
`cases`	帰納型の値をコンストラクタに基づいて場合分けしたいとき
`fun_cases`	関数定義に基づいて場合分けしたいとき
`ext`	外延性を利用したいとき
`unfold`	名前を定義に展開したいとき

ライブラリ検索と自動証明

タクティク	用途
`exact?`	ゴールを閉じることのできる補題を検索したいとき
`rw?`	ゴールを書き換えることのできる補題を検索したいとき
`decide`	計算によって命題の真偽を判定したいとき
`simp`	等式書き換えによる単純化を自動で行いたいとき
`grind`	書き換え・前方推論・後方推論・場合分けを自動で行いたいとき
`try?`	とりあえず証明したいとき