feat(library/init/meta): improve induction tactic interface

It uses .rec recursor when it is not specified

library/init/meta/interactive.lean

@@ -264,12 +264,7 @@ do e_type ← infer_type e >>= whnf,
    return I
 
 meta def induction (p : parse texpr) (rec_name : parse using_ident) (ids : parse with_ident_list) : tactic unit :=
-do e ← i_to_expr p,
-   match rec_name with
-   | some n := tactic.induction e n ids
-   | none   := do I ← get_type_name e, tactic.induction e (I <.> "rec") ids
-   end,
-   return ()
+do e ← i_to_expr p, tactic.induction e ids rec_name, return ()
 
 meta def cases (p : parse texpr) (ids : parse with_ident_list) : tactic unit :=
 do e ← i_to_expr p,

library/init/meta/mk_dec_eq_instance.lean

@@ -104,7 +104,7 @@ do I_name ← get_dec_eq_type_name,
    -- Use brec_on if type is recursive.
    -- We store the functional in the variable F.
    if is_recursive env I_name
-   then intro1 >>= (λ x, induction x (I_name <.> "brec_on") (idx_names ++ [v_name, F_name]) >> return ())
+   then intro1 >>= (λ x, induction x (idx_names ++ [v_name, F_name]) (some $ I_name <.> "brec_on") >> return ())
    else intro v_name >> return (),
    -- Apply cases to first element of type (I ...)
    get_local v_name >>= cases,

library/init/meta/mk_has_sizeof_instance.lean

@@ -67,7 +67,7 @@ do I_name ← get_has_sizeof_type_name,
    -- Use brec_on if type is recursive.
    -- We store the functional in the variable F.
    if is_recursive env I_name
-   then intro `_v >>= (λ x, induction x (I_name <.> "brec_on") [v_name, F_name] >> return ())
+   then intro `_v >>= (λ x, induction x [v_name, F_name] (some $ I_name <.> "brec_on") >> return ())
    else intro v_name >> return (),
    arg_names : list (list name) ← mk_constructors_arg_names I_name `_p,
    get_local v_name >>= λ v, cases v (join arg_names),

library/init/meta/smt/smt_tactic.lean

@@ -384,8 +384,8 @@ meta def add_lemmas_from_facts_core : list expr → smt_tactic unit
 meta def add_lemmas_from_facts : smt_tactic unit :=
 get_facts >>= add_lemmas_from_facts_core
 
-meta def induction (e : expr) (rec : name) (ids : list name) : smt_tactic unit :=
-slift (tactic.induction e rec ids >> return ()) -- pass on the information?
+meta def induction (e : expr) (ids : list name := []) (rec : option name := none) : smt_tactic unit :=
+slift (tactic.induction e ids rec >> return ()) -- pass on the information?
 
 meta def when (c : Prop) [decidable c] (tac : smt_tactic unit) : smt_tactic unit :=
 if c then tac else skip

library/init/meta/tactic.lean

@@ -369,8 +369,10 @@ meta constant abstract_eq     : expr → expr → tactic bool
    It returns for each new goal a list of new hypotheses and a list of substitutions for hypotheses
    depending on `h`. The substitutions map internal names to their replacement terms. If the
    replacement is again a hypothesis the user name stays the same. The internal names are only valid
-   in the original goal, not in the type context of the new goal. -/
-meta constant induction (h : expr) (rec : name) (ns : list name := []) (md := semireducible) : tactic (list (list expr × list (name × expr)))
+   in the original goal, not in the type context of the new goal.
+
+   If `rec` is none, then the type of `h` is inferred, if it is of the form `C ...`, tactic uses `C.rec` -/
+meta constant induction (h : expr) (ns : list name := []) (rec : option name := none) (md := semireducible) : tactic (list (list expr × list (name × expr)))
 /- Apply `cases_on` recursor, names for the new hypotheses are retrieved from `ns`.
    `h` must be a local constant. It returns for each new goal the name of the constructor, a list of new hypotheses, and a list of
    substitutions for hypotheses depending on `h`. The number of new goals may be smaller than the

src/library/tactic/induction_tactic.cpp

@@ -344,8 +344,26 @@ vm_obj induction_tactic_core(transparency_mode const & m, expr const & H, name c
     }
 }
 
-vm_obj tactic_induction(vm_obj const & H, vm_obj const & rec, vm_obj const & ns, vm_obj const & m, vm_obj const & s) {
-    return induction_tactic_core(to_transparency_mode(m), to_expr(H), to_name(rec), to_list_name(ns), tactic::to_state(s));
+vm_obj tactic_induction(vm_obj const & H, vm_obj const & ns, vm_obj const & rec, vm_obj const & m, vm_obj const & s) {
+    if (is_none(rec)) {
+        try {
+            type_context ctx = mk_type_context_for(s, m);
+            expr type = ctx.infer(to_expr(H));
+            expr C    = get_app_fn(type);
+            if (is_constant(C)) {
+                name C_rec(const_name(C), "rec");
+                return induction_tactic_core(to_transparency_mode(m), to_expr(H), C_rec, to_list_name(ns), tactic::to_state(s));
+            } else {
+                return tactic::mk_exception("induction tactic failed, inductive datatype expected",
+                                            tactic::to_state(s));
+            }
+        } catch (exception & ex) {
+            return tactic::mk_exception(ex, tactic::to_state(s));
+        }
+    } else {
+        return induction_tactic_core(to_transparency_mode(m), to_expr(H),
+                                     to_name(get_some_value(rec)), to_list_name(ns), tactic::to_state(s));
+    }
 }
 
 void initialize_induction_tactic() {

tests/lean/induction_tac1.lean

@@ -3,7 +3,7 @@ open tactic
 example (p q : Prop) : p ∨ q → q ∨ p :=
 by do
   H ← intro `H,
-  induction H `or.rec [`Hp, `Hq],
+  induction H [`Hp, `Hq],
   trace_state,
   constructor_idx 2, assumption,
   constructor_idx 1, assumption
@@ -14,7 +14,7 @@ open nat
 example (n : ℕ) : n = 0 ∨ n = succ (pred n) :=
 by do
   n ← get_local `n,
-  induction n `nat.rec [`n', `Hind],
+  induction n [`n', `Hind],
   trace_state,
   constructor_idx 1, reflexivity,
   constructor_idx 2, reflexivity,
@@ -25,7 +25,7 @@ print "-----"
 example (n : ℕ) (H : n ≠ 0) : n > 0 → n = succ (pred n) :=
 by do
   n ← get_local `n,
-  induction n `nat.rec [],
+  induction n [],
   trace_state,
   intro `H1, contradiction,
   intros, reflexivity

tests/lean/run/induction_tac3.lean

@@ -3,7 +3,7 @@ open tactic
 example (p q : Prop) : p ∨ q → q ∨ p :=
 by do
   H ← intro `H,
-  induction H `or.rec [],
+  induction H,
   constructor_idx 2, assumption,
   constructor_idx 1, assumption
 
@@ -11,7 +11,7 @@ open nat
 example (n : ℕ) : n = 0 ∨ n = succ (pred n) :=
 by do
   n ← get_local `n,
-  induction n `nat.rec [],
+  induction n,
   constructor_idx 1, reflexivity,
   constructor_idx 2, reflexivity,
   return ()
@@ -19,6 +19,6 @@ by do
 example (n : ℕ) (H : n ≠ 0) : n > 0 → n = succ (pred n) :=
 by do
   n ← get_local `n,
-  induction n `nat.rec [],
+  induction n,
   intro `H1, contradiction,
   intros, reflexivity

tests/lean/run/induction_tactic_delta.lean

@@ -11,5 +11,5 @@ definition foo'.rec := @foo.rec
 
 example : Pi (x : foo'), x = x :=
 by do x ← intro `x,
-      induction x `foo'.rec [],
+      induction x,
       reflexivity

tests/lean/run/unfold_crash.lean

@@ -26,7 +26,7 @@ theorem vappend_assoc :
 by do
      intros,
      v <- get_local `v1,
-     induction v (`vector.rec_on) [],
+     induction v,
      v2 ← get_local `v2,
      cases v2 [`m, `h2, `t2],
      trace_state, trace "------",

tests/lean/unfold1.lean

@@ -6,7 +6,7 @@ do get_local Hname >>= rewrite_core reducible tt tt occurrences.all ff,
 
 example (l : list nat) : list.append l [] = l :=
 by do
-  get_local `l >>= λ H, induction H `list.rec_on [`h, `t, `iH],
+  get_local `l >>= λ H, induction H [`h, `t, `iH],
   --
   dunfold [`list.append],
   trace_state,