From 60d32555772e38b2e61520fd026e6a915cb7cebe Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 22 Dec 2016 10:51:16 -0800 Subject: [PATCH] fix(library/type_context): issue #1258 again This is yet another fix. --- src/library/tactic/induction_tactic.cpp | 5 +---- src/library/type_context.cpp | 18 ++++++++++++++++++ tests/lean/1258.lean | 4 ++++ tests/lean/1258.lean.expected.out | 8 ++++++++ tests/lean/run/1258.lean | 2 +- tests/lean/run/rec_and_tac_issue.lean | 5 +++++ 6 files changed, 37 insertions(+), 5 deletions(-) create mode 100644 tests/lean/1258.lean create mode 100644 tests/lean/1258.lean.expected.out create mode 100644 tests/lean/run/rec_and_tac_issue.lean diff --git a/src/library/tactic/induction_tactic.cpp b/src/library/tactic/induction_tactic.cpp index 02d9e4de9d..d5ce706a6c 100644 --- a/src/library/tactic/induction_tactic.cpp +++ b/src/library/tactic/induction_tactic.cpp @@ -142,14 +142,11 @@ list 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 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 indices_H; diff --git a/src/library/type_context.cpp b/src/library/type_context.cpp index 5b4a416726..f493f433ce 100644 --- a/src/library/type_context.cpp +++ b/src/library/type_context.cpp @@ -378,6 +378,7 @@ pair type_context::revert_core(buffer & 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 type_context::revert_core(buffer & 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()); } }); diff --git a/tests/lean/1258.lean b/tests/lean/1258.lean new file mode 100644 index 0000000000..6e785b9eaa --- /dev/null +++ b/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 diff --git a/tests/lean/1258.lean.expected.out b/tests/lean/1258.lean.expected.out new file mode 100644 index 0000000000..65a2f864c2 --- /dev/null +++ b/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) diff --git a/tests/lean/run/1258.lean b/tests/lean/run/1258.lean index 6e785b9eaa..add8dceff4 100644 --- a/tests/lean/run/1258.lean +++ b/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 diff --git a/tests/lean/run/rec_and_tac_issue.lean b/tests/lean/run/rec_and_tac_issue.lean new file mode 100644 index 0000000000..18114fa83b --- /dev/null +++ b/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