feat(library): add tactic unfreeze_local_instances

library/init/meta/tactic.lean

@@ -522,6 +522,22 @@ meta constant set_tag (g : expr) (t : tag) : tactic unit
 /-- Return tag associated with `g`. Return `[]` if there is no tag. -/
 meta constant get_tag (g : expr) : tactic tag
 
+/-- By default, Lean only considers local instances in the header of declarations.
+    This has two main benefits.
+    1- Results produced by the type class resolution procedure can be easily cached.
+    2- The set of local instances does not have to be recomputed.
+
+    This approach has the following disadvantages:
+    1- Frozen local instances cannot be reverted.
+    2- Local instances defined inside of a declaration are not considered during type
+       class resolution.
+
+    This tactic resets the set of local instances. After executing this tactic,
+    the set of local instances will be recomputed and the cache will be frequently
+    reset. Note that, the cache is still used when executing a single tactic that
+    may generate many type class resolution problems (e.g., `simp`). -/
+meta constant unfreeze_local_instances : tactic unit
+
 meta def induction' (h : expr) (ns : list name := []) (rec : option name := none) (md := semireducible) : tactic unit :=
 induction h ns rec md >> return ()
 

src/library/tactic/smt/smt_state.cpp

@@ -172,12 +172,26 @@ static tactic_state clear_recs(tactic_state const & s) {
         return set_mctx_goals(s, mctx, cons(new_mvar, tail(s.goals())));
 }
 
+static optional<local_instance> get_last_local_instance(local_context const & lctx) {
+    if (optional<local_instances> const & lis = lctx.get_frozen_local_instances()) {
+        if (*lis)
+            return optional<local_instance>(head(*lis));
+    }
+    return optional<local_instance>();
+}
+
 static pair<tactic_state, unsigned> revert_all(tactic_state const & s) {
     lean_assert(s.goals());
     optional<metavar_decl> g = s.get_main_goal_decl();
     local_context lctx       = g->get_context();
     buffer<expr> hs;
-    lctx.for_each([&](local_decl const & d) { hs.push_back(d.mk_ref()); });
+    if (optional<local_instance> const & last_local_inst = get_last_local_instance(lctx)) {
+        /* We should not revert local instances. */
+        local_decl const & last_local_inst_decl = lctx.get_local_decl(mlocal_name(last_local_inst->get_local()));
+        lctx.for_each_after(last_local_inst_decl, [&](local_decl const & d) { hs.push_back(d.mk_ref()); });
+    } else {
+        lctx.for_each([&](local_decl const & d) { hs.push_back(d.mk_ref()); });
+    }
     bool preserve_to_revert_order = false;
     tactic_state new_s = revert(hs, s, preserve_to_revert_order);
     return mk_pair(new_s, hs.size());
@@ -400,15 +414,13 @@ tactic_state add_em_facts(tactic_state const & ts, smt_goal & g) {
 vm_obj mk_smt_state(tactic_state s, smt_config const & cfg) {
     if (!s.goals()) return mk_no_goals_exception(s);
     unsigned num_reverted;
-    /* TODO(Leo): revert-all is an anti-idiom, because we need to unfreeze_local_instances.
-       Solution: we should not revert local instances.
+    /* Remark: revert_all only reverts declarations after the last local instance.
 
        It is not reliable to implement "revert/do something/intro" idiom using `num_reverted`.
        The problem is that the `do something` step may eliminate `let`-decls.
        We have to figure out a way to do it more reliably.
     */
     std::tie(s, num_reverted) = revert_all(clear_recs(s));
-    s = unfreeze_local_instances(s);
     smt_goal new_goal(cfg);
 
     vm_obj r = preprocess(s, cfg.m_pre_config);

tests/lean/hinst_lemmas2.lean.expected.out

@@ -1,5 +1,5 @@
-{[gax3, patterns: {{f ?x_0}, {g ?x_0 ?x_0}}],
- [fax1, patterns: {{f ?x_0}, {g ?x_0 ?x_0}}],
+{[fax1, patterns: {{f ?x_0}, {g ?x_0 ?x_0}}],
+ [gax3, patterns: {{f ?x_0}, {g ?x_0 ?x_0}}],
  [gax6, patterns: {{g ?x_0 ?x_1}}],
  [gax1, patterns: {{g ?x_0 ?x_1}}],
  [gax2, patterns: {{g ?x_0 (f ?x_1)}}],

tests/lean/with_cases.lean

@@ -2,6 +2,7 @@ open tactic
 
 example (p q : Prop) [s₁ : decidable p] [s₂ : decidable q] : true :=
 begin
+  unfreeze_local_instances,
   with_cases { cases s₁; cases s₂ },
   trace_state,
   all_goals { intros, trivial }