From 7c8d0f444f28f77b9d9e8f8fc130da66dc7cc090 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 10 Jul 2016 13:49:28 -0700 Subject: [PATCH] feat(library/tactic/backward): finish backward chaining tactic --- library/init/meta/tactic.lean | 4 +- .../tactic/backward/backward_chaining.cpp | 107 +++++++++++++++++- src/library/tactic/gexpr.cpp | 6 +- src/library/tactic/gexpr.h | 4 +- src/library/type_context.h | 1 + .../run/{blast18.lean => back_chaining1.lean} | 12 +- .../run/{blast19.lean => back_chaining2.lean} | 12 +- tests/lean/run/back_chaining3.lean | 22 ++++ tests/lean/run/blast21.lean | 22 ---- 9 files changed, 146 insertions(+), 44 deletions(-) rename tests/lean/run/{blast18.lean => back_chaining1.lean} (64%) rename tests/lean/run/{blast19.lean => back_chaining2.lean} (55%) create mode 100644 tests/lean/run/back_chaining3.lean delete mode 100644 tests/lean/run/blast21.lean diff --git a/library/init/meta/tactic.lean b/library/init/meta/tactic.lean index 2c0f1d0c7f..afb46ef05a 100644 --- a/library/init/meta/tactic.lean +++ b/library/init/meta/tactic.lean @@ -549,10 +549,10 @@ do max ← get_nat_option ("back_chaining" <.> "max_depth") 8, backward_chaining_core reducible tt max leaf_tactic extra_lemmas meta_definition back_chaining : tactic unit := -back_chaining_core failed [] +back_chaining_core assumption [] meta_definition back_chaining_using : list expr → tactic unit := -back_chaining_core failed +back_chaining_core assumption meta_definition back_chaining_using_hs : tactic unit := local_context >>= back_chaining_core failed diff --git a/src/library/tactic/backward/backward_chaining.cpp b/src/library/tactic/backward/backward_chaining.cpp index 1cec097bce..edce4e10a6 100644 --- a/src/library/tactic/backward/backward_chaining.cpp +++ b/src/library/tactic/backward/backward_chaining.cpp @@ -5,10 +5,12 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include "util/sexpr/option_declarations.h" +#include "library/trace.h" #include "library/vm/vm_nat.h" #include "library/vm/vm_expr.h" #include "library/vm/vm_list.h" #include "library/tactic/tactic_state.h" +#include "library/tactic/apply_tactic.h" #include "library/tactic/backward/backward_lemmas.h" #ifndef LEAN_DEFAULT_BACKWARD_CHAINING_MAX_DEPTH @@ -22,6 +24,8 @@ unsigned get_backward_chaining_max_depth(options const & o) { return o.get_unsigned(*g_backward_chaining_max_depth, LEAN_DEFAULT_BACKWARD_CHAINING_MAX_DEPTH); } +#define lean_back_trace(code) lean_trace(name({"tactic", "back_chaining"}), scope_trace_env _scope1(m_ctx.env(), m_ctx); code) + struct back_chaining_fn { tactic_state m_initial_state; type_context m_ctx; @@ -30,6 +34,16 @@ struct back_chaining_fn { vm_obj m_leaf_tactic; backward_lemma_index m_lemmas; + struct choice { + tactic_state m_state; + list m_lemmas; + choice(tactic_state const & s, list const & lemmas): + m_state(s), m_lemmas(lemmas) {} + }; + + tactic_state m_state; + buffer m_choices; + back_chaining_fn(tactic_state const & s, transparency_mode md, bool use_instances, unsigned max_depth, vm_obj const & leaf_tactic, list const & extra_lemmas): @@ -38,20 +52,107 @@ struct back_chaining_fn { m_use_instances(use_instances), m_max_depth(max_depth), m_leaf_tactic(leaf_tactic), - m_lemmas(backward_lemma_index(m_ctx)) { + m_lemmas(backward_lemma_index(m_ctx)), + m_state(m_initial_state) { + lean_assert(s.goals()); for (expr const & extra : extra_lemmas) { m_lemmas.insert(m_ctx, extra); } } + bool invoke_leaf_tactic() { + lean_assert(m_state.goals()); + tactic_state tmp = set_goals(m_state, to_list(head(m_state.goals()))); + vm_obj s = to_obj(tmp); + vm_obj r = invoke(m_leaf_tactic, 1, &s); + if (optional new_s = is_tactic_success(r)) { + m_state = set_goals(*new_s, tail(m_state.goals())); + return true; + } else { + return false; + } + } + + bool try_lemmas(list const & lemmas) { + m_ctx.set_mctx(m_state.mctx()); + list it = lemmas; + while (it) { + backward_lemma const & blemma = head(it); + expr lemma = blemma.to_expr(m_ctx); + lean_back_trace(tout() << "[" << m_choices.size() << "] trying lemma " << lemma << "\n";); + if (optional new_state = apply(m_ctx, false, m_use_instances, lemma, m_state)) { + lean_back_trace(tout() << "succeed\n";); + if (tail(it)) { + m_choices.emplace_back(m_state, tail(it)); + } + m_state = *new_state; + return true; + } + it = tail(it); + } + return false; + } + + bool backtrack() { + while (!m_choices.empty()) { + lean_back_trace(tout() << "[" << m_choices.size() << "] backtracking\n";); + list lemmas = m_choices.back().m_lemmas; + m_state = m_choices.back().m_state; + m_choices.pop_back(); + if (try_lemmas(lemmas)) { + return true; + } + } + return false; + } + + bool run() { + while (true) { + loop_entry: + lean_back_trace(tout() << "current state:\n" << m_state.pp() << "\n";); + if (!m_state.goals()) + return true; + if (m_choices.size() >= m_max_depth) { + lean_back_trace(tout() << "maximum depth reached\n" << m_state.pp() << "\n";); + if (!backtrack()) + return false; + goto loop_entry; + } + metavar_decl g = *m_state.get_main_goal_decl(); + expr target = m_ctx.whnf(g.get_type()); + list lemmas = m_lemmas.find(head_index(target)); + if (!lemmas) { + if (!invoke_leaf_tactic()) { + if (!backtrack()) + return false; + goto loop_entry; + } + } else { + if (!try_lemmas(lemmas)) { + if (!backtrack()) + return false; + goto loop_entry; + } + } + } + } + vm_obj operator()() { - // TODO(Leo): - return mk_tactic_exception("back_chaining entry point", m_initial_state); + list goals = m_initial_state.goals(); + m_state = set_goals(m_initial_state, to_list(head(goals))); + if (run()) { + tactic_state final_state = set_goals(m_state, tail(goals)); + return mk_tactic_success(final_state); + } else { + return mk_tactic_exception("back_chaining failed, use command 'set_option trace.back_chaining true' to obtain more details", m_initial_state); + } } }; vm_obj back_chaining(transparency_mode md, bool use_instances, unsigned max_depth, vm_obj const & leaf_tactic, list const & extra_lemmas, tactic_state const & s) { + optional g = s.get_main_goal_decl(); + if (!g) return mk_no_goals_exception(s); return back_chaining_fn(s, md, use_instances, max_depth, leaf_tactic, extra_lemmas)(); } diff --git a/src/library/tactic/gexpr.cpp b/src/library/tactic/gexpr.cpp index 2de7091982..c883ba3f3e 100644 --- a/src/library/tactic/gexpr.cpp +++ b/src/library/tactic/gexpr.cpp @@ -7,13 +7,13 @@ Author: Leonardo de Moura #include "library/tactic/gexpr.h" namespace lean { -expr gexpr::to_expr(environment const & env, metavar_context & mctx) const { +expr gexpr::to_expr(type_context & ctx) const { if (m_univ_poly) { - declaration const & fdecl = env.get(const_name(m_expr)); + declaration const & fdecl = ctx.env().get(const_name(m_expr)); buffer ls_buffer; unsigned num_univ_ps = fdecl.get_num_univ_params(); for (unsigned i = 0; i < num_univ_ps; i++) - ls_buffer.push_back(mctx.mk_univ_metavar_decl()); + ls_buffer.push_back(ctx.mk_univ_metavar_decl()); levels ls = to_list(ls_buffer.begin(), ls_buffer.end()); return mk_constant(const_name(m_expr), ls); } else { diff --git a/src/library/tactic/gexpr.h b/src/library/tactic/gexpr.h index 7164a6a229..0fbf4d8ea6 100644 --- a/src/library/tactic/gexpr.h +++ b/src/library/tactic/gexpr.h @@ -6,7 +6,7 @@ Author: Leonardo de Moura */ #pragma once #include "kernel/expr.h" -#include "library/metavar_context.h" +#include "library/type_context.h" #include "library/io_state_stream.h" namespace lean { @@ -33,7 +33,7 @@ public: /** \brief Convert generalized expression into a regular expression. If it is universe polymorphic, we accomplish that by creating meta-variables using \c mctx. */ - expr to_expr(environment const & env, metavar_context & mctx) const; + expr to_expr(type_context & ctx) const; /** \brief Return "bare" expression (without adding fresh metavariables if universe polymorphic) */ expr to_bare_expr() const { return m_expr; } diff --git a/src/library/type_context.h b/src/library/type_context.h index 342767d72e..78e2ac8a92 100644 --- a/src/library/type_context.h +++ b/src/library/type_context.h @@ -205,6 +205,7 @@ public: local_context const & lctx() const { return m_lctx; } metavar_context const & mctx() const { return m_mctx; } expr mk_metavar_decl(local_context const & ctx, expr const & type) { return m_mctx.mk_metavar_decl(ctx, type); } + level mk_univ_metavar_decl() { return m_mctx.mk_univ_metavar_decl(); } metavar_context const & get_mctx() const { return m_mctx; } /* note: mctx must be a descendent of m_mctx */ diff --git a/tests/lean/run/blast18.lean b/tests/lean/run/back_chaining1.lean similarity index 64% rename from tests/lean/run/blast18.lean rename to tests/lean/run/back_chaining1.lean index 6c7fadd4d4..fd6cccda71 100644 --- a/tests/lean/run/blast18.lean +++ b/tests/lean/run/back_chaining1.lean @@ -1,6 +1,4 @@ -exit -- Backward chaining with tagged rules -set_option blast.strategy "backward" constants {P Q R S T U : Prop} (Hpq : P → Q) (Hqr : Q → R) (Hrs : R → S) (Hst : S → T) constants (Huq : U → Q) (Hur : U → R) (Hus : U → S) (Hut : U → T) attribute Hpq [intro] @@ -13,7 +11,9 @@ attribute Hur [intro] attribute Hus [intro] attribute Hut [intro] -definition lemma1 (p : P) : Q := by blast -definition lemma2 (p : P) : R := by blast -definition lemma3 (p : P) : S := by blast -definition lemma4 (p : P) : T := by blast +open tactic + +definition lemma1 (p : P) : Q := by back_chaining +definition lemma2 (p : P) : R := by back_chaining +definition lemma3 (p : P) : S := by back_chaining +definition lemma4 (p : P) : T := by back_chaining diff --git a/tests/lean/run/blast19.lean b/tests/lean/run/back_chaining2.lean similarity index 55% rename from tests/lean/run/blast19.lean rename to tests/lean/run/back_chaining2.lean index 41e0db42cb..0a5f423f8c 100644 --- a/tests/lean/run/blast19.lean +++ b/tests/lean/run/back_chaining2.lean @@ -1,6 +1,4 @@ -exit -- Backward chaining with hypotheses -set_option blast.strategy "backward" constants {P Q R S T U : Prop} constants (Huq : U → Q) (Hur : U → R) (Hus : U → S) (Hut : U → T) attribute Huq [intro] @@ -8,7 +6,9 @@ attribute Hur [intro] attribute Hus [intro] attribute Hut [intro] -definition lemma1 : (P → Q) → P → Q := by blast -definition lemma2 : (P → Q) → (Q → R) → P → R := by blast -definition lemma3 : (P → Q) → (Q → R) → (R → S) → P → S := by blast -definition lemma4 : (P → Q) → (Q → R) → (R → S) → (S → T) → P → T := by blast +open tactic + +definition lemma1 : (P → Q) → P → Q := by intros >> back_chaining_using_hs +definition lemma2 : (P → Q) → (Q → R) → P → R := by intros >> back_chaining_using_hs +definition lemma3 : (P → Q) → (Q → R) → (R → S) → P → S := by intros >> back_chaining_using_hs +definition lemma4 : (P → Q) → (Q → R) → (R → S) → (S → T) → P → T := by intros >> back_chaining_using_hs diff --git a/tests/lean/run/back_chaining3.lean b/tests/lean/run/back_chaining3.lean new file mode 100644 index 0000000000..15f31f2018 --- /dev/null +++ b/tests/lean/run/back_chaining3.lean @@ -0,0 +1,22 @@ +namespace ex +open tactic + +constant typ : Type₁ + +constant subtype : typ → typ → Prop + +constant subtype_refl : ∀ T, subtype T T + +constant subtype_trans : ∀ S T U, subtype S T → subtype T U → subtype S U + +attribute subtype_refl subtype_trans [intro] + +lemma L1 : ∀ T1 T2 T3 T4, subtype T1 T2 → subtype T2 T3 → subtype T3 T4 → subtype T1 T4 := +by intros >> back_chaining_using_hs + +set_option back_chaining.max_depth 10 + +lemma L2 : ∀ T1 T2 T3 T4 T5 T6 (H1 :subtype T1 T2) (H2 : subtype T2 T3) (H3 : subtype T3 T4) (H3 : subtype T4 T5) (H4 : subtype T5 T6), subtype T1 T6 := +by intros >> back_chaining_using_hs + +end ex diff --git a/tests/lean/run/blast21.lean b/tests/lean/run/blast21.lean deleted file mode 100644 index 0f3205ec6e..0000000000 --- a/tests/lean/run/blast21.lean +++ /dev/null @@ -1,22 +0,0 @@ -exit - -namespace ex -set_option blast.strategy "backward" - -constant typ : Type₁ - -constant subtype : typ → typ → Prop - -constant subtype_refl : ∀ T, subtype T T - -constant subtype_trans : ∀ S T U, subtype S T → subtype T U → subtype S U - -attribute subtype_refl subtype_trans [intro] - -lemma L1 : ∀ T1 T2 T3 T4 T5 T6, subtype T1 T2 → subtype T2 T3 → subtype T3 T4 → subtype T4 T5 → subtype T5 T6 → subtype T1 T6 := -by blast - -reveal L1 -print L1 - -end ex