unfold
unfold
は、式の展開(unfolding)を行うタクティクです。定義に基づいて式を展開します。
何も指定しなければゴールを変形しようとします。ローカルコンテキストにある項 h
について展開を行うには、unfold ... at h
のように at
を付けます。
dsimp
タクティクを使っても同様のことができます。基本的に dsimp
を使用することが推奨されます。
def myFun (n : Nat) : Nat :=
n + 1
example (n : Nat) : myFun n ≥ 1 := by
-- `dsimp` でも同じことができる
try
dsimp [myFun]
show n + 1 ≥ 1
fail
-- `myFun` を定義に展開する
unfold myFun
simp_arith