done

done は、証明終了の合図です。証明すべきゴールが残っていない時に成功し、それ以外の時にはエラーになります。QED のようなものです。証明がサブゴールに分かれている場合、サブゴールごとに判定を行います。

example (P Q : Prop) (h : P → Q) : ¬ P ∨ Q := by
  -- `P` が成り立つかどうかで場合分けを行う
  by_cases hP : P

  -- `P` が成り立つ場合
  case pos =>
    -- `P → Q` より `Q` が成り立つ
    have := h hP

    -- したがって結論が従う
    exact Or.inr this

    -- `P` が成り立つ場合の証明終わり。
    done

  -- `P` が成り立たない場合
  case neg =>
    -- `¬ P` が成り立つので、`¬ P ∨ Q` も成り立つ
    exact Or.inl hP

    -- `P` が成り立たない場合の証明終わり。
    done

舞台裏

getUnsolvedGoals という関数で、現在の残りのゴールを取得することができます。これを利用すると、done タクティクと同様のはたらきをするタクティクを自作することができます。ここでは elab コマンドを使った実装を紹介します。

open Lean.Elab Tactic Term in

elab "my_done" : tactic => do
  -- 未解決のゴールを List として取得する
  let gs ← getUnsolvedGoals

  -- ゴールが残っている場合はエラーにする
  unless gs.isEmpty do
    reportUnsolvedGoals gs
    throwAbortTactic

example : 1 = 1 := by
  rfl
  my_done

/-
error: unsolved goals
⊢ 2 = 2
-/
example : 1 = 1 ∧ 2 = 2 := by
  refine ⟨rfl, ?_⟩
  my_done

これを使うと、派生タクティクを自作することもできます。ゴールを閉じたときに 🎉 でお祝いしてくれるタクティクを自作してみましょう。

open Lean Elab Tactic Term in

elab "tada" : tactic => do
  let gs ← getUnsolvedGoals

  unless gs.isEmpty do
    reportUnsolvedGoals gs
    throwAbortTactic

  -- ゴールが残っていない場合はお祝いメッセージを表示する
  logInfo "Goals accomplished 🎉"

/- info: Goals accomplished 🎉 -/
example : 1 = 1 := by
  rfl
  tada