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