try

try は、失敗するかもしれないタクティクをエラーにすることなく実行します。try で指定されたタクティクが成功した場合は try なしの場合と変わりませんが、失敗した場合は try 実行前の状態に戻ります。

import Aesop -- `aesop` を使用するため

variable (P Q : Prop)

example : (P → Q) → (¬ Q → ¬ P) := by
  -- `assumption` は通らないが、エラーにならない
  try assumption

  try
    -- `aesop` が通り、証明が終了する
    aesop
    done

    -- 強制的に失敗させる
    fail

  -- `try` 実行前の状態に戻る
  show (P → Q) → ¬Q → ¬P

  aesop