cases_eliminator

[cases_eliminator] 属性は、cases タクティクで場合分けをした際の枝を変更します。

より詳しくいうと、cases タクティクの using キーワードのデフォルトの引数を変更することができます。デフォルトでは、帰納型 T に対して T.casesOn という定理が自動生成されてそれが暗黙の裡に using キーワードの引数として使われますが、[cases_eliminator] 属性で別な定理を指定すると、それが使われるようになります。

variable {α : Type}

/-- 遅延評価のリストもどき -/
inductive Many (α : Type) where
  | none : Many α
  | more : α → (Unit → Many α) → Many α

example (xs : Many α) : True := by
  cases xs with
  | none => trivial
  | more x xs =>
    -- xs の型が Unit → Many α になっており、
    -- 必要なとき毎回 xs () で取り出さなければならず面倒
    guard_hyp xs : Unit → Many α
    trivial

/-- Unit が登場しないように工夫した関数 -/
def Many.cons (x : α) (xs : Many α) : Many α :=
  .more x (fun () => xs)

-- Many を定義したときに自動生成される定理
/--
info: CasesEliminator.Many.casesOn.{u} {α : Type} {motive : Many α → Sort u}
  (t : Many α) (none : motive Many.none)
  (more : (a : α) → (a_1 : Unit → Many α) → motive (Many.more a a_1)) : motive t
-/
#guard_msgs (whitespace := lax) in #check Many.casesOn

/-- Many.casesOn の more を cons に置き換えたバージョン。
この定理に `[cases_eliminator]` 属性を与えることで、
`casesOn` の代わりにこれがデフォルトで使われるようになる。 -/
@[cases_eliminator]
protected def Many.cons_casesOn.{u} {α : Type} {motive : Many α → Sort u} (t : Many α) (none : motive Many.none)
    (cons : (a : α) → (b : Many α) → motive (Many.cons a b)) : motive t := by
  match t with
  | .none => assumption
  | .more x xs =>
    exact cons x (xs ())

example (xs : Many α) : True := by
  cases xs

  case none => trivial

  -- case で分割したときのデフォルトのコンストラクタが cons に変わる
  case cons x xs =>
    -- xs の型が Many α になっている！
    guard_hyp xs : Many α
    trivial

デフォルトの挙動に戻すには、using キーワードに .casesOn を渡します。

example (x : Many α) : True := by
  cases x using Many.casesOn
  case none => trivial
  case more x => trivial

なお rcases には影響しません。

example (xs : Many α) : True := by
  rcases xs with _ | _

  case none => trivial

  case more _ xs =>
    -- xs の型が Unit → Many α になっている
    guard_hyp xs : Unit → Many α
    trivial

Lean by Example

cases_eliminator