汎用的な tactic

decide

Lean が真偽を計算できる命題を決定して証明します． 有限な計算で判定できる命題に有効です． 対象の命題に対する Decidable インスタンスがあり，計算結果が真である場合にゴールを閉じます．

example : 3 < 5 := by
  decide

example : (2 + 2 = 4) := by
  decide

grind

書き換え，前向き推論，後ろ向き推論，場合分けなどを組み合わせる汎用自動化 tactic です． 強力ですが，何をしたのかが見えにくくなることもあるので，講義資料では短い例に限定して使います． 自動化 tactic は証明を短くしますが，初学段階ではまず手動の tactic でゴールの変化を追えるようにしておくことが重要です．

example (P Q R : Prop) (hPQ : P → Q) (hQR : Q → R) (hP : P) : R := by
  grind

example (P Q : Prop) (h : P ∧ Q) : Q ∧ P := by
  grind

simp や grind は便利ですが，証明が通らないときに原因を理解しにくいことがあります． 最初は intro，apply，constructor，cases，rw などで証明構造を書けるようにしてから，自動化を使うのがよいです．

演習

grind で閉じる論理問題を作り，手動証明と比較してください．

example (P Q R : Prop) (h₁ : P → Q) (h₂ : Q → R) (hP : P) : R := by
  -- `grind`
  sorry