induction_eliminator

[induction_eliminator] 属性は、帰納法の枝を変更することを可能にします。

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

variable {α : Type}

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

/-- Many に対する合併関数 -/
def Many.union : Many α → Many α → Many α
  | .none, ys => ys
  | .more x xs, ys => Many.more x (fun () => union (xs ()) ys)

-- Many に関する定理を帰納法で示す例
example (xs : Many α) : Many.union xs Many.none = xs := by
  induction xs with
  | none => rfl
  | more x xs ih =>
    -- ここで xs の型は Unit → Many α になっている
    -- 必要なとき毎回 xs () で取り出さなければならず面倒
    guard_hyp xs : Unit → Many α

    simp [Many.union, ih]

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

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

-- Many.rec の `Many.more` の部分を `Many.cons` に置き換えた定理を作る。
-- これに `[induction_eliminator]` 属性を与えることで、
-- コンストラクタ `Many.more` の代わりに `Many.cons` が使えるようになる
@[induction_eliminator]
protected def Many.cons_rec.{u} {α : Type} {motive : Many α → Sort u}
  (none : motive Many.none)
  (cons : (a : α) → (b : Many α) → (motive b) → motive (Many.cons a b))
    : (t : Many α) → motive t
  | .none => none
  | .more x xs => cons x (xs ()) (Many.cons_rec none cons (xs ()))

example (xs : Many α) : Many.union xs Many.none = xs := by
  induction xs with
  | none => rfl
  | cons x xs ih =>
    -- ここで xs の型が Many α になっている！
    -- 毎回 `xs ()` などと書く必要がなくなった
    guard_hyp xs : Many α

    simp [Many.union, Many.cons, ih]

[induction_eliminator] を設定する前の挙動に戻すには、using キーワードに明示的に .rec 定理を与えます。

example (xs : Many α) : True := by
  -- 明示的に指定すれば， 元の挙動に戻せる
  induction xs using Many.rec with
  | none => trivial
  | more _ xs _ =>
    -- 元のように Many.more が使われる
    guard_hyp xs : Unit → Many α

    trivial

Lean by Example

induction_eliminator