From fd41a4f76d878c030fbbd64f7d41188479768968 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 14 Nov 2015 15:58:11 -0800 Subject: [PATCH] feat(library/blast): add simplify_target action --- src/library/blast/CMakeLists.txt | 3 +- src/library/blast/action_result.h | 2 + src/library/blast/simple_strategy.cpp | 45 ++++++++++++++++++++++ src/library/blast/simplify_actions.cpp | 52 ++++++++++++++++++++++++++ src/library/blast/simplify_actions.h | 14 +++++++ tests/lean/run/blast11.lean | 12 ++++++ 6 files changed, 127 insertions(+), 1 deletion(-) create mode 100644 src/library/blast/simplify_actions.cpp create mode 100644 src/library/blast/simplify_actions.h create mode 100644 tests/lean/run/blast11.lean diff --git a/src/library/blast/CMakeLists.txt b/src/library/blast/CMakeLists.txt index 43ca3e848..b0c7f41b9 100644 --- a/src/library/blast/CMakeLists.txt +++ b/src/library/blast/CMakeLists.txt @@ -1,4 +1,5 @@ add_library(blast OBJECT expr.cpp state.cpp blast.cpp blast_tactic.cpp init_module.cpp simplifier.cpp simple_actions.cpp intros_action.cpp proof_expr.cpp options.cpp choice_point.cpp simple_strategy.cpp backward_action.cpp util.cpp - gexpr.cpp revert_action.cpp subst_action.cpp no_confusion_action.cpp) + gexpr.cpp revert_action.cpp subst_action.cpp no_confusion_action.cpp + simplify_actions.cpp) diff --git a/src/library/blast/action_result.h b/src/library/blast/action_result.h index 870ecc74d..4d7e01a6c 100644 --- a/src/library/blast/action_result.h +++ b/src/library/blast/action_result.h @@ -29,7 +29,9 @@ public: static action_result failed() { return action_result(false); } static action_result new_branch() { return action_result(true); } static action_result solved(expr const & pr) { return action_result(pr); } + optional to_opt_expr() const { return m_kind == Solved ? some_expr(m_proof) : none_expr(); } }; inline bool failed(action_result const & r) { return r.get_kind() == action_result::Failed; } +inline bool solved(action_result const & r) { return r.get_kind() == action_result::Solved; } }} diff --git a/src/library/blast/simple_strategy.cpp b/src/library/blast/simple_strategy.cpp index 1860bee71..77b529059 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_action.h" #include "library/blast/no_confusion_action.h" +#include "library/blast/simplify_actions.h" namespace lean { namespace blast { @@ -52,6 +53,45 @@ class simple_strategy { return curr_state().activate_hypothesis(); } + /* \brief Preprocess state + It keeps applying intros, activating and finally simplify target. + Return an expression if the goal has been proved during preprocessing step. */ + optional preprocess_core() { + display_msg("* Preprocess"); + while (true) { + if (intros_action()) + continue; + if (auto hidx = activate_hypothesis()) { + if (auto pr = assumption_contradiction_actions(*hidx)) { + return pr; + } + if (subst_action(*hidx)) + continue; + action_result r = no_confusion_action(*hidx); + if (solved(r)) + return r.to_opt_expr(); + continue; + } + break; + } + if (auto pr = assumption_action()) + return pr; + return simplify_target_action().to_opt_expr(); + } + + optional preprocess() { + if (auto pr = preprocess_core()) { + auto r = next_branch(*pr); + if (!solved(r)) { + throw exception("invalid blast preprocessing action, preprocessing actions should not create branches"); + } else { + return r.to_opt_expr(); + } + } else { + return none_expr(); + } + } + action_result next_action() { if (intros_action()) { display_action("intros"); @@ -160,7 +200,12 @@ class simple_strategy { } optional search() { + clear_choice_points(); curr_state().set_simp_rule_sets(get_simp_rule_sets(env())); + if (auto pr = preprocess()) + return pr; + if (get_num_choice_points() > 0) + throw exception("invalid blast preprocessing action, preprocessing actions should not create choice points"); state s = curr_state(); unsigned d = m_config.m_init_depth; while (true) { diff --git a/src/library/blast/simplify_actions.cpp b/src/library/blast/simplify_actions.cpp new file mode 100644 index 000000000..909965ea7 --- /dev/null +++ b/src/library/blast/simplify_actions.cpp @@ -0,0 +1,52 @@ +/* +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/simple_actions.h" +#include "library/blast/blast.h" +#include "library/blast/simplifier.h" + +namespace lean { +namespace blast { +static bool use_iff(expr const & target) { + return is_standard(env()) && is_prop(target); +} + +class simplify_target_proof_step_cell : public proof_step_cell { + bool m_iff; + expr m_eq_pr; +public: + simplify_target_proof_step_cell(bool iff, expr const & eq_pr): + m_iff(iff), m_eq_pr(eq_pr) {} + + virtual ~simplify_target_proof_step_cell() {} + + virtual action_result resolve(expr const & pr) const { + try { + app_builder & b = get_app_builder(); + if (m_iff) + return action_result::solved(b.mk_app(get_iff_mpr_name(), m_eq_pr, pr)); + else + return action_result::solved(b.mk_app(get_eq_mpr_name(), m_eq_pr, pr)); + } catch (app_builder_exception &) { + return action_result::failed(); + } + } +}; + +action_result simplify_target_action() { + state & s = curr_state(); + expr target = s.get_target(); + bool iff = use_iff(target); + name rname = iff ? get_iff_name() : get_eq_name(); + auto r = simplify(rname, target, s.get_simp_rule_sets()); + if (r.is_none()) + return action_result::failed(); // did nothing + s.push_proof_step(new simplify_target_proof_step_cell(iff, r.get_proof())); + s.set_target(r.get_new()); + return action_result::new_branch(); +} +}} diff --git a/src/library/blast/simplify_actions.h b/src/library/blast/simplify_actions.h new file mode 100644 index 000000000..caf2c3890 --- /dev/null +++ b/src/library/blast/simplify_actions.h @@ -0,0 +1,14 @@ +/* +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 "library/blast/hypothesis.h" +namespace lean { +namespace blast { +optional simplify_hypothesis_action(hypothesis_idx hidx); +bool add_simp_rule_action(hypothesis_idx hidx); +action_result simplify_target_action(); +}} diff --git a/tests/lean/run/blast11.lean b/tests/lean/run/blast11.lean new file mode 100644 index 000000000..c34451713 --- /dev/null +++ b/tests/lean/run/blast11.lean @@ -0,0 +1,12 @@ +import data.nat +open algebra nat + +definition lemma1 (a b : nat) : a + b + 0 = b + a := +by blast + +print lemma1 + +definition lemma2 (a b c : nat) : a + b + 0 + c + a + a + b = 0 + 0 + c + a + b + a + a + b := +by blast + +print lemma2