refactor(library/tactic): cleanup common pattern

src/kernel/metavar.cpp

@@ -16,6 +16,7 @@ Author: Leonardo de Moura
 #include "kernel/level.h"
 #include "kernel/cache_stack.h"
 #include "kernel/expr_cache.h"
+#include "kernel/abstract.h"
 
 #ifndef LEAN_INSTANTIATE_METAVARS_CACHE_CAPACITY
 #define LEAN_INSTANTIATE_METAVARS_CACHE_CAPACITY 1024*8
@@ -58,6 +59,10 @@ optional<level> substitution::get_level(name const & m) const {
     return it ? some_level(*it) : none_level();
 }
 
+void substitution::assign(expr const & mvar, buffer<expr> const & locals, expr const & v, justification const & j) {
+    assign(mlocal_name(mvar), Fun(locals, v), j);
+}
+
 void substitution::assign(name const & m, expr const & t, justification const & j) {
     lean_assert(closed(t));
     m_expr_subst.insert(m, t);

src/kernel/metavar.h

@@ -60,6 +60,9 @@ public:
     bool is_expr_assigned(name const & m) const;
     bool is_level_assigned(name const & m) const;
 
+    void assign(expr const & mvar, buffer<expr> const & locals, expr const & v, justification const & j);
+    void assign(expr const & mvar, buffer<expr> const & locals, expr const & v) { return assign(mvar, locals, v, justification()); }
+
     void assign(name const & m, expr const & t, justification const & j);
     void assign(name const & m, expr const & t) { assign(m, t, justification()); }
     void assign(expr const & m, expr const & t, justification const & j) { assign(mlocal_name(m), t, j); }

src/library/definitional/equations.cpp

@@ -925,7 +925,7 @@ class equation_compiler_fn {
                 imps_list                 = tail(imps_list);
                 rn_maps                   = tail(rn_maps);
                 expr t                    = compile_core(new_p);
-                subst.assign(new_g.get_name(), new_g.abstract(t));
+                assign(subst, new_g, t);
             }
             expr t = subst.instantiate_all(g.get_meta());
             return some_expr(t);

src/library/tactic/apply_tactic.cpp

@@ -146,9 +146,7 @@ static proof_state_seq apply_tactic_core(environment const & env, io_state const
             name_generator new_ngen(ngen);
             substitution new_subst = subst;
             expr new_e = new_subst.instantiate_all(e);
-            expr new_p = g.abstract(new_e);
+            assign(new_subst, g, new_e);
-            check_has_no_local(new_p, _e, "apply");
-            new_subst.assign(g.get_name(), new_p);
             goals new_gs = tail_gs;
             if (subgoals_action != IgnoreSubgoals) {
                 buffer<expr> metas;

src/library/tactic/assert_tactic.cpp

@@ -46,9 +46,8 @@ tactic assert_tactic(elaborate_fn const & elab, name const & id, expr const & e)
                 expr new_meta2_core = mk_app(new_mvar2, hyps);
                 expr new_meta2      = mk_app(new_meta2_core, new_local);
                 goal new_goal2(new_meta2, g.get_type());
-                expr val            = g.abstract(mk_app(new_meta2_core, new_meta1));
                 substitution new_subst = new_s.get_subst();
-                new_subst.assign(g.get_name(), val);
+                assign(new_subst, g, mk_app(new_meta2_core, new_meta1));
                 return some_proof_state(proof_state(new_s, cons(new_goal1, cons(new_goal2, tail(gs))), new_subst, ngen));
             }
             return none_proof_state();

src/library/tactic/change_tactic.cpp

@@ -32,8 +32,7 @@ tactic change_goal_tactic(elaborate_fn const & elab, expr const & e) {
                 if (tc->is_def_eq(t, *new_e, justification(), cs) && !cs) {
                     expr M   = g.mk_meta(ngen.next(), *new_e);
                     goal new_g(M, *new_e);
-                    expr val = g.abstract(M);
+                    assign(subst, g, M);
-                    subst.assign(g.get_name(), val);
                     return some(proof_state(new_s, cons(new_g, tail(gs)), subst, ngen));
                 } else {
                     // generate error

src/library/tactic/clear_tactic.cpp

@@ -30,9 +30,8 @@ tactic clear_tactic(name const & n) {
             expr new_type = g.get_type();
             expr new_meta = mk_app(mk_metavar(ngen.next(), Pi(hyps, new_type)), hyps);
             goal new_g(new_meta, new_type);
-            expr val      = g.abstract(new_meta);
             substitution new_subst = s.get_subst();
-            new_subst.assign(g.get_name(), val);
+            assign(new_subst, g, new_meta);
             proof_state new_s(s, goals(new_g, tail_gs), new_subst, ngen);
             return some_proof_state(new_s);
         } else {

src/library/tactic/exact_tactic.cpp

@@ -25,10 +25,8 @@ tactic exact_tactic(elaborate_fn const & elab, expr const & e, bool enforce_type
                                                        report_unassigned, enforce_type_during_elaboration)) {
                 goals const & gs   = new_s.get_goals();
                 goal const & g     = head(gs);
-                expr new_p         = g.abstract(*new_e);
                 substitution subst = new_s.get_subst();
-                check_has_no_local(new_p, e, "exact");
+                assign(subst, g, *new_e);
-                subst.assign(g.get_name(), new_p);
                 return some(proof_state(new_s, tail(gs), subst));
             }
             return none_proof_state();

src/library/tactic/generalize_tactic.cpp

@@ -38,7 +38,6 @@ tactic generalize_tactic(elaborate_fn const & elab, expr const & e, name const &
                     n = x;
                 expr new_t = mk_pi(n, e_t, abstract(t, *new_e));
                 expr new_m = g.mk_meta(ngen.next(), new_t);
-                expr new_v = g.abstract(mk_app(new_m, *new_e));
                 try {
                     tc->check_ignore_levels(g.abstract(new_t));
                 } catch (kernel_exception const & ex) {
@@ -52,7 +51,7 @@ tactic generalize_tactic(elaborate_fn const & elab, expr const & e, name const &
                     return none_proof_state();
                 }
 
-                subst.assign(g.get_name(), new_v);
+                assign(subst, g, mk_app(new_m, *new_e));
                 goal new_g(new_m, new_t);
                 return some(proof_state(new_s, goals(new_g, tail(gs)), subst, ngen));
             }

src/library/tactic/goal.cpp

@@ -172,6 +172,12 @@ void goal::get_hyps(buffer<expr> & r) const {
     get_app_args(m_meta, r);
 }
 
+void assign(substitution & s, goal const & g, expr const & v) {
+    buffer<expr> hyps;
+    expr const & mvar = get_app_args(g.get_meta(), hyps);
+    s.assign(mvar, hyps, v);
+}
+
 static bool uses_name(name const & n, buffer<expr> const & locals) {
     for (expr const & local : locals) {
         if (is_local(local) && local_pp_name(local) == n)

src/library/tactic/goal.h

@@ -103,6 +103,8 @@ public:
     format pp(formatter const & fmt) const;
 };
 
+void assign(substitution & s, goal const & g, expr const & v);
+
 name get_unused_name(name const & prefix, unsigned & idx, buffer<expr> const & locals);
 name get_unused_name(name const & prefix, buffer<expr> const & locals);
 name get_unused_name(name const & prefix, unsigned & idx, expr const & meta);

src/library/tactic/inversion_tactic.cpp

@@ -162,8 +162,8 @@ class inversion_tac {
         }
     }
 
-    void assign(name const & n, expr const & val) {
+    void assign(goal const & g, expr const & val) {
-        m_subst.assign(n, val);
+        ::lean::assign(m_subst, g, val);
     }
 
     /** \brief We say h has independent indices IF
@@ -286,9 +286,9 @@ class inversion_tac {
             expr new_type = Pi(eqs, g.get_type());
             expr new_meta = mk_app(mk_metavar(m_ngen.next(), Pi(hyps, new_type)), hyps);
             goal new_g(new_meta, new_type);
-            expr val      = g.abstract(mk_app(mk_app(mk_app(Fun(ts, Fun(h_new, new_meta)), m_nindices, I_args.end() - m_nindices), h),
+            expr val      = mk_app(mk_app(mk_app(Fun(ts, Fun(h_new, new_meta)), m_nindices, I_args.end() - m_nindices), h),
-                                              refls));
+                                   refls);
-            assign(g.get_name(), val);
+            assign(g, val);
             return new_g;
         } else {
             // proof relevant version
@@ -316,9 +316,9 @@ class inversion_tac {
             expr new_type = Pi(eqs, g.get_type());
             expr new_meta = mk_app(mk_metavar(m_ngen.next(), Pi(hyps, new_type)), hyps);
             goal new_g(new_meta, new_type);
-            expr val      = g.abstract(mk_app(mk_app(mk_app(Fun(ts, Fun(h_new, new_meta)), m_nindices, I_args.end() - m_nindices), h),
+            expr val      = mk_app(mk_app(mk_app(Fun(ts, Fun(h_new, new_meta)), m_nindices, I_args.end() - m_nindices), h),
-                                              refls));
+                                   refls);
-            assign(g.get_name(), val);
+            assign(g, val);
             return new_g;
         }
     }
@@ -340,8 +340,8 @@ class inversion_tac {
         expr new_type = Pi(deps, g.get_type());
         expr new_meta = mk_app(mk_metavar(m_ngen.next(), Pi(new_hyps, new_type)), new_hyps);
         goal new_g(new_meta, new_type);
-        expr val      = g.abstract(mk_app(new_meta, deps));
+        expr val      = mk_app(new_meta, deps);
-        assign(g.get_name(), val);
+        assign(g, val);
         return new_g;
     }
 
@@ -420,8 +420,7 @@ class inversion_tac {
             name const & intro_name = intro_names[i];
             new_imps.push_back(filter(imps, [&](implementation_ptr const & imp) { return imp->get_constructor_name() == intro_name; }));
         }
-        expr val        = g.abstract(cases_on);
+        assign(g, cases_on);
-        assign(g.get_name(), val);
         return mk_pair(to_list(new_goals), to_list(new_imps));
     }
 
@@ -484,8 +483,8 @@ class inversion_tac {
             expr new_meta = mk_app(mk_metavar(m_ngen.next(), Pi(new_hyps, g_type)), new_hyps);
             goal new_g(new_meta, g_type);
             new_gs.push_back(new_g);
-            expr val      = g.abstract(Fun(nargs, new_hyps.end() - nargs, new_meta));
+            expr val      = Fun(nargs, new_hyps.end() - nargs, new_meta);
-            assign(g.get_name(), val);
+            assign(g, val);
             gs = tail(gs);
         }
         return mk_pair(to_list(new_gs), to_list(new_args));
@@ -566,8 +565,8 @@ class inversion_tac {
         // aux_eq : a = eq.rec A s C a s p
         expr trans_eq    = mk_app({mk_constant(get_eq_trans_name(), {lvl}), A, reduced_lhs, lhs, rhs, *aux_eq, old_eq});
         // trans_eq : a = b
-        expr val         = g.abstract(Fun(old_eq, mk_app(new_meta, trans_eq)));
+        expr val         = Fun(old_eq, mk_app(new_meta, trans_eq));
-        assign(g.get_name(), val);
+        assign(g, val);
         return intro_next_eq(new_g);
     }
 
@@ -598,8 +597,8 @@ class inversion_tac {
             hyps.pop_back();
             expr H        = mk_local(m_ngen.next(), g.get_unused_name(binding_name(type)), binding_domain(type), binder_info());
             expr to_eq    = mk_app(mk_constant(get_heq_to_eq_name(), const_levels(heq_fn)), args[0], args[1], args[3], H);
-            expr val      = g.abstract(Fun(H, mk_app(mk_app(new_mvar, hyps), to_eq)));
+            expr val      = Fun(H, mk_app(mk_app(new_mvar, hyps), to_eq));
-            assign(g.get_name(), val);
+            assign(g, val);
             return new_g;
         } else {
             if (m_throw_tactic_exception) {
@@ -626,8 +625,8 @@ class inversion_tac {
         hyps.push_back(new_hyp);
         expr new_meta = mk_app(mk_metavar(m_ngen.next(), Pi(hyps, new_type)), hyps);
         goal new_g(new_meta, new_type);
-        expr val      = g.abstract(Fun(new_hyp, new_meta));
+        expr val      = Fun(new_hyp, new_meta);
-        assign(g.get_name(), val);
+        assign(g, val);
         return new_g;
     }
 
@@ -722,8 +721,7 @@ class inversion_tac {
             expr new_type = g.get_type();
             expr new_meta = mk_app(mk_metavar(m_ngen.next(), Pi(hyps, new_type)), hyps);
             goal new_g(new_meta, new_type);
-            expr val      = g.abstract(new_meta);
+            assign(g, new_meta);
-            assign(g.get_name(), val);
             return unify_eqs(new_g, neqs-1);
         }
         buffer<expr> lhs_args, rhs_args;
@@ -755,15 +753,15 @@ class inversion_tac {
                 expr new_mvar = mk_metavar(m_ngen.next(), Pi(hyps, new_type));
                 expr new_meta = mk_app(new_mvar, hyps);
                 goal new_g(new_meta, new_type);
-                expr val      = g.abstract(lift_down(mk_app(no_confusion, new_meta)));
+                expr val      = lift_down(mk_app(no_confusion, new_meta));
-                assign(g.get_name(), val);
+                assign(g, val);
                 unsigned A_nparams = *inductive::get_num_params(m_env, const_name(A_fn));
                 lean_assert(lhs_args.size() >= A_nparams);
                 return unify_eqs(new_g, neqs - 1 + lhs_args.size() - A_nparams);
             } else {
                 // conflict transition, eq is of the form c_1 ... = c_2 ..., where c_1 and c_2 are different constructors/intro rules.
-                expr val      = g.abstract(lift_down(no_confusion));
+                expr val      = lift_down(no_confusion);
-                assign(g.get_name(), val);
+                assign(g, val);
                 return optional<goal>(); // goal has been solved
             }
         }
@@ -798,8 +796,7 @@ class inversion_tac {
                 expr new_mvar           = mk_metavar(m_ngen.next(), Pi(new_hyps, new_type));
                 expr new_meta           = mk_app(new_mvar, new_hyps);
                 goal new_g(new_meta, new_type);
-                expr val                = g.abstract(new_meta);
+                assign(g, new_meta);
-                assign(g.get_name(), val);
                 return unify_eqs(new_g, neqs-1);
             } else {
                 expr deps_g_type    = Pi(deps, g_type);
@@ -837,8 +834,8 @@ class inversion_tac {
                 goal new_g(new_meta, new_type);
                 expr eq_rec_minor   = mk_app(new_mvar, non_deps);
                 eq_rec              = mk_app(eq_rec, eq_rec_minor, rhs, eq);
-                expr val            = g.abstract(mk_app(eq_rec, deps));
+                expr val            = mk_app(eq_rec, deps);
-                assign(g.get_name(), val);
+                assign(g, val);
                 return unify_eqs(new_g, neqs-1);
             }
         } else if (is_local(lhs)) {
@@ -853,8 +850,8 @@ class inversion_tac {
             level eq_symm_lvl = sort_level(m_tc.ensure_type(A).first);
             expr symm_pr  = mk_constant(get_eq_symm_name(), {eq_symm_lvl});
             symm_pr       = mk_app(symm_pr, A, lhs, rhs, eq);
-            expr val      = g.abstract(mk_app(new_meta, symm_pr));
+            expr val      = mk_app(new_meta, symm_pr);
-            assign(g.get_name(), val);
+            assign(g, val);
             return unify_eqs(new_g, neqs);
         }
         if (m_throw_tactic_exception) {
@@ -912,8 +909,8 @@ class inversion_tac {
         expr new_meta  = mk_app(mk_metavar(m_ngen.next(), Pi(new_hyps, g_type)), new_hyps);
         goal new_g(new_meta, g_type);
         unsigned ndeps = deps.size();
-        expr val       = g.abstract(Fun(ndeps, new_hyps.end() - ndeps, new_meta));
+        expr val       = Fun(ndeps, new_hyps.end() - ndeps, new_meta);
-        assign(g.get_name(), val);
+        assign(g, val);
         return mk_pair(new_g, rs);
     }
 
@@ -941,8 +938,7 @@ class inversion_tac {
             expr new_type = g.get_type();
             expr new_meta = mk_app(mk_metavar(m_ngen.next(), Pi(hyps, new_type)), hyps);
             goal new_g(new_meta, new_type);
-            expr val      = g.abstract(new_meta);
+            assign(g, new_meta);
-            assign(g.get_name(), val);
             return new_g;
         } else {
             return g;

src/library/tactic/revert_tactic.cpp

@@ -35,9 +35,8 @@ tactic revert_tactic(name const & n) {
             expr new_type = Pi(h, g.get_type());
             expr new_meta = mk_app(mk_metavar(ngen.next(), Pi(hyps, new_type)), hyps);
             goal new_g(new_meta, new_type);
-            expr val      = g.abstract(mk_app(new_meta, h));
             substitution new_subst = s.get_subst();
-            new_subst.assign(g.get_name(), val);
+            assign(new_subst, g, mk_app(new_meta, h));
             proof_state new_s(s, goals(new_g, tail_gs), new_subst, ngen);
             return some_proof_state(new_s);
         } else {

src/library/tactic/rewrite_tactic.cpp

@@ -511,8 +511,7 @@ class rewrite_fn {
     void replace_goal(expr const & new_type) {
         expr M = m_g.mk_meta(m_ngen.next(), new_type);
         goal new_g(M, new_type);
-        expr val = m_g.abstract(M);
+        assign(m_subst, m_g, M);
-        m_subst.assign(m_g.get_name(), val);
         update_goal(new_g);
     }
 
@@ -540,8 +539,7 @@ class rewrite_fn {
         expr new_mvar = mk_metavar(m_ngen.next(), Pi(new_hyps, new_type));
         expr new_meta = mk_app(new_mvar, new_hyps);
         goal new_g(new_meta, new_type);
-        expr val      = m_g.abstract(new_meta);
+        assign(m_subst, m_g, new_meta);
-        m_subst.assign(m_g.get_name(), val);
         update_goal(new_g);
     }
 
@@ -968,8 +966,7 @@ class rewrite_fn {
             expr new_mvar = mk_metavar(m_ngen.next(), Pi(new_hyps, new_type));
             expr new_meta = mk_app(new_mvar, new_hyps);
             goal new_g(new_meta, new_type);
-            expr val      = m_g.abstract(mk_app(new_mvar, args));
+            assign(m_subst, m_g, mk_app(new_mvar, args));
-            m_subst.assign(m_g.get_name(), val);
             update_goal(new_g);
             return true;
         }
@@ -1003,8 +1000,7 @@ class rewrite_fn {
             }
 
             goal new_g(M, Pb);
-            expr val = m_g.abstract(H);
+            assign(m_subst, m_g, H);
-            m_subst.assign(m_g.get_name(), val);
             update_goal(new_g);
             // regular(m_env, m_ios) << "FOUND\n" << a << "\n==>\n" << b << "\nWITH\n" << Heq << "\n";
             // regular(m_env, m_ios) << H << "\n";
@@ -1116,13 +1112,13 @@ class rewrite_fn {
             expr rhs = app_arg(type);
             if (m_unifier_tc->is_def_eq(lhs, rhs, justification(), cs) && !cs) {
                 expr H = is_eq(type) ? mk_refl(*m_tc, lhs) : mk_iff_refl(lhs);
-                m_subst.assign(m_g.get_name(), m_g.abstract(H));
+                assign(m_subst, m_g, H);
                 return true;
             } else {
                 return false;
             }
         } else if (type == mk_true()) {
-            m_subst.assign(m_g.get_name(), mk_constant(get_eq_intro_name()));
+            assign(m_subst, m_g, mk_constant(get_eq_intro_name()));
             return true;
         } else {
             return false;

src/library/tactic/tactic.cpp

@@ -227,16 +227,16 @@ tactic assumption_tactic() {
             goals new_gs = map_goals(s, [&](goal const & g) -> optional<goal> {
                     expr const & t  = g.get_type();
                     optional<expr> h;
-                    buffer<expr> locals;
+                    buffer<expr> hyps;
-                    get_app_args(g.get_meta(), locals);
+                    g.get_hyps(hyps);
-                    for (auto const & l : locals) {
+                    for (auto const & l : hyps) {
                         if (mlocal_type(l) == t) {
                             h = l;
                             break;
                         }
                     }
                     if (h) {
-                        subst.assign(g.get_mvar(), g.abstract(*h), justification());
+                        assign(subst, g, *h);
                         solved = true;
                         return optional<goal>();
                     } else {