TL;DR
Lean などの定理証明支援系で、証明をどう組み立てるかを指示する命令。by に続けてタクティクを並べ、ゴールを 1 つずつ変形して証明を完成させる。
なぜ必要か
Lean の公式チュートリアル Theorem Proving in Lean 4 によると、証明は証明項として表せるが、タクティクを使うと証明項を直接書くより短く、楽に書ける。また、タクティクは Lean の自動化を使う入り口にもなる。ゼロから始めるLean言語入門 ― 手を動かして学ぶ形式数学ライブラリ開発でも、タクティクは定理の証明に必要な操作をプログラムとして対話的に書くための機能として紹介されている。
仕組み
定理を宣言すると、示すべき目標であるゴールができる。ゴールは使える仮定と ⊢ の後ろの目標からなる。各タクティクは現在のゴールを変形し、すべてのゴールがなくなると証明が終わる。証明が終わっていなければ、Lean は残ったゴールをエラーとして示す。
代表的なタクティクには仮定を文脈に導入する intro、関数とみなせる式を適用して残りの引数を新しいゴールにする apply、式でゴールをちょうど埋める exact がある。
例
theorem test (p q : Prop) (hp : p) (hq : q) : p ∧ q ∧ p := by
apply And.intro
· exact hp
· apply And.intro
· exact hq
· exact hp注意点
Theorem Proving in Lean 4 によると、タクティクで書いた証明は、各ステップの結果を読み手が追う必要があるので、証明項より読みにくくなることがある。ゼロから始めるLean言語入門 ― 手を動かして学ぶ形式数学ライブラリ開発 によると、タクティクは Lean 固有の機能ではなく、Rocq（旧称 Coq）なども持っている。