simp_all
simp_all
タクティクは、simp
タクティクの派生で、仮定とゴールに対してこれ以上適用できなくなるまで simp
を適用します。
simp at *
と似ていますが、simp_all
は簡約された仮定を再び簡約に使うなど再帰的な挙動をします。
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