fix(library/type_context): issue #1258 again

This is yet another fix.

src/library/tactic/induction_tactic.cpp

@@ -142,14 +142,11 @@ 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, mvar0, to_revert);
+    expr mvar1 = revert(env, opts, mctx, mvar, to_revert);
     lean_assert(to_revert.size() >= indices.size() + 1);
     /* Re-introduce indices and major. */
     buffer<name> indices_H;

src/library/type_context.cpp

@@ -378,6 +378,7 @@ pair<local_context, expr> type_context::revert_core(buffer<expr> & to_revert, lo
     }
     local_decl d0  = *ctx.get_local_decl(to_revert[0]);
     unsigned next_idx = 1;
+    unsigned init_sz  = to_revert.size();
     ctx.for_each_after(d0, [&](local_decl const & d) {
             /* Check if d is in initial to_revert */
             for (unsigned i = next_idx; i < num; i++) {
@@ -388,6 +389,23 @@ 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, m_mctx, to_revert)) {
+                if (d.get_info().is_rec()) {
+                    /* We should not revert auxiliary declarations added by the equation compiler.
+                       See discussion at issue #1258 at github. */
+                    sstream out;
+                    out << "failed to revert ";
+                    for (unsigned i = 0; i < init_sz; i++) {
+                        if (i > 0) out << " ";
+                        out << "'" << to_revert[i] << "'";
+                    }
+                    out << ", '" << d.get_pp_name() << "' "
+                        << "depends on " << (init_sz == 1 ? "it" : "them")
+                        << ", and '" << d.get_pp_name() << "' is an auxiliary declaration "
+                        << "introduced by the equation compiler (possible solution: "
+                        << "use tactic 'clear' to remove '" << d.get_pp_name() << "' "
+                        << "from the local context)\n";
+                    throw exception(out);
+                }
                 to_revert.push_back(d.mk_ref());
             }
         });

tests/lean/1258.lean

@@ -0,0 +1,4 @@
+constant P : list ℕ → list ℕ → Prop
+lemma foo (xs : list ℕ) : Π (ns : list ℕ), P xs ns
+| []      := sorry
+| (n::ns) := begin cases xs, exact sorry, exact sorry end

tests/lean/1258.lean.expected.out

@@ -0,0 +1,8 @@
+1258.lean:4:19: error: failed to revert 'xs', 'foo' depends on it, and 'foo' is an auxiliary declaration introduced by the equation compiler (possible solution: use tactic 'clear' to remove 'foo' from the local context)
+
+state:
+xs : list ℕ,
+foo : ∀ (ns : list ℕ), P xs ns,
+n : ℕ,
+ns : list ℕ
+⊢ P xs (n :: ns)

tests/lean/run/1258.lean

@@ -1,4 +1,4 @@
 constant P : list ℕ → list ℕ → Prop
 lemma foo (xs : list ℕ) : Π (ns : list ℕ), P xs ns
 | []      := sorry
-| (n::ns) := begin cases xs, exact sorry, exact sorry end
+| (n::ns) := begin clear foo, cases xs, exact sorry, exact sorry end

tests/lean/run/rec_and_tac_issue.lean

@@ -0,0 +1,5 @@
+open nat
+
+def f : ℕ → ℕ → ℕ
+| 0        b := 0
+| (succ n) b := begin cases b with b', exact 0, exact f n b' end