`fun_induction` についてもっと説明する

[Seasawher]

fun_induction f x1 x2 ... xn という風に引数を与えないとエラーになるケースと、引数を省略してもエラーにならないケースと存在する。この違いは何だろうか。ドキュメントコメントに書いてあったはずで、具体例とともに説明したい。

[Seasawher]

引数を省略するとエラーになる例

import Lean.LibrarySuggestions.Default

namespace List

variable {α : Type}

@[grind]
def last? (as : List α) : Option α :=
  match as with
  | [] => none
  | [a] => some a
  | _ :: bs => last? bs

@[grind =]
theorem last?_isSome {as : List α} (h : as ≠ []) : as.last?.isSome := by
  fun_induction last? with simp_all

@[grind =, simp]
theorem last?_append_singleton (as : List α) (a : α) :
    last? (as ++ [a]) = some a := by
  induction as with grind

-- @[grind =]
theorem last?_append (as bs : List α) :
  (as ++ bs).last? = if bs = [] then as.last? else bs.last? := by
  fun_induction last? bs generalizing as with try grind
  | case3 b bs hbs ih =>
    have ih := ih (as ++ [b])
    grind

example (as bs : List α) :
  (as ++ bs).last? = if bs = [] then as.last? else bs.last? := by
  fun_induction last? generalizing as with try grind -- エラー
  | case3 b bs hbs ih =>
    have ih := ih (as ++ [b])
    grind