flexible_induction_on.lean

inductive induction_target :=
| expr : expr -> induction_target
| name : name → induction_target

definition expr_to_induction_target [coercion] (e : expr) : induction_target :=
  induction_target.expr e

definition name_to_induction_target [coercion] (n : name) : induction_target :=
  induction_target.name n

definition string_to_induction_target [coercion] (s : string) : induction_target :=
  induction_target.name s

meta_definition mk_n_fresh_names (n : nat) : tactic (list name) :=
  match n with
  | 0 := return []
  | nat.succ m := do
    fresh <- tactic.mk_fresh_name,
    tail <- mk_n_fresh_names m,
    return (fresh :: tail)
  end

meta_definition induction_on (target : induction_target) : tactic unit := do
  H <- (match target with | induction_target.name n := tactic.get_local n
                          | induction_target.expr e := return e
                          end),
  t <- tactic.infer_type H,
  let type_sym := expr.get_app_fn t in
  let type_name := expr.const_name type_sym in
  let recursor := type_name <.> "rec_on" in do
    k <- tactic.mk_const recursor,
    arity <- tactic.get_arity k,
    ns <- mk_n_fresh_names arity,
    tactic.induction_core tactic.transparency.semireducible H recursor ns

open tactic

theorem nat_add_comm : Π (n m : nat), n + m = n + m =
  by do intros, induction_on "n"