From c1ecaf4edd011dbd3035b1fef1e2734ce103243e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 12 Jan 2017 21:49:17 -0800 Subject: [PATCH] feat(library/tactic/smt/smt_state): do not apply intros automatically in `begin[smt]...end` blocks --- src/library/tactic/smt/smt_state.cpp | 42 +++++++++++++++++++--------- tests/lean/run/blast_unit2.lean | 2 +- tests/lean/run/heap.lean | 1 + tests/lean/run/listex2.lean | 1 + tests/lean/run/smt_ematch2.lean | 2 +- tests/lean/smt_begin_end1.lean | 3 ++ 6 files changed, 36 insertions(+), 15 deletions(-) diff --git a/src/library/tactic/smt/smt_state.cpp b/src/library/tactic/smt/smt_state.cpp index 2ade3b8a11..c9377ca1f9 100644 --- a/src/library/tactic/smt/smt_state.cpp +++ b/src/library/tactic/smt/smt_state.cpp @@ -152,7 +152,7 @@ vm_obj mk_smt_tactic_success(vm_obj const & ss, tactic_state const & ts) { Reason: ematching will close the goal by instantiating them. Then later, the equation compiler will fail to eliminate this application using structural or well founded induction. */ -tactic_state clear_recs(tactic_state const & s) { +static tactic_state clear_recs(tactic_state const & s) { lean_assert(s.goals()); expr mvar = head(s.goals()); metavar_context mctx = s.mctx(); @@ -163,13 +163,14 @@ tactic_state clear_recs(tactic_state const & s) { return set_mctx_goals(s, mctx, cons(new_mvar, tail(s.goals()))); } -tactic_state revert_all(tactic_state const & s) { +static pair revert_all(tactic_state const & s) { lean_assert(s.goals()); optional g = s.get_main_goal_decl(); local_context lctx = g->get_context(); buffer hs; lctx.for_each([&](local_decl const & d) { hs.push_back(d.mk_ref()); }); - return revert(hs, s); + tactic_state new_s = revert(hs, s); + return mk_pair(new_s, hs.size()); } static dsimplify_fn mk_dsimp(type_context & ctx, defeq_can_state & dcs, smt_pre_config const & cfg) { @@ -255,8 +256,21 @@ static expr_pair preprocess_forward(type_context & ctx, defeq_can_state & dcs, s return preprocess_forward(ctx, dcs, g.get_pre_config(), type, h); } -expr intros(environment const & env, options const & opts, metavar_context & mctx, expr const & mvar, - defeq_can_state & dcs, smt_goal & s_goal, bool use_unused_names) { +static name mk_intro_name(type_context & ctx, name const & bname, bool use_unused_names, list & user_ids) { + if (user_ids) { + name r = head(user_ids); + user_ids = tail(user_ids); + return r; + } else if (use_unused_names) { + return ctx.get_unused_name(bname); + } else { + return bname; + } +} + +static expr intros(environment const & env, options const & opts, metavar_context & mctx, expr const & mvar, + defeq_can_state & dcs, smt_goal & s_goal, bool use_unused_names, + optional const & num, list ids) { optional decl = mctx.get_metavar_decl(mvar); lean_assert(decl); type_context ctx(env, opts, mctx, decl->get_context(), transparency_mode::Semireducible); @@ -272,7 +286,7 @@ expr intros(environment const & env, options const & opts, metavar_context & mct type_context::tmp_locals locals(ctx); buffer new_Hs; buffer to_inst; - while (true) { + for (unsigned i = 0; !num || i < *num; i++) { if (!is_pi(target) && !is_let(target)) { target = instantiate_rev(target, to_inst.size(), to_inst.data()); to_inst.clear(); @@ -280,8 +294,7 @@ expr intros(environment const & env, options const & opts, metavar_context & mct } if (is_pi(target)) { expr type = dsimp(instantiate_rev(binding_domain(target), to_inst.size(), to_inst.data())); - name n = binding_name(target); - if (use_unused_names) n = ctx.get_unused_name(n); + name n = mk_intro_name(ctx, binding_name(target), use_unused_names, ids); expr h = locals.push_local(n, type); to_inst.push_back(h); new_Hs.push_back(h); @@ -293,8 +306,7 @@ expr intros(environment const & env, options const & opts, metavar_context & mct } else if (is_let(target)) { expr type = dsimp(instantiate_rev(let_type(target), to_inst.size(), to_inst.data())); expr value = dsimp(instantiate_rev(let_value(target), to_inst.size(), to_inst.data())); - name n = let_name(target); - if (use_unused_names) n = ctx.get_unused_name(n); + name n = mk_intro_name(ctx, let_name(target), use_unused_names, ids); expr h = locals.push_let(n, type, value); to_inst.push_back(h); new_Hs.push_back(h); @@ -360,7 +372,8 @@ 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); - s = revert_all(clear_recs(s)); + unsigned num_reverted; + std::tie(s, num_reverted) = revert_all(clear_recs(s)); smt_goal new_goal(cfg); @@ -371,7 +384,9 @@ vm_obj mk_smt_state(tactic_state s, smt_config const & cfg) { metavar_context mctx = s.mctx(); bool use_unused_names = true; defeq_can_state dcs = s.dcs(); - expr new_M = intros(s.env(), s.get_options(), mctx, head(s.goals()), dcs, new_goal, use_unused_names); + list ids; + expr new_M = intros(s.env(), s.get_options(), mctx, head(s.goals()), dcs, new_goal, use_unused_names, + optional(num_reverted), ids); s = set_mctx_goals_dcs(s, mctx, cons(new_M, tail(s.goals())), dcs); s = add_em_facts(s, new_goal); @@ -719,8 +734,9 @@ vm_obj smt_tactic_intros_core(vm_obj const & use_unused_names, vm_obj const & ss metavar_context mctx = ts.mctx(); defeq_can_state dcs = ts.dcs(); + list ids; expr new_mvar = intros(ts.env(), ts.get_options(), mctx, head(ts.goals()), - dcs, new_sgoal, to_bool(use_unused_names)); + dcs, new_sgoal, to_bool(use_unused_names), optional(), ids); tactic_state new_ts = set_mctx_goals_dcs(ts, mctx, cons(new_mvar, tail(ts.goals())), dcs); vm_obj new_ss = mk_vm_cons(to_obj(new_sgoal), tail(ss)); diff --git a/tests/lean/run/blast_unit2.lean b/tests/lean/run/blast_unit2.lean index ed9aa915cb..779cb333f7 100644 --- a/tests/lean/run/blast_unit2.lean +++ b/tests/lean/run/blast_unit2.lean @@ -1,7 +1,7 @@ variables {A₁ A₂ A₃ A₄ B₁ B₂ B₃ B₄ : Prop} meta def blast : tactic unit := -using_smt $ return () +using_smt $ smt_tactic.intros >> return () constants (a b c d e : nat) constants (p : nat → Prop) diff --git a/tests/lean/run/heap.lean b/tests/lean/run/heap.lean index 86f700bceb..25a6d10d06 100644 --- a/tests/lean/run/heap.lean +++ b/tests/lean/run/heap.lean @@ -26,6 +26,7 @@ lemma ex (hnoalias : ∀ h y₁ y₂ w₁ w₂, is_def (h ∙ y₁ ↣ w₁ ∙ y₂ ↣ w₂) → y₁ ≠ y₂) : is_def (h₁ ∙ (x₁ ↣ v₁ ∙ x₂ ↣ v₂) ∙ h₂ ∙ (x₃ ↣ v₃)) → x₁ ≠ x₃ ∧ x₁ ≠ x₂ ∧ x₂ ≠ x₃ := begin [smt] + intros, smt_tactic.add_lemmas_from_facts, repeat {ematch} end diff --git a/tests/lean/run/listex2.lean b/tests/lean/run/listex2.lean index d1aae92d64..aa3cebd9be 100644 --- a/tests/lean/run/listex2.lean +++ b/tests/lean/run/listex2.lean @@ -59,6 +59,7 @@ set_option trace.smt.ematch true /- Using ematching -/ lemma ex (a b c : nat) (l₁ l₂ : list nat) : a ∈ l₁ → a ∈ b::b::c::l₂ ++ b::c::l₁ ++ [c, c, b] := begin [smt] + intros, add_lemma [in_left, in_right, in_head, in_tail], repeat {ematch} -- It will loop if there is a matching loop end diff --git a/tests/lean/run/smt_ematch2.lean b/tests/lean/run/smt_ematch2.lean index 3bbf8ac505..f7d6e3fb0c 100644 --- a/tests/lean/run/smt_ematch2.lean +++ b/tests/lean/run/smt_ematch2.lean @@ -7,7 +7,7 @@ meta def no_ac : smt_config := { default_smt_config with cc_cfg := { default_cc_config with ac := ff }} meta def blast : tactic unit := -using_smt_core no_ac $ repeat (ematch >> try close) +using_smt_core no_ac $ intros >> repeat (ematch >> try close) section add_comm_monoid variables [add_comm_monoid α] diff --git a/tests/lean/smt_begin_end1.lean b/tests/lean/smt_begin_end1.lean index 9d9dc738ab..67492a10d0 100644 --- a/tests/lean/smt_begin_end1.lean +++ b/tests/lean/smt_begin_end1.lean @@ -4,6 +4,7 @@ axiom pf (a : nat) : p (f a) (f a) → p a a example (a b c : nat) : a = b → p (f a) (f b) → p a b := begin [smt] + intros, assert h : p (f a) (f a), trace_state, add_fact (pf _ h) @@ -19,6 +20,7 @@ begin intro h, subst h, begin [smt] + intros, assert h₁ : p (f a) (f a), trace_state, add_fact (pf _ h₁) @@ -27,6 +29,7 @@ end example (p q : Prop) : p ∨ q → p ∨ ¬q → ¬p ∨ q → p ∧ q := begin [smt] + intros, tactic.split, { by_cases p }, { by_cases p }