fix(library/local_context): depends_on should take into account assigned metavariables

src/library/local_context.cpp

@@ -10,6 +10,7 @@ Author: Leonardo de Moura
 #include "library/pp_options.h"
 #include "library/local_context.h"
 #include "library/metavar_context.h"
+#include "library/trace.h"
 
 namespace lean {
 static name *       g_local_prefix;
@@ -49,39 +50,58 @@ expr local_decl::mk_ref() const {
     return mk_local_ref(m_ptr->m_name, m_ptr->m_pp_name, m_ptr->m_bi);
 }
 
-bool depends_on(expr const & e, unsigned num, expr const * locals) {
+static bool depends_on_core(expr const & e, metavar_context const & mctx, unsigned num, expr const * locals,
+                            name_set & visited_mvars) {
     lean_assert(std::all_of(locals, locals+num, is_local_decl_ref));
-    if (!has_local(e))
+    if (!has_local(e) && !has_expr_metavar(e))
         return false;
     bool found = false;
     for_each(e, [&](expr const & e, unsigned) {
             if (found) return false;
-            if (!has_local(e)) return false;
+            if (!has_local(e) && !has_expr_metavar(e)) return false;
             if (is_local_decl_ref(e) &&
                 std::any_of(locals, locals+num,
                             [&](expr const & l) { return mlocal_name(e) == mlocal_name(l); })) {
                 found = true;
                 return false;
             }
+            if (is_metavar_decl_ref(e)) {
+                if (auto v = mctx.get_assignment(e)) {
+                    if (!visited_mvars.contains(mlocal_name(e))) {
+                        visited_mvars.insert(mlocal_name(e));
+                        if (depends_on_core(*v, mctx, num, locals, visited_mvars)) {
+                            found = true;
+                            return false;
+                        }
+                    }
+                }
+            }
             return true;
         });
     return found;
 }
 
-bool depends_on(local_decl const & d, unsigned num, expr const * locals) {
-    if (depends_on(d.get_type(), num, locals))
+bool depends_on(expr const & e, metavar_context const & mctx, unsigned num, expr const * locals) {
+    name_set visited_mvars;
+    return depends_on_core(e, mctx, num, locals, visited_mvars);
+}
+
+bool depends_on(local_decl const & d, metavar_context const & mctx, unsigned num, expr const * locals) {
+    name_set visited_mvars;
+    if (depends_on_core(d.get_type(), mctx, num, locals, visited_mvars))
         return true;
-    if (auto v = d.get_value())
-        return depends_on(*v, num, locals);
+    if (auto v = d.get_value()) {
+        return depends_on_core(*v, mctx, num, locals, visited_mvars);
+    }
     return false;
 }
 
-bool depends_on(expr const & e, buffer<expr> const & locals) {
-    return depends_on(e, locals.size(), locals.data());
+bool depends_on(expr const & e, metavar_context const & mctx, buffer<expr> const & locals) {
+    return depends_on(e, mctx, locals.size(), locals.data());
 }
 
-bool depends_on(local_decl const & d, buffer<expr> const & locals) {
-    return depends_on(d, locals.size(), locals.data());
+bool depends_on(local_decl const & d, metavar_context const & mctx, buffer<expr> const & locals) {
+    return depends_on(d, mctx, locals.size(), locals.data());
 }
 
 expr local_context::mk_local_decl(name const & n, name const & ppn, expr const & type, optional<expr> const & value, binder_info const & bi) {
@@ -167,13 +187,13 @@ bool local_context::rename_user_name(name const & from, name const & to) {
     }
 }
 
-optional<local_decl> local_context::has_dependencies(local_decl const & d) const {
+optional<local_decl> local_context::has_dependencies(local_decl const & d, metavar_context const & mctx) const {
     lean_assert(get_local_decl(d.get_name()));
     expr l = d.mk_ref();
     optional<local_decl> r;
     for_each_after(d, [&](local_decl const & d2) {
             if (r) return;
-            if (depends_on(d2, 1, &l))
+            if (depends_on(d2, mctx, 1, &l))
                 r = d2;
         });
     return r;
@@ -181,7 +201,6 @@ optional<local_decl> local_context::has_dependencies(local_decl const & d) const
 
 void local_context::clear(local_decl const & d) {
     lean_assert(get_local_decl(d.get_name()));
-    lean_assert(!has_dependencies(d));
     m_idx2local_decl.erase(d.get_idx());
     m_name2local_decl.erase(d.get_name());
 }

src/library/local_context.h

@@ -57,10 +57,12 @@ public:
 
 bool is_local_decl_ref(expr const & e);
 
-bool depends_on(expr const & e, unsigned num, expr const * locals);
-bool depends_on(local_decl const & d, unsigned num, expr const * locals);
-bool depends_on(expr const & e, buffer<expr> const & locals);
-bool depends_on(local_decl const & d, buffer<expr> const & locals);
+class metavar_context;
+
+bool depends_on(expr const & e, metavar_context const & mctx, unsigned num, expr const * locals);
+bool depends_on(local_decl const & d, metavar_context const & mctx,  unsigned num, expr const * locals);
+bool depends_on(expr const & e, metavar_context const & mctx,  buffer<expr> const & locals);
+bool depends_on(local_decl const & d, metavar_context const & mctx, buffer<expr> const & locals);
 
 class metavar_context;
 
@@ -106,7 +108,7 @@ public:
     /** \brief Return a non-none iff other local decls depends on \c d. If the result is not none,
         then it is the name of the local decl that depends on d.
         \pre \c d is in this local context. */
-    optional<local_decl> has_dependencies(local_decl const & d) const;
+    optional<local_decl> has_dependencies(local_decl const & d, metavar_context const & mctx) const;
 
     /** \brief Return an unused hypothesis "user name" with the given prefix, the suffix is an
         unsigned >= idx. */

src/library/tactic/cases_tactic.cpp

@@ -138,7 +138,7 @@ struct cases_tactic_fn {
         lctx.for_each_after(*h_decl, [&](local_decl const & h1) {
                 if (!ok) return;
                 /* h1 must not depend on the indices */
-                if (depends_on(h1, m_nindices, args.end() - m_nindices))
+                if (depends_on(h1, m_mctx, m_nindices, args.end() - m_nindices))
                     ok = false;
             });
         return ok;

src/library/tactic/clear_tactic.cpp

@@ -18,9 +18,9 @@ expr clear(metavar_context & mctx, expr const & mvar, expr const & H) {
     optional<local_decl> d     = lctx.get_local_decl(H);
     if (!d)
         throw exception(sstream() << "clear tactic failed, unknown '" << local_pp_name(H) << "' hypothesis");
-    if (depends_on(g->get_type(), 1, &H))
+    if (depends_on(g->get_type(), mctx, 1, &H))
         throw exception(sstream() << "clear tactic failed, target type depends on '" << local_pp_name(H) << "'");
-    if (optional<local_decl> d2 = lctx.has_dependencies(*d))
+    if (optional<local_decl> d2 = lctx.has_dependencies(*d, mctx))
         throw exception(sstream() << "clear tactic failed, hypothesis '" << d2->get_pp_name() << "' depends on '" << local_pp_name(H) << "'");
     lctx.clear(*d);
     expr new_mvar              = mctx.mk_metavar_decl(lctx, g->get_type());

src/library/tactic/revert_tactic.cpp

@@ -35,7 +35,8 @@ vm_obj revert(list<expr> const & ls, tactic_state const & s) {
         if (lctx.get_local_decl(l)) {
             locals.push_back(l);
         } else {
-            return mk_tactic_exception(sstream() << "revert tactic failed, unknown '" << local_pp_name(l) << "' hypothesis", s);
+            return mk_tactic_exception(sstream() << "revert tactic failed, unknown '"
+                                       << local_pp_name(l) << "' hypothesis", s);
         }
     }
     tactic_state new_s = revert(locals, s);

src/library/type_context.cpp

@@ -267,7 +267,7 @@ pair<local_context, expr> type_context::revert_core(buffer<expr> & to_revert, lo
                 }
             }
             /* We may still need to revert d if it depends on locals already in reverted */
-            if (depends_on(d, to_revert)) {
+            if (depends_on(d, m_mctx, to_revert)) {
                 to_revert.push_back(d.mk_ref());
             }
         });
@@ -320,13 +320,13 @@ expr type_context::mk_binding(bool is_pi, unsigned num_locals, expr const * loca
     for (unsigned i = 0; i < num_locals; i++) {
         local_decl const & decl = *m_lctx.get_local_decl(locals[i]);
         decls.push_back(decl);
-        types.push_back(abstract_locals(decl.get_type(), i, locals));
+        types.push_back(abstract_locals(instantiate_mvars(decl.get_type()), i, locals));
         if (auto v = decl.get_value())
-            values.push_back(some_expr(abstract_locals(*v, i, locals)));
+            values.push_back(some_expr(abstract_locals(instantiate_mvars(*v), i, locals)));
         else
             values.push_back(none_expr());
     }
-    expr new_e = abstract_locals(e, num_locals, locals);
+    expr new_e = abstract_locals(instantiate_mvars(e), num_locals, locals);
     lean_assert(types.size() == values.size());
     unsigned i = types.size();
     while (i > 0) {

tests/lean/dep_bug.lean

@@ -0,0 +1,16 @@
+open tactic
+
+
+
+example (a b c : nat) (H : c = b) : a + c = a + b :=
+by do
+  N ← to_expr `(nat),
+  define `v N,
+  trace_state,
+  trace  "------------",
+  to_expr `(a + b) >>= exact,
+  trace_state,
+  trace "------------",
+  get_local `H >>= subst,
+  trace_state,
+  to_expr `(eq.refl v) >>= exact

tests/lean/dep_bug.lean.expected.out

@@ -0,0 +1,17 @@
+a b c : ℕ,
+H : c = b
+⊢ ℕ
+
+a b c : ℕ,
+H : c = b,
+v : ℕ := ?m_1
+⊢ a + c = a + b
+------------
+a b c : ℕ,
+H : c = b,
+v : ℕ := a + b
+⊢ a + c = a + b
+------------
+a c : ℕ,
+v : ℕ := a + c
+⊢ a + c = a + c

tests/lean/focus_tac.lean.expected.out

@@ -27,5 +27,5 @@ a : ℕ
 ⊢ ℕ
 ---- after focus tac ----
 a : ℕ,
-x : ℕ := ?m_1
+x : ℕ := a
 ⊢ a = a