fun_cases

fun_cases は、関数定義に応じて場合分けを行うためのタクティクです。

たとえば以下の例では、swapHead はリストに対して「空か、シングルトンか、そのほか」で場合分けをして定義されています。一方でリストは再帰的なデータ型としては「空か、そのほか」で定義されているため、cases タクティクで普通に場合分けをしようとすると場合分けの分岐が合いません。fun_cases を使うと、関数定義で使用された場合分けを再利用することができます。

variable {α : Type}

/-- リストの先頭２要素を入れ替える -/
@[simp]
def swapHead (xs : List α) : List α :=
  match xs with
  | [] => []
  | [x] => [x]
  | x :: y :: zs => y :: x :: zs

example (l : List α) : swapHead (swapHead l) = l := by
  fun_cases swapHead l <;> simp

-- `fun_cases` を使用しなかった場合、場合分けの手間が増える
example (l : List α) : swapHead (swapHead l) = l := by
  cases l with
  | nil => simp
  | cons x xs =>
    cases xs with
    | nil => simp
    | cons y ys => simp

舞台裏

Lean で関数 f を定義すると f.fun_cases という名前の補助的な定理が自動生成されます。fun_cases タクティクは、この補助定理を使用して場合分けを行っています。cases タクティクでも、using で明示的に指定すれば fun_cases と同様のことができます。

example (l : List α) : swapHead (swapHead l) = l := by
  cases l using swapHead.fun_cases <;> simp

関数内で宣言した補題の再利用

以上のように「関数定義に使用した場合分けを再利用できる」のが fun_cases タクティクの主な利点ですが、他にも「関数定義の中で宣言した補題を再利用できる」という利点があります。

variable {α : Type} [LE α] [DecidableEq α] [DecidableLE α]

instance : Min α := minOfLe

/-- リストの最小値を先頭に持ってくる -/
@[simp, grind]
def minFirst (xs : List α) : List α :=
  match h : xs with
  | [] => []
  | x :: xs =>
    let μ := List.min (x :: xs) (h := by simp)
    let rest := List.erase (x :: xs) μ

    -- 関数定義の中で補題を示しておくと、`fun_cases` で再利用できる
    have : (μ :: rest).length = (x :: xs).length := by
      grind [List.min_mem]

    μ :: rest

@[grind =]
theorem minFirst_length (xs : List α) :
    (minFirst xs).length = xs.length := by
  -- 普通にinductionすると失敗する
  fail_if_success induction xs with grind

  -- `fun_cases` を使うと成功する
  fun_cases minFirst xs with grind