From fee0cff29556ea4cbb9dcfc0bf3d0ac33e2e869e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 11 Nov 2015 00:02:47 -0800 Subject: [PATCH] feat(library/blast): add simple indexing data-structure for active hypotheses --- src/library/app_builder.cpp | 55 ++++++++++---------- src/library/app_builder.h | 3 ++ src/library/blast/CMakeLists.txt | 4 +- src/library/blast/assumption.cpp | 24 --------- src/library/blast/hypothesis.h | 1 + src/library/blast/simple_actions.cpp | 58 ++++++++++++++++++++++ src/library/blast/simple_actions.h | 15 ++++++ src/library/blast/simple_strategy.cpp | 11 ++-- src/library/blast/state.cpp | 48 ++++++++++++++++-- src/library/blast/state.h | 55 ++++++++++++-------- src/library/blast/util.cpp | 18 +++++++ src/library/blast/{assumption.h => util.h} | 4 +- tests/lean/run/blast4.lean | 17 +++++++ 13 files changed, 232 insertions(+), 81 deletions(-) delete mode 100644 src/library/blast/assumption.cpp create mode 100644 src/library/blast/simple_actions.cpp create mode 100644 src/library/blast/simple_actions.h create mode 100644 src/library/blast/util.cpp rename src/library/blast/{assumption.h => util.h} (59%) create mode 100644 tests/lean/run/blast4.lean diff --git a/src/library/app_builder.cpp b/src/library/app_builder.cpp index 04b751a87..577527581 100644 --- a/src/library/app_builder.cpp +++ b/src/library/app_builder.cpp @@ -301,19 +301,17 @@ struct app_builder::imp { } } - optional get_level(expr const & A) { + level get_level(expr const & A) { expr Type = m_ctx->whnf(m_ctx->infer(A)); if (!is_sort(Type)) - return none_level(); - return some_level(sort_level(Type)); + throw app_builder_exception(); + return sort_level(Type); } expr mk_eq(expr const & a, expr const & b) { expr A = m_ctx->infer(a); - auto lvl = get_level(A); - if (!lvl) - throw app_builder_exception(); - return ::lean::mk_app(mk_constant(get_eq_name(), {*lvl}), A, a, b); + level lvl = get_level(A); + return ::lean::mk_app(mk_constant(get_eq_name(), {lvl}), A, a, b); } expr mk_iff(expr const & a, expr const & b) { @@ -321,11 +319,9 @@ struct app_builder::imp { } expr mk_eq_refl(expr const & a) { - expr A = m_ctx->infer(a); - auto lvl = get_level(A); - if (!lvl) - throw app_builder_exception(); - return ::lean::mk_app(mk_constant(get_eq_refl_name(), {*lvl}), A, a); + expr A = m_ctx->infer(a); + level lvl = get_level(A); + return ::lean::mk_app(mk_constant(get_eq_refl_name(), {lvl}), A, a); } expr mk_iff_refl(expr const & a) { @@ -338,10 +334,8 @@ struct app_builder::imp { if (!is_eq(p, lhs, rhs)) throw app_builder_exception(); expr A = m_ctx->infer(lhs); - auto lvl = get_level(A); - if (!lvl) - throw app_builder_exception(); - return ::lean::mk_app(mk_constant(get_eq_symm_name(), {*lvl}), A, lhs, rhs, H); + level lvl = get_level(A); + return ::lean::mk_app(mk_constant(get_eq_symm_name(), {lvl}), A, lhs, rhs, H); } expr mk_iff_symm(expr const & H) { @@ -359,10 +353,8 @@ struct app_builder::imp { if (!is_eq(p1, lhs1, rhs1) || !is_eq(p2, lhs2, rhs2)) throw app_builder_exception(); expr A = m_ctx->infer(lhs1); - auto lvl = get_level(A); - if (!lvl) - throw app_builder_exception(); - return ::lean::mk_app({mk_constant(get_eq_trans_name(), {*lvl}), A, lhs1, rhs1, rhs2, H1, H2}); + level lvl = get_level(A); + return ::lean::mk_app({mk_constant(get_eq_trans_name(), {lvl}), A, lhs1, rhs1, rhs2, H1, H2}); } expr mk_iff_trans(expr const & H1, expr const & H2) { @@ -428,13 +420,13 @@ struct app_builder::imp { if (!is_eq(p, lhs, rhs)) throw app_builder_exception(); expr A = m_ctx->infer(lhs); - auto A_lvl = get_level(A); + level A_lvl = get_level(A); expr mtype = m_ctx->whnf(m_ctx->infer(motive)); if (!is_pi(mtype) || !is_sort(binding_body(mtype))) throw app_builder_exception(); level l_1 = sort_level(binding_body(mtype)); name const & eqrec = is_standard(m_ctx->env()) ? get_eq_rec_name() : get_eq_nrec_name(); - return ::lean::mk_app({mk_constant(eqrec, {l_1, *A_lvl}), A, lhs, motive, H1, rhs, H2}); + return ::lean::mk_app({mk_constant(eqrec, {l_1, A_lvl}), A, lhs, motive, H1, rhs, H2}); } expr mk_eq_drec(expr const & motive, expr const & H1, expr const & H2) { @@ -443,18 +435,17 @@ struct app_builder::imp { if (!is_eq(p, lhs, rhs)) throw app_builder_exception(); expr A = m_ctx->infer(lhs); - auto A_lvl = get_level(A); + level A_lvl = get_level(A); expr mtype = m_ctx->whnf(m_ctx->infer(motive)); if (!is_pi(mtype) || !is_pi(binding_body(mtype)) || !is_sort(binding_body(binding_body(mtype)))) throw app_builder_exception(); level l_1 = sort_level(binding_body(binding_body(mtype))); name const & eqrec = is_standard(m_ctx->env()) ? get_eq_drec_name() : get_eq_rec_name(); - return ::lean::mk_app({mk_constant(eqrec, {l_1, *A_lvl}), A, lhs, motive, H1, rhs, H2}); + return ::lean::mk_app({mk_constant(eqrec, {l_1, A_lvl}), A, lhs, motive, H1, rhs, H2}); } expr mk_congr_arg(expr const & f, expr const & H) { // TODO(Leo): efficient version - return mk_app(get_congr_arg_name(), {f, H}); } @@ -467,6 +458,16 @@ struct app_builder::imp { // TODO(Leo): efficient version return mk_app(get_congr_name(), {H1, H2}); } + + expr mk_false_rec(expr const & c, expr const & H) { + level c_lvl = get_level(c); + if (is_standard(m_ctx->env())) { + return ::lean::mk_app(mk_constant(get_false_rec_name(), {c_lvl}), c, H); + } else { + expr H_type = m_ctx->infer(H); + return ::lean::mk_app(mk_constant(get_empty_rec_name(), {c_lvl}), mk_lambda("e", H_type, c), H); + } + } }; app_builder::app_builder(environment const & env, io_state const & ios, reducible_behavior b): @@ -563,6 +564,10 @@ expr app_builder::mk_sorry(expr const & type) { return mk_app(get_sorry_name(), type); } +expr app_builder::mk_false_rec(expr const & c, expr const & H) { + return m_ptr->mk_false_rec(c, H); +} + void app_builder::set_local_instances(list const & insts) { m_ptr->m_ctx->set_local_instances(insts); } diff --git a/src/library/app_builder.h b/src/library/app_builder.h index 44e045c98..ee196ac13 100644 --- a/src/library/app_builder.h +++ b/src/library/app_builder.h @@ -119,6 +119,9 @@ public: /** \brief Create (@sorry type) */ expr mk_sorry(expr const & type); + /** \brief False elimination */ + expr mk_false_rec(expr const & c, expr const & H); + /** \brief Set the local instances. This method is relevant when we want to expose local class instances to the app_builder. diff --git a/src/library/blast/CMakeLists.txt b/src/library/blast/CMakeLists.txt index d57166d77..772ceeeba 100644 --- a/src/library/blast/CMakeLists.txt +++ b/src/library/blast/CMakeLists.txt @@ -1,3 +1,3 @@ add_library(blast OBJECT expr.cpp state.cpp blast.cpp blast_tactic.cpp - init_module.cpp simplifier.cpp assumption.cpp intros.cpp proof_expr.cpp - options.cpp choice_point.cpp simple_strategy.cpp backward.cpp) + init_module.cpp simplifier.cpp simple_actions.cpp intros.cpp proof_expr.cpp + options.cpp choice_point.cpp simple_strategy.cpp backward.cpp util.cpp) diff --git a/src/library/blast/assumption.cpp b/src/library/blast/assumption.cpp deleted file mode 100644 index 5e7ba005c..000000000 --- a/src/library/blast/assumption.cpp +++ /dev/null @@ -1,24 +0,0 @@ -/* -Copyright (c) 2015 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#include "library/blast/blast.h" - -namespace lean { -namespace blast { -optional assumption_action() { - // TODO(Leo): this is a very naive implementation that just traverses the set of - // active hypothesis - state const & s = curr_state(); - expr const & target = s.get_target(); - auto hidx = s.find_active_hypothesis([&](unsigned, hypothesis const & h) { - return is_def_eq(h.get_type(), target); - }); - if (!hidx) - return none_expr(); - hypothesis const * h = s.get_hypothesis_decl(*hidx); - return some_expr(h->get_self()); -} -}} diff --git a/src/library/blast/hypothesis.h b/src/library/blast/hypothesis.h index 373241c05..209215d89 100644 --- a/src/library/blast/hypothesis.h +++ b/src/library/blast/hypothesis.h @@ -15,6 +15,7 @@ class hypothesis; class branch; class state; +typedef unsigned hypothesis_idx; typedef rb_tree hypothesis_idx_set; typedef list hypothesis_idx_list; typedef buffer hypothesis_idx_buffer; diff --git a/src/library/blast/simple_actions.cpp b/src/library/blast/simple_actions.cpp new file mode 100644 index 000000000..53c29ba58 --- /dev/null +++ b/src/library/blast/simple_actions.cpp @@ -0,0 +1,58 @@ +/* +Copyright (c) 2015 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#include "library/constants.h" +#include "library/blast/util.h" +#include "library/blast/blast.h" + +namespace lean { +namespace blast { +// TODO(Leo): we should create choice points when there are meta-variables +optional assumption_action() { + state const & s = curr_state(); + expr const & target = s.get_target(); + for (hypothesis_idx hidx : s.get_head_related()) { + hypothesis const * h = s.get_hypothesis_decl(hidx); + lean_assert(h); + if (is_def_eq(h->get_type(), target)) + return some_expr(h->get_self()); + } + return none_expr(); +} + +optional assumption_contradiction_actions(hypothesis_idx hidx) { + state const & s = curr_state(); + app_builder & b = get_app_builder(); + hypothesis const * h = s.get_hypothesis_decl(hidx); + lean_assert(h); + expr const & type = h->get_type(); + if (blast::is_false(type)) { + return some_expr(b.mk_false_rec(s.get_target(), h->get_self())); + } + if (is_def_eq(type, s.get_target())) { + return some_expr(h->get_self()); + } + expr p1 = type; + bool is_neg1 = is_not(type, p1); + for (hypothesis_idx hidx2 : s.get_head_related(hidx)) { + hypothesis const * h2 = s.get_hypothesis_decl(hidx2); + expr type2 = h2->get_type(); + expr p2 = type2; + bool is_neg2 = is_not(type2, p2); + if (is_neg1 != is_neg2) { + if (is_def_eq(p1, p2)) { + if (is_neg1) { + return some_expr(b.mk_app(get_absurd_name(), {s.get_target(), h2->get_self(), h->get_self()})); + } else { + lean_assert(is_neg2); + return some_expr(b.mk_app(get_absurd_name(), {s.get_target(), h->get_self(), h2->get_self()})); + } + } + } + } + return none_expr(); +} +}} diff --git a/src/library/blast/simple_actions.h b/src/library/blast/simple_actions.h new file mode 100644 index 000000000..3f9145728 --- /dev/null +++ b/src/library/blast/simple_actions.h @@ -0,0 +1,15 @@ +/* +Copyright (c) 2015 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +#include "kernel/expr.h" +namespace lean { +namespace blast { +optional assumption_action(); +/** \brief Apply assumption and contradiction actions using the given hypothesis. + \remark This action is supposed to be applied when a hypothesis is activated. */ +optional assumption_contradiction_actions(hypothesis_idx hidx); +}} diff --git a/src/library/blast/simple_strategy.cpp b/src/library/blast/simple_strategy.cpp index 089a14d83..4a75b6dbe 100644 --- a/src/library/blast/simple_strategy.cpp +++ b/src/library/blast/simple_strategy.cpp @@ -7,7 +7,7 @@ Author: Leonardo de Moura #include "library/blast/blast.h" #include "library/blast/options.h" #include "library/blast/choice_point.h" -#include "library/blast/assumption.h" +#include "library/blast/simple_actions.h" #include "library/blast/intros.h" #include "library/blast/backward.h" @@ -22,7 +22,7 @@ class simple_strategy { enum status { NoAction, ClosedBranch, Continue }; - optional activate_hypothesis() { + optional activate_hypothesis() { return curr_state().activate_hypothesis(); } @@ -30,12 +30,15 @@ class simple_strategy { if (intros_action()) return action_result::new_branch(); - if (activate_hypothesis()) { - // TODO(Leo): we should probably eagerly simplify the activated hypothesis. + if (auto hidx = activate_hypothesis()) { + if (auto pr = assumption_contradiction_actions(*hidx)) + return action_result::solved(*pr); return action_result::new_branch(); } if (auto pr = assumption_action()) { + // Remark: this action is only relevant + // when the target has been modified. return action_result::solved(*pr); } diff --git a/src/library/blast/state.cpp b/src/library/blast/state.cpp index 5a24853fa..d29d8ba27 100644 --- a/src/library/blast/state.cpp +++ b/src/library/blast/state.cpp @@ -10,6 +10,7 @@ Author: Leonardo de Moura #include "kernel/for_each_fn.h" #include "kernel/replace_fn.h" #include "library/replace_visitor.h" +#include "library/blast/util.h" #include "library/blast/state.h" namespace lean { @@ -433,9 +434,50 @@ expr state::mk_hypothesis(expr const & type) { return mk_hypothesis(hidx, name(*g_prefix, hidx), type, none_expr()); } -void state::update_indices(unsigned /* hidx */) { - // TODO(Leo): we need to update the indexing data-structures and send - // the hypothesis if to the congruence closure module after it is implemented. +static optional to_head_index(expr type) { + is_not(type, type); + expr const & f = get_app_fn(type); + if (is_constant(f) || is_local(f)) + return optional(head_index(f)); + else + return optional(); +} + +static optional to_head_index(hypothesis const & h) { + return to_head_index(h.get_type()); +} + +list state::get_occurrences_of(head_index const & h) const { + if (auto r = m_branch.m_head_to_hyps.find(h)) + return *r; + else + return list(); +} + +list state::get_head_related(hypothesis_idx hidx) const { + hypothesis const * h = get_hypothesis_decl(hidx); + lean_assert(h); + /* update m_head_to_hyps */ + if (auto i = to_head_index(*h)) + return get_occurrences_of(*i); + else + return list(); +} + +list state::get_head_related() const { + if (auto i = to_head_index(m_branch.m_target)) + return get_occurrences_of(*i); + else + return list(); +} + +void state::update_indices(hypothesis_idx hidx) { + hypothesis const * h = get_hypothesis_decl(hidx); + lean_assert(h); + /* update m_head_to_hyps */ + if (auto i = to_head_index(*h)) + m_branch.m_head_to_hyps.insert(*i, hidx); + /* TODO(Leo): update congruence closure indices */ } optional state::activate_hypothesis() { diff --git a/src/library/blast/state.h b/src/library/blast/state.h index fcbf62513..5e62d1301 100644 --- a/src/library/blast/state.h +++ b/src/library/blast/state.h @@ -7,6 +7,7 @@ Author: Leonardo de Moura #pragma once #include "util/rb_map.h" #include "kernel/expr.h" +#include "library/head_map.h" #include "library/tactic/goal.h" #include "library/blast/action_result.h" #include "library/blast/hypothesis.h" @@ -90,7 +91,7 @@ public: class branch { friend class state; typedef hypothesis_idx_map forward_deps; - typedef rb_map todo_queue; + typedef rb_map todo_queue; // Hypothesis/facts in the current state hypothesis_decls m_hyp_decls; // We break the set of hypotheses in m_context in 3 sets that are not necessarily disjoint: @@ -107,12 +108,13 @@ class branch { // A derived hypothesis can be in the to-do or active sets. // // We say a hypothesis is in the to-do set when the blast haven't process it yet. - hypothesis_idx_set m_assumption; - hypothesis_idx_set m_active; - todo_queue m_todo_queue; - forward_deps m_forward_deps; // given an entry (h -> {h_1, ..., h_n}), we have that each h_i uses h. - expr m_target; - hypothesis_idx_set m_target_deps; + hypothesis_idx_set m_assumption; + hypothesis_idx_set m_active; + todo_queue m_todo_queue; + head_map m_head_to_hyps; + forward_deps m_forward_deps; // given an entry (h -> {h_1, ..., h_n}), we have that each h_i uses h. + expr m_target; + hypothesis_idx_set m_target_deps; }; /** \brief Proof state for the blast tactic */ @@ -128,20 +130,20 @@ class state { proof_steps m_proof_steps; branch m_branch; - void add_forward_dep(unsigned hidx_user, unsigned hidx_provider); - void add_deps(expr const & e, hypothesis & h_user, unsigned hidx_user); - void add_deps(hypothesis & h_user, unsigned hidx_user); + void add_forward_dep(hypothesis_idx hidx_user, hypothesis_idx hidx_provider); + void add_deps(expr const & e, hypothesis & h_user, hypothesis_idx hidx_user); + void add_deps(hypothesis & h_user, hypothesis_idx hidx_user); /** \brief Compute the weight of a hypothesis with the given type We use this weight to update the todo_queue. */ - double compute_weight(unsigned hidx, expr const & type); + double compute_weight(hypothesis_idx hidx, expr const & type); /** \brief This method is invoked when a hypothesis move from todo to active. We will update indices and data-structures (e.g., congruence closure). */ - void update_indices(unsigned hidx); + void update_indices(hypothesis_idx hidx); - expr mk_hypothesis(unsigned new_hidx, name const & n, expr const & type, optional const & value); + expr mk_hypothesis(hypothesis_idx new_hidx, name const & n, expr const & type, optional const & value); unsigned add_metavar_decl(metavar_decl const & decl); goal to_goal(branch const &) const; @@ -149,8 +151,8 @@ class state { expr mk_binding(bool is_lambda, unsigned num, expr const * hrefs, expr const & b) const; #ifdef LEAN_DEBUG - bool check_hypothesis(expr const & e, unsigned hidx, hypothesis const & h) const; - bool check_hypothesis(unsigned hidx, hypothesis const & h) const; + bool check_hypothesis(expr const & e, hypothesis_idx hidx, hypothesis const & h) const; + bool check_hypothesis(hypothesis_idx hidx, hypothesis const & h) const; bool check_target() const; #endif public: @@ -168,7 +170,7 @@ public: The context of this metavariable will be all assumption hypotheses occurring in the current branch. */ expr mk_metavar(expr const & type); - metavar_decl const * get_metavar_decl(unsigned idx) const { return m_metavar_decls.find(idx); } + metavar_decl const * get_metavar_decl(hypothesis_idx idx) const { return m_metavar_decls.find(idx); } metavar_decl const * get_metavar_decl(expr const & e) const { return get_metavar_decl(mref_index(e)); } /************************ @@ -188,20 +190,20 @@ public: /** \brief Return true iff the hypothesis with index \c hidx_user depends on the hypothesis with index \c hidx_provider. */ - bool hidx_depends_on(unsigned hidx_user, unsigned hidx_provider) const; + bool hidx_depends_on(hypothesis_idx hidx_user, hypothesis_idx hidx_provider) const; - hypothesis const * get_hypothesis_decl(unsigned hidx) const { return m_branch.m_hyp_decls.find(hidx); } + hypothesis const * get_hypothesis_decl(hypothesis_idx hidx) const { return m_branch.m_hyp_decls.find(hidx); } hypothesis const * get_hypothesis_decl(expr const & h) const { return get_hypothesis_decl(href_index(h)); } - void for_each_hypothesis(std::function const & fn) const { m_branch.m_hyp_decls.for_each(fn); } - optional find_active_hypothesis(std::function const & fn) const { // NOLINT - return m_branch.m_active.find_if([&](unsigned hidx) { + void for_each_hypothesis(std::function const & fn) const { m_branch.m_hyp_decls.for_each(fn); } + optional find_active_hypothesis(std::function const & fn) const { // NOLINT + return m_branch.m_active.find_if([&](hypothesis_idx hidx) { return fn(hidx, *get_hypothesis_decl(hidx)); }); } /** \brief Activate the next hypothesis in the TODO queue, return none if the TODO queue is empty. */ - optional activate_hypothesis(); + optional activate_hypothesis(); /** \brief Store in \c r the hypotheses in this branch sorted by dependency depth */ void get_sorted_hypotheses(hypothesis_idx_buffer & r) const; @@ -210,6 +212,15 @@ public: hypothesis_idx_set get_assumptions() const { return m_branch.m_assumption; } + /** \brief Return (active) hypotheses whose head symbol is h or (not h) */ + list get_occurrences_of(head_index const & h) const; + + /** \brief Return (active) hypotheses whose head symbol is equal to the of hidx or it is the negation of */ + list get_head_related(hypothesis_idx hidx) const; + + /** \brief Return (active) hypotheses whose head symbol is equal to target or it is the negation of */ + list get_head_related() const; + /************************ Abstracting hypotheses *************************/ diff --git a/src/library/blast/util.cpp b/src/library/blast/util.cpp new file mode 100644 index 000000000..6a198b6d3 --- /dev/null +++ b/src/library/blast/util.cpp @@ -0,0 +1,18 @@ +/* +Copyright (c) 2015 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#include "library/util.h" +#include "library/blast/blast.h" + +namespace lean { +namespace blast { +bool is_not(expr const & e, expr & a) { + return ::lean::is_not(env(), e, a); +} +bool is_false(expr const & e) { + return ::lean::is_false(env(), e); +} +}} diff --git a/src/library/blast/assumption.h b/src/library/blast/util.h similarity index 59% rename from src/library/blast/assumption.h rename to src/library/blast/util.h index 1b56d9c3f..48ad4ca28 100644 --- a/src/library/blast/assumption.h +++ b/src/library/blast/util.h @@ -8,5 +8,7 @@ Author: Leonardo de Moura #include "kernel/expr.h" namespace lean { namespace blast { -optional assumption_action(); +/** \brief Return true iff \c e is of the form (not a) or (a -> false), and false otherwise */ +bool is_not(expr const & e, expr & a); +bool is_false(expr const & e); }} diff --git a/tests/lean/run/blast4.lean b/tests/lean/run/blast4.lean new file mode 100644 index 000000000..2126eec67 --- /dev/null +++ b/tests/lean/run/blast4.lean @@ -0,0 +1,17 @@ +lemma T1 (a b : Prop) : false → a := +by blast + +reveal T1 +print T1 + +lemma T2 (a b c : Prop) : ¬ a → b → a → c := +by blast + +reveal T2 +print T2 + +example (a b c : Prop) : a → b → ¬ a → c := +by blast + +example (a b c : Prop) : a → b → b → ¬ a → c := +by blast