From 5ada4312d783d48a77a0bf9018566802cf4af9d6 Mon Sep 17 00:00:00 2001 From: Daniel Selsam Date: Thu, 19 Nov 2015 10:57:59 -0800 Subject: [PATCH] feat(library/blast/forward): propositional forward chaining --- src/CMakeLists.txt | 2 + src/library/app_builder.cpp | 9 ++ src/library/app_builder.h | 2 + .../blast/backward/backward_action.cpp | 3 +- src/library/blast/forward/CMakeLists.txt | 1 + src/library/blast/forward/forward_action.cpp | 142 ++++++++++++++++++ src/library/blast/forward/forward_action.h | 15 ++ src/library/blast/forward/init_module.cpp | 18 +++ src/library/blast/forward/init_module.h | 13 ++ src/library/blast/init_module.cpp | 3 + src/library/blast/simple_strategy.cpp | 2 + src/util/rb_multi_map.h | 50 ++++++ tests/lean/run/blast22.lean | 13 ++ 13 files changed, 271 insertions(+), 2 deletions(-) create mode 100644 src/library/blast/forward/CMakeLists.txt create mode 100644 src/library/blast/forward/forward_action.cpp create mode 100644 src/library/blast/forward/forward_action.h create mode 100644 src/library/blast/forward/init_module.cpp create mode 100644 src/library/blast/forward/init_module.h create mode 100644 src/util/rb_multi_map.h create mode 100644 tests/lean/run/blast22.lean diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 3a3e96651..aad93b9f1 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -351,6 +351,8 @@ add_subdirectory(library/blast) set(LEAN_OBJS ${LEAN_OBJS} $) add_subdirectory(library/blast/backward) set(LEAN_OBJS ${LEAN_OBJS} $) +add_subdirectory(library/blast/forward) +set(LEAN_OBJS ${LEAN_OBJS} $) add_subdirectory(library/error_handling) set(LEAN_OBJS ${LEAN_OBJS} $) add_subdirectory(compiler) diff --git a/src/library/app_builder.cpp b/src/library/app_builder.cpp index b35127a12..07db2d072 100644 --- a/src/library/app_builder.cpp +++ b/src/library/app_builder.cpp @@ -494,6 +494,11 @@ struct app_builder::imp { return mk_app(get_false_of_true_iff_false_name(), {H}); } + expr mk_not(expr const & H) { + // TODO(dhs): implement custom version if bottleneck. + return mk_app(get_not_name(), {H}); + } + expr mk_partial_add(expr const & A) { level lvl = get_level(A); auto A_has_add = m_ctx->mk_class_instance(::lean::mk_app(mk_constant(get_has_add_name(), {lvl}), A)); @@ -656,6 +661,10 @@ expr app_builder::mk_false_of_true_iff_false(expr const & H) { return m_ptr->mk_false_of_true_iff_false(H); } +expr app_builder::mk_not(expr const & H) { + return m_ptr->mk_not(H); +} + expr app_builder::mk_partial_add(expr const & A) { return m_ptr->mk_partial_add(A); } diff --git a/src/library/app_builder.h b/src/library/app_builder.h index ff1825de2..0c8b9112b 100644 --- a/src/library/app_builder.h +++ b/src/library/app_builder.h @@ -126,6 +126,8 @@ public: /** \brief (true <-> false) -> false */ expr mk_false_of_true_iff_false(expr const & H); + expr mk_not(expr const & H); + expr mk_partial_add(expr const & A); expr mk_partial_mul(expr const & A); expr mk_zero(expr const & A); diff --git a/src/library/blast/backward/backward_action.cpp b/src/library/blast/backward/backward_action.cpp index 8c1989971..a657204b7 100644 --- a/src/library/blast/backward/backward_action.cpp +++ b/src/library/blast/backward/backward_action.cpp @@ -29,8 +29,7 @@ struct backward_proof_step_cell : public proof_step_cell { state & s = curr_state(); s.set_branch(m_branch); expr mvar = head(m_mvars); - if (!is_def_eq(mvar, pr)) - return action_result::failed(); + if (!is_def_eq(mvar, pr)) return action_result::failed(); list new_mvars = tail(m_mvars); if (empty(new_mvars)) { // solved all branches diff --git a/src/library/blast/forward/CMakeLists.txt b/src/library/blast/forward/CMakeLists.txt new file mode 100644 index 000000000..3342b96fc --- /dev/null +++ b/src/library/blast/forward/CMakeLists.txt @@ -0,0 +1 @@ +add_library(forward OBJECT init_module.cpp forward_action.cpp) diff --git a/src/library/blast/forward/forward_action.cpp b/src/library/blast/forward/forward_action.cpp new file mode 100644 index 000000000..97c75a742 --- /dev/null +++ b/src/library/blast/forward/forward_action.cpp @@ -0,0 +1,142 @@ +/* +Copyright (c) 2015 Daniel Selsam. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: Daniel Selsam +*/ +#include "kernel/instantiate.h" +#include "kernel/abstract.h" +#include "kernel/inductive/inductive.h" +#include "library/blast/blast.h" +#include "library/blast/action_result.h" +#include "library/blast/forward/forward_action.h" +#include "library/blast/proof_expr.h" +#include "library/blast/choice_point.h" +#include "library/blast/hypothesis.h" +#include "library/blast/util.h" +#include "library/expr_lt.h" +#include "util/rb_multi_map.h" + +namespace lean { +namespace blast { + +static unsigned g_ext_id = 0; +struct forward_branch_extension : public branch_extension { + rb_multi_map m_lemma_map; + rb_map m_fact_map; + + forward_branch_extension() {} + forward_branch_extension(forward_branch_extension const & b): + m_lemma_map(b.m_lemma_map), m_fact_map(b.m_fact_map) {} + virtual ~forward_branch_extension() {} + virtual branch_extension * clone() override { return new forward_branch_extension(*this); } + + virtual void hypothesis_activated(hypothesis const & h, hypothesis_idx hidx) override { + expr type = whnf(h.get_type()); + if (!is_pi(type)) { + if (is_prop(type)) m_fact_map.insert(type, hidx); + return; + } + bool has_antecedent = false; + while (is_pi(type) && is_prop(binding_domain(type)) && closed(binding_body(type))) { + has_antecedent = true; + m_lemma_map.insert(binding_domain(type), hidx); + type = binding_body(type); + } + if (has_antecedent && is_prop(type)) { + expr not_type; + if (blast::is_not(type, not_type)) m_lemma_map.insert(not_type, hidx); + else m_lemma_map.insert(get_app_builder().mk_not(type), hidx); + } + } + + virtual void hypothesis_deleted(hypothesis const & , hypothesis_idx ) override { + // TODO(dhs): discard once the extensions no longer see duplicates + } + +public: + list const * find_lemmas(expr const & e) { return m_lemma_map.find(e); } + hypothesis_idx const * find_fact(expr const & e) { return m_fact_map.find(e); } +}; + +void initialize_forward_action() { + g_ext_id = register_branch_extension(new forward_branch_extension()); +} + +void finalize_forward_action() { } + +static forward_branch_extension & get_extension() { + return static_cast(curr_state().get_extension(g_ext_id)); +} + +action_result forward_fact(expr const & type) { + forward_branch_extension & ext = get_extension(); + list const * lemmas = ext.find_lemmas(type); + if (!lemmas) return action_result::failed(); + bool success = false; + for_each(*lemmas, [&](hypothesis_idx const & hidx) { + action_result r = forward_action(hidx); + success = success || (r.get_kind() == action_result::NewBranch); + }); + if (success) return action_result::new_branch(); + else return action_result::failed(); +} + +action_result forward_pi(expr const & _type, expr const & proof) { + forward_branch_extension & ext = get_extension(); + bool missing_argument = false; + bool has_antecedent = false; + expr type = _type; + expr new_hypothesis = proof; + expr local; + while (is_pi(type) && is_prop(binding_domain(type)) && closed(binding_body(type))) { + has_antecedent = true; + hypothesis_idx const * fact_hidx = ext.find_fact(binding_domain(type)); + if (fact_hidx) { + hypothesis const & fact_h = curr_state().get_hypothesis_decl(*fact_hidx); + new_hypothesis = mk_app(new_hypothesis, fact_h.get_self()); + } else { + if (missing_argument) return action_result::failed(); + local = mk_fresh_local(binding_domain(type)); + new_hypothesis = mk_app(new_hypothesis, local); + missing_argument = true; + } + type = binding_body(type); + } + + if (!has_antecedent) { + return action_result::failed(); + } else if (!missing_argument) { + curr_state().mk_hypothesis(type, new_hypothesis); + return action_result::new_branch(); + } else if (is_prop(type)) { + expr not_type; + if (blast::is_not(type, not_type)) { + hypothesis_idx const * fact_hidx = ext.find_fact(not_type); + if (!fact_hidx) return action_result::failed(); + hypothesis const & fact_h = curr_state().get_hypothesis_decl(*fact_hidx); + // TODO(dhs): if classical, use double negation elimination + curr_state().mk_hypothesis(get_app_builder().mk_not(infer_type(local)), + Fun(local, mk_app(new_hypothesis, fact_h.get_self()))); + return action_result::new_branch(); + } else { + hypothesis_idx const * fact_hidx = ext.find_fact(get_app_builder().mk_not(type)); + if (!fact_hidx) return action_result::failed(); + hypothesis const & fact_h = curr_state().get_hypothesis_decl(*fact_hidx); + curr_state().mk_hypothesis(get_app_builder().mk_not(infer_type(local)), + Fun(local, mk_app(fact_h.get_self(), new_hypothesis))); + return action_result::new_branch(); + } + } else { + return action_result::failed(); + } + lean_unreachable(); +} + +action_result forward_action(unsigned _hidx) { + hypothesis const & h = curr_state().get_hypothesis_decl(_hidx); + expr type = whnf(h.get_type()); + if (is_pi(type)) return forward_pi(type, h.get_self()); + else if (is_prop(type)) return forward_fact(type); + else return action_result::failed(); +} +}} diff --git a/src/library/blast/forward/forward_action.h b/src/library/blast/forward/forward_action.h new file mode 100644 index 000000000..11f1e5baa --- /dev/null +++ b/src/library/blast/forward/forward_action.h @@ -0,0 +1,15 @@ +/* +Copyright (c) 2015 Daniel Selsam. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: Daniel Selsam +*/ +#pragma once +#include "library/blast/action_result.h" + +namespace lean { +namespace blast { +action_result forward_action(unsigned hidx); + +void initialize_forward_action(); +void finalize_forward_action(); +}} diff --git a/src/library/blast/forward/init_module.cpp b/src/library/blast/forward/init_module.cpp new file mode 100644 index 000000000..7922d42eb --- /dev/null +++ b/src/library/blast/forward/init_module.cpp @@ -0,0 +1,18 @@ +/* +Copyright (c) 2015 Daniel Selsam. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: Daniel Selsam +*/ +#include "library/blast/forward/forward_action.h" + +namespace lean { +namespace blast { + +void initialize_forward_module() { + initialize_forward_action(); +} + +void finalize_forward_module() { + finalize_forward_action(); +} +}} diff --git a/src/library/blast/forward/init_module.h b/src/library/blast/forward/init_module.h new file mode 100644 index 000000000..e2ffd2bb9 --- /dev/null +++ b/src/library/blast/forward/init_module.h @@ -0,0 +1,13 @@ +/* +Copyright (c) 2015 Daniel Selsam. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: Daniel Selsam +*/ +#pragma once + +namespace lean { +namespace blast { +void initialize_forward_module(); +void finalize_forward_module(); +} +} diff --git a/src/library/blast/init_module.cpp b/src/library/blast/init_module.cpp index 6674434f3..f1710b433 100644 --- a/src/library/blast/init_module.cpp +++ b/src/library/blast/init_module.cpp @@ -12,6 +12,7 @@ Author: Leonardo de Moura #include "library/blast/options.h" #include "library/blast/recursor_action.h" #include "library/blast/backward/init_module.h" +#include "library/blast/forward/init_module.h" namespace lean { void initialize_blast_module() { @@ -21,12 +22,14 @@ void initialize_blast_module() { initialize_blast(); blast::initialize_simplifier(); blast::initialize_backward_module(); + blast::initialize_forward_module(); initialize_blast_tactic(); blast::initialize_recursor_action(); } void finalize_blast_module() { blast::finalize_recursor_action(); finalize_blast_tactic(); + blast::finalize_forward_module(); blast::finalize_backward_module(); blast::finalize_simplifier(); finalize_blast(); diff --git a/src/library/blast/simple_strategy.cpp b/src/library/blast/simple_strategy.cpp index e0f137256..3df7caa4c 100644 --- a/src/library/blast/simple_strategy.cpp +++ b/src/library/blast/simple_strategy.cpp @@ -13,6 +13,7 @@ Author: Leonardo de Moura #include "library/blast/subst_action.h" #include "library/blast/backward/backward_action.h" #include "library/blast/backward/backward_strategy.h" +#include "library/blast/forward/forward_action.h" #include "library/blast/no_confusion_action.h" #include "library/blast/simplify_actions.h" #include "library/blast/recursor_action.h" @@ -35,6 +36,7 @@ class simple_strategy : public strategy { Try(subst_action(*hidx)); Try(no_confusion_action(*hidx)); Try(discard_action(*hidx)); + Try(forward_action(*hidx)); Try(recursor_preprocess_action(*hidx)); return action_result::new_branch(); } diff --git a/src/util/rb_multi_map.h b/src/util/rb_multi_map.h new file mode 100644 index 000000000..b33f97961 --- /dev/null +++ b/src/util/rb_multi_map.h @@ -0,0 +1,50 @@ +/* +Copyright (c) 2015 Daniel Selsam. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: Daniel Selsam +*/ +#pragma once +#include "util/rb_map.h" +#include "util/list.h" +#include "kernel/expr.h" +#include "library/io_state_stream.h" + +namespace lean { + +template +class rb_multi_map { + rb_map, Cmp> m_map; + +public: + rb_multi_map() {} + bool empty() const { return m_map.empty(); } + bool contains(T const & t) const { return m_map.contains(t); } + list const * find(T const & t) const { return m_map.find(t); } + void erase(T const & t) { m_map.erase(t); } + template void filter(T const & t, P && p) { + if (auto it = m_map.find(t)) { + auto new_vs = ::lean::filter(*it, std::forward

(p)); + if (!new_vs) + m_map.erase(t); + else + m_map.insert(t, new_vs); + } + } + void erase(T const & t, V const & v) { + filter(t, [&](V const & v2) { return v != v2; }); + } + void insert(T const & t, V const & v) { + if (auto it = m_map.find(t)) + m_map.insert(t, cons(v, *it)); + else + m_map.insert(t, to_list(v)); + } + template void for_each(F && f) const { m_map.for_each(f); } + template void for_each_entry(F && f) const { + m_map.for_each([&](T const & t, list const & vs) { + for (V const & v : vs) + f(t, v); + }); + } +}; +} diff --git a/tests/lean/run/blast22.lean b/tests/lean/run/blast22.lean new file mode 100644 index 000000000..5e6fc398e --- /dev/null +++ b/tests/lean/run/blast22.lean @@ -0,0 +1,13 @@ +-- Basic (propositional) forward chaining +constants (A B C D : Prop) + +definition lemma1 : A → (A → B) → B := by blast +definition lemma2 : ¬ B → (A → B) → ¬ A := by blast +definition lemma3 : ¬ C → A → (A → B → C) → ¬ B := by blast +definition lemma4 : C → A → (A → B → ¬ C) → ¬ B := by blast +-- TODO(dhs): [forward_action] is responsible for +-- eliminating double negation +definition lemma5 : C → A → (A → ¬ B → ¬ C) → ¬ ¬ B := by blast +definition lemma6 : (A → B → ¬ C) → C → A → ¬ B := by blast +definition lemma7 : ¬ C → (A → B → C) → A → ¬ B := by blast +definition lemma8 : A → (A → B) → C → B ∧ C := by blast