simp_all

simp_all タクティクは、simp タクティクの派生で、仮定とゴールに対してこれ以上適用できなくなるまで simp を適用します。

simp at * と似ていますが、simp_all は簡約された仮定を再び簡約に使うなど再帰的な挙動をします。

section
  /- ## simp_all では示せるが simp at * では示せない例 -/

  example (P : Nat → Bool)
      (h1 : P (if 0 + 0 = 0 then 1 else 2))
      (h2 : P (if P 1 then 0 else 1) ) : P 0 := by
    simp at *

    -- まだゴールが残っている
    show P 0

    simp [h1] at h2
    assumption

  example (P : Nat → Bool)
      (h1 : P (if 0 + 0 = 0 then 1 else 2))
      (h2 : P (if P 1 then 0 else 1) ) : P 0 := by
    -- 一発で終わる。
    -- h1 を簡約した後で、h2 を「簡約後の h1」を使って簡約し、
    -- ゴールと仮定が一致していることを確認するという挙動をする。
    simp_all
end

なお simp_all はローカルコンテキストにある命題を使って単純化を行おうとするため、ローカルコンテキストにある命題によってはエラーになることがあります。¹

/-
error: tactic 'simp' failed, nested error:
maximum recursion depth has been reached
use `set_option maxRecDepth <num>` to increase limit
use `set_option diagnostics true` to get diagnostic information
-/
example (_h : 1 + 1 = 2) : True := by
  have : 1 = 1 + 1 - 1 := by simp

  -- `simp_all` では示せない
  -- 仮定にある `1` を `1 + 1 - 1` に置き換えて無限ループになっているようだ
  simp_all

example (_h : 1 + 1 = 2) : True := by
  -- 左辺と右辺を逆にしてみると
  have : 1 + 1 - 1 = 1 := by simp

  -- `simp_all` で示せるようになる
  simp_all

¹ ここで挙げているコード例は、Lean の公式 Zulip の aesop with a "bad simp hypothesis" in the context というスレッドで Frédéric Dupuis さんが挙げたコード例を参考にしています。