fix(library/type_context, library/tactic/induction_tactic): fix for issue #1258 was incorrect

The fix was incorrect because it could produce an invalid local context.
Actually, the regression tests/lean/run/1258.lean was producing an
assertion violation.

src/library/tactic/clear_tactic.cpp

@@ -28,6 +28,27 @@ expr clear(metavar_context & mctx, expr const & mvar, expr const & H) {
     return new_mvar;
 }
 
+expr clear_rec_core(metavar_context & mctx, expr const & mvar) {
+    optional<metavar_decl> g   = mctx.get_metavar_decl(mvar);
+    lean_assert(g);
+    local_context lctx         = g->get_context();
+    if (optional<local_decl> d = lctx.find_if([](local_decl const & d) { return d.get_info().is_rec(); })) {
+        return clear(mctx, mvar, d->mk_ref());
+    } else {
+        return mvar;
+    }
+}
+
+expr clear_recs(metavar_context & mctx, expr const & mvar) {
+    expr curr = mvar;
+    while (true) {
+        expr next = clear_rec_core(mctx, curr);
+        if (next == curr)
+            return curr;
+        curr = next;
+    }
+}
+
 vm_obj clear(expr const & H, tactic_state const & s) {
     lean_assert(is_local(H));
     try {

src/library/tactic/clear_tactic.h

@@ -10,6 +10,9 @@ namespace lean {
 vm_obj clear(expr const & H, tactic_state const & s);
 vm_obj clear_internal(name const & n, tactic_state const & s);
 expr clear(metavar_context & mctx, expr const & mvar, expr const & H);
+/* Eliminate hypotheses that are marked as 'rec'
+   (i.e., auxiliary hypotheses generated by the equation compiler). */
+expr clear_recs(metavar_context & mctx, expr const & mvar);
 void initialize_clear_tactic();
 void finalize_clear_tactic();
 }

src/library/tactic/induction_tactic.cpp

@@ -142,11 +142,14 @@ list<expr> induction(environment const & env, options const & opts, transparency
                         << "' does not support dependent elimination, but conclusion "
                         << "depends on major premise");
     }
+    /* We should not revert auxiliary declarations added by the equation compiler.
+       See discussion at issue #1258 at github. */
+    expr mvar0 = clear_recs(mctx, mvar);
     /* Revert indices and major premise */
     buffer<expr> to_revert;
     to_revert.append(indices);
     to_revert.push_back(H);
-    expr mvar1 = revert(env, opts, mctx, mvar, to_revert);
+    expr mvar1 = revert(env, opts, mctx, mvar0, to_revert);
     lean_assert(to_revert.size() >= indices.size() + 1);
     /* Re-introduce indices and major. */
     buffer<name> indices_H;

src/library/type_context.cpp

@@ -386,11 +386,6 @@ pair<local_context, expr> type_context::revert_core(buffer<expr> & to_revert, lo
                     return;
                 }
             }
-            if (d.get_info().is_rec()) {
-                /* We should not revert auxiliary declarations added by the equation compiler.
-                   See discussion at issue #1258 at github. */
-                return;
-            }
             /* We may still need to revert d if it depends on locals already in reverted */
             if (depends_on(d, m_mctx, to_revert)) {
                 to_revert.push_back(d.mk_ref());