feat(library/tactic): add eassumption tactic, and remove redundant 'subgoals' from apply tactic

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

library/standard/tactic.lean

@@ -29,6 +29,7 @@ definition focus_at   (t : tactic) (i : num)  : tactic := builtin_tactic
 definition try_for     (t : tactic) (ms : num) : tactic := builtin_tactic
 definition now         : tactic := builtin_tactic
 definition assumption  : tactic := builtin_tactic
+definition eassumption : tactic := builtin_tactic
 definition state       : tactic := builtin_tactic
 definition fail        : tactic := builtin_tactic
 definition id          : tactic := builtin_tactic

src/library/tactic/apply_tactic.cpp

@@ -13,6 +13,7 @@ Author: Leonardo de Moura
 #include "kernel/type_checker.h"
 #include "library/kernel_bindings.h"
 #include "library/unifier.h"
+#include "library/occurs.h"
 #include "library/tactic/apply_tactic.h"
 
 namespace lean {
@@ -60,8 +61,36 @@ void collect_simple_meta(expr const & e, buffer<expr> & metas) {
         });
 }
 
-tactic apply_tactic(expr const & _e) {
-    return tactic([=](environment const & env, io_state const & ios, proof_state const & s) {
+/**
+    \brief Given a sequence metas: <tt>(?m_1 ...) (?m_2 ... ) ... (?m_k ...)</tt>,
+    we say ?m_i is "redundant" if it occurs in the type of some ?m_j.
+    This procedure removes from metas any redundant element.
+*/
+static void remove_redundant_metas(buffer<expr> & metas) {
+    buffer<expr> mvars;
+    for (expr const & m : metas)
+        mvars.push_back(get_app_fn(m));
+    unsigned k = 0;
+    for (unsigned i = 0; i < metas.size(); i++) {
+        bool found = false;
+        for (unsigned j = 0; j < metas.size(); j++) {
+            if (j != i) {
+                if (occurs(mvars[i], mlocal_type(mvars[j]))) {
+                    found = true;
+                    break;
+                }
+            }
+        }
+        if (!found) {
+            metas[k] = metas[i];
+            k++;
+        }
+    }
+    metas.shrink(k);
+}
+
+proof_state_seq apply_tactic_core(environment const & env, io_state const & ios, proof_state const & s, expr const & _e,
+                                  bool add_meta, bool add_subgoals) {
     goals const & gs = s.get_goals();
     if (empty(gs))
         return proof_state_seq();
@@ -72,6 +101,9 @@ tactic apply_tactic(expr const & _e) {
     expr  t          = g.get_type();
     expr  e          = _e;
     expr  e_t        = tc.infer(e);
+    buffer<expr> metas;
+    collect_simple_meta(e, metas);
+    if (add_meta) {
         unsigned num_t   = get_expect_num_args(tc, t);
         unsigned num_e_t = get_expect_num_args(tc, e_t);
         if (num_t > num_e_t)
@@ -81,7 +113,10 @@ tactic apply_tactic(expr const & _e) {
             expr meta  = g.mk_meta(ngen.next(), binding_domain(e_t));
             e          = mk_app(e, meta);
             e_t        = instantiate(binding_body(e_t), meta);
+            metas.push_back(meta);
         }
+    }
+    list<expr> meta_lst = to_list(metas.begin(), metas.end());
     lazy_list<substitution> substs = unify(env, t, e_t, ngen.mk_child(), s.get_subst(), get_noop_unifier_plugin(), ios.get_options());
     return map2<proof_state>(substs, [=](substitution const & subst) -> proof_state {
             name_generator new_ngen(ngen);
@@ -90,21 +125,50 @@ tactic apply_tactic(expr const & _e) {
             expr new_p = g.abstract(new_e);
             check_has_no_local(new_p, _e, "apply");
             substitution new_subst = subst.assign(g.get_name(), new_p);
-                    buffer<expr> metas;
-                    collect_simple_meta(new_e, metas);
             goals new_gs = tail_gs;
+            if (add_subgoals) {
+                buffer<expr> metas;
+                for (auto m : meta_lst) {
+                    if (!new_subst.is_assigned(get_app_fn(m)))
+                        metas.push_back(m);
+                }
+                remove_redundant_metas(metas);
                 unsigned i = metas.size();
                 while (i > 0) {
                     --i;
                     new_gs = cons(goal(metas[i], subst.instantiate(tc.infer(metas[i]))), new_gs);
                 }
+            }
             return proof_state(new_gs, new_subst, new_ngen);
         });
+}
+
+tactic apply_tactic(expr const & e) {
+    return tactic([=](environment const & env, io_state const & ios, proof_state const & s) {
+            return apply_tactic_core(env, ios, s, e, true, true);
+        });
+}
+
+tactic eassumption_tactic() {
+    return tactic([=](environment const & env, io_state const & ios, proof_state const & s) {
+            goals const & gs = s.get_goals();
+            if (empty(gs))
+                return proof_state_seq();
+            proof_state_seq r;
+            goal g = head(gs);
+            buffer<expr> hs;
+            get_app_args(g.get_meta(), hs);
+            for (expr const & h : hs) {
+                r = append(r, apply_tactic_core(env, ios, s, h, false, false));
+            }
+            return r;
         });
 }
 
 int mk_apply_tactic(lua_State * L) { return push_tactic(L, apply_tactic(to_expr(L, 1))); }
+int mk_eassumption_tactic(lua_State * L) { return push_tactic(L, eassumption_tactic()); }
 void open_apply_tactic(lua_State * L) {
     SET_GLOBAL_FUN(mk_apply_tactic,       "apply_tac");
+    SET_GLOBAL_FUN(mk_eassumption_tactic, "eassumption_tac");
 }
 }

src/library/tactic/apply_tactic.h

@@ -9,5 +9,6 @@ Author: Leonardo de Moura
 #include "library/tactic/tactic.h"
 namespace lean {
 tactic apply_tactic(expr const & e);
+tactic eassumption_tactic();
 void open_apply_tactic(lua_State * L);
 }

src/library/tactic/expr_to_tactic.cpp

@@ -145,6 +145,7 @@ register_unary_num_tac::register_unary_num_tac(name const & n, std::function<tac
 static register_simple_tac reg_id(name(g_tac, "id"), []() { return id_tactic(); });
 static register_simple_tac reg_now(name(g_tac, "now"), []() { return now_tactic(); });
 static register_simple_tac reg_assumption(name(g_tac, "assumption"), []() { return assumption_tactic(); });
+static register_simple_tac reg_eassumption(name(g_tac, "eassumption"), []() { return eassumption_tactic(); });
 static register_simple_tac reg_fail(name(g_tac, "fail"), []() { return fail_tactic(); });
 static register_simple_tac reg_beta(name(g_tac, "beta"), []() { return beta_tactic(); });
 static register_bin_tac reg_then(g_and_then_tac_name, [](tactic const & t1, tactic const & t2) { return then(t1, t2); });

tests/lean/run/tactic20.lean

@@ -0,0 +1,12 @@
+import standard
+using tactic
+
+definition assump := eassumption
+
+theorem tst {A : Type} {a b c : A} (H1 : a = b) (H2 : b = c) : a = c
+:= by apply trans; assump; assump
+
+
+
+
+

tests/lean/run/tactic21.lean

@@ -0,0 +1,17 @@
+import standard
+using tactic
+
+definition assump := eassumption
+
+theorem tst1 {A : Type} {a b c : A} {p : A → A → Bool} (H1 : p a b) (H2 : p b c) : ∃ x, p a x ∧ p x c
+:= by apply exists_intro; apply and_intro; assump; assump
+
+theorem tst2 {A : Type} {a b c d : A} {p : A → A → Bool} (Ha : p a c) (H1 : p a b) (Hb : p b d) (H2 : p b c) : ∃ x, p a x ∧ p x c
+:= by apply exists_intro; apply and_intro; assump; assump
+
+(*
+print(get_env():find("tst2"):value())
+*)
+
+
+