feat(src/library/tactic): tactic.induction_core returns for each new goal the list of introduced hypotheses and substitutions for dependent hypotheses

Also add to_obj(buffer<vm_obj>) to construct a vm-list of vm objects.

library/init/meta/interactive.lean

@@ -312,7 +312,8 @@ do e ← i_to_expr p,
    match rec_name with
    | some n := induction_core semireducible e n ids
    | none   := do I ← get_type_name e, induction_core semireducible e (I <.> "rec") ids
-   end
+   end,
+   return ()
 
 meta def cases (p : qexpr0) (ids : 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_core semireducible x (I_name <.> "brec_on") (idx_names ++ [v_name, F_name]))
+   then intro1 >>= (λ x, induction_core semireducible x (I_name <.> "brec_on") (idx_names ++ [v_name, F_name]) >> return ())
    else intro v_name >> return (),
 
    -- Apply cases to first element of type (I ...)

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_core semireducible x (I_name <.> "brec_on") [v_name, F_name])
+   then intro `_v >>= (λ x, induction_core semireducible x (I_name <.> "brec_on") [v_name, F_name] >> return ())
    else intro v_name >> return (),
    arg_names : list (list name) ← mk_constructors_arg_names I_name `_p,
    get_local v_name >>= λ v, cases_using v (join arg_names),

library/init/meta/smt/smt_tactic.lean

@@ -361,7 +361,7 @@ 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)
+slift (tactic.induction e rec ids >> return ()) -- pass on the information?
 
 end smt_tactic
 

library/init/meta/tactic.lean

@@ -413,8 +413,13 @@ meta constant abstract_hash : expr → tactic nat
 meta constant abstract_weight : expr → tactic nat
 meta constant abstract_eq     : expr → expr → tactic bool
 /- (induction_core m H rec ns) induction on H using recursor rec, names for the new hypotheses
-   are retrieved from ns. If ns does not have sufficient names, then use the internal binder names in the recursor. -/
-meta constant induction_core : transparency → expr → name → list name → tactic unit
+   are retrieved from ns. If ns does not have sufficient names, then use the internal binder names
+   in the recursor.
+   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_core : transparency → expr → name → list name → tactic (list (list expr × list (name × expr)))
 /- (cases_core m H ns) apply cases_on recursor, names for the new hypotheses are retrieved from ns.
    H must be a local constant -/
 meta constant cases_core     : transparency → expr → list name → tactic unit
@@ -866,7 +871,7 @@ cases_core semireducible H []
 meta def cases_using : expr → list name → tactic unit :=
 cases_core semireducible
 
-meta def induction : expr → name → list name → tactic unit :=
+meta def induction : expr → name → list name → tactic (list (list expr × list (name × expr))) :=
 induction_core semireducible
 
 meta def destruct (e : expr) : tactic unit :=

src/library/tactic/induction_tactic.cpp

@@ -320,10 +320,25 @@ vm_obj induction_tactic_core(transparency_mode const & m, expr const & H, name c
     try {
         metavar_context mctx = s.mctx();
         list<name> tmp_ns = ns;
+        list<list<expr>> hyps;
+        hsubstitution_list substs;
         list<expr> new_goals = induction(s.env(), s.get_options(), m, mctx, head(s.goals()), H, rec_name, tmp_ns,
-                                         nullptr, nullptr);
+                                         &hyps, &substs);
         tactic_state new_s   = set_mctx_goals(s, mctx, append(new_goals, tail(s.goals())));
-        return mk_tactic_success(new_s);
+
+        buffer<vm_obj> info;
+        while (!is_nil(hyps)) {
+            vm_obj hyps_obj = to_obj(head(hyps));
+            buffer<vm_obj> substs_objs;
+            head(substs).for_each([&](name const & from, expr const & to) {
+                    substs_objs.push_back(mk_vm_pair(to_obj(from), to_obj(to)));
+                });
+
+            info.push_back(mk_vm_pair(hyps_obj, to_obj(substs_objs)));
+            hyps = tail(hyps);
+            substs = tail(substs);
+        }
+        return mk_tactic_success(to_obj(info), new_s);
     } catch (exception & ex) {
         return mk_tactic_exception(ex, s);
     }

src/library/vm/vm_list.cpp

@@ -32,6 +32,8 @@ vm_obj to_obj(list<name> const & ls) { return list_to_obj(ls); }
 vm_obj to_obj(list<level> const & ls) { return list_to_obj(ls); }
 vm_obj to_obj(list<expr> const & ls) { return list_to_obj(ls); }
 
+vm_obj to_obj(list<list<expr>> const & ls) { return list_to_obj(ls); }
+
 vm_obj to_obj(buffer<name> const & ls) { return to_obj(to_list(ls)); }
 vm_obj to_obj(buffer<level> const & ls) { return to_obj(to_list(ls)); }
 vm_obj to_obj(buffer<expr> const & ls) { return to_obj(to_list(ls)); }
@@ -106,6 +108,13 @@ vm_obj to_obj(list<unsigned> const & ls) {
     return to_vm_list(ls, [&](unsigned n) { return mk_vm_nat(n); });
 }
 
+vm_obj to_obj(buffer<vm_obj> const & ls) {
+    vm_obj obj = mk_vm_nil();
+    for (unsigned i = ls.size(); i > 0; i--)
+        obj = mk_vm_cons(ls[i - 1], obj);
+    return obj;
+}
+
 void initialize_vm_list() {
     DECLARE_VM_CASES_BUILTIN(name({"list", "cases_on"}), list_cases_on);
 }

src/library/vm/vm_list.h

@@ -26,6 +26,7 @@ list<expr> to_list_expr(vm_obj const & o);
 void to_buffer_expr(vm_obj const & o, buffer<expr> & r);
 vm_obj to_obj(buffer<expr> const & ls);
 vm_obj to_obj(list<expr> const & ls);
+vm_obj to_obj(list<list<expr>> const & ls);
 
 template<typename A, typename F>
 vm_obj to_vm_list(list<A> const & ls, F const & fn) {
@@ -34,6 +35,7 @@ vm_obj to_vm_list(list<A> const & ls, F const & fn) {
 }
 
 vm_obj to_obj(list<unsigned> const & ls);
+vm_obj to_obj(buffer<vm_obj> const & ls);
 
 /* Helper functions for accessing (list A) when A is not expr, name nor level */
 inline bool is_nil(vm_obj const & o) { return is_simple(o); }

tests/lean/interactive/do_info.lean.expected.out

@@ -1,7 +1,7 @@
 {"msg":{"caption":"trace output","file_name":"f","pos_col":3,"pos_line":4,"severity":"information","text":"a b c : ℕ,\nh : a = b,\na_1 : c = b\n⊢ a = ?m_1\n\na b c : ℕ,\nh : a = b,\na_1 : c = b\n⊢ ?m_1 = c\n"},"response":"additional_message"}
 {"message":"file invalidated","response":"ok","seq_num":0}
-{"record":{"full-id":"tactic.intro","source":{"column":9,"file":"/library/init/meta/tactic.lean","line":521},"state":"a b c : ℕ\n⊢ a = b → c = b → a = c","type":"name → tactic expr"},"response":"ok","seq_num":6}
+{"record":{"full-id":"tactic.intro","source":{"column":9,"file":"/library/init/meta/tactic.lean","line":526},"state":"a b c : ℕ\n⊢ a = b → c = b → a = c","type":"name → tactic expr"},"response":"ok","seq_num":6}
 {"record":{"full-id":"tactic.transitivity","source":{"column":9,"file":"/library/init/meta/relation_tactics.lean","line":30},"state":"a b c : ℕ\n⊢ a = b → c = b → a = c","type":"tactic unit"},"response":"ok","seq_num":9}
-{"record":{"full-id":"tactic.assumption","source":{"column":9,"file":"/library/init/meta/tactic.lean","line":619},"state":"a b c : ℕ\n⊢ a = b → c = b → a = c","type":"tactic unit"},"response":"ok","seq_num":12}
+{"record":{"full-id":"tactic.assumption","source":{"column":9,"file":"/library/init/meta/tactic.lean","line":624},"state":"a b c : ℕ\n⊢ a = b → c = b → a = c","type":"tactic unit"},"response":"ok","seq_num":12}
 {"record":{"full-id":"tactic.symmetry","source":{"column":9,"file":"/library/init/meta/relation_tactics.lean","line":27},"state":"a b c : ℕ\n⊢ a = b → c = b → a = c","type":"tactic unit"},"response":"ok","seq_num":14}
-{"record":{"full-id":"tactic.assumption","source":{"column":9,"file":"/library/init/meta/tactic.lean","line":619},"state":"a b c : ℕ\n⊢ a = b → c = b → a = c","type":"tactic unit"},"response":"ok","seq_num":16}
+{"record":{"full-id":"tactic.assumption","source":{"column":9,"file":"/library/init/meta/tactic.lean","line":624},"state":"a b c : ℕ\n⊢ a = b → c = b → a = c","type":"tactic unit"},"response":"ok","seq_num":16}