From f8f3f9402e21f5ad50f0bd9043be5b55b449b073 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 10 Nov 2015 16:57:57 -0800 Subject: [PATCH] feat(library/blast): major reorg and basic backward chaining action --- src/library/blast/CMakeLists.txt | 2 +- src/library/blast/backward.cpp | 148 ++++++++++++++++++++++++++ src/library/blast/backward.h | 14 +++ src/library/blast/choice_point.cpp | 11 +- src/library/blast/choice_point.h | 16 +-- src/library/blast/intros.cpp | 8 +- src/library/blast/simple_strategy.cpp | 82 ++++++++------ src/library/blast/state.cpp | 32 +++--- src/library/blast/state.h | 87 +++++++++------ tests/lean/run/blast3.lean | 35 ++++++ 10 files changed, 335 insertions(+), 100 deletions(-) create mode 100644 src/library/blast/backward.cpp create mode 100644 src/library/blast/backward.h create mode 100644 tests/lean/run/blast3.lean diff --git a/src/library/blast/CMakeLists.txt b/src/library/blast/CMakeLists.txt index 7d4821e90..d57166d77 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) + options.cpp choice_point.cpp simple_strategy.cpp backward.cpp) diff --git a/src/library/blast/backward.cpp b/src/library/blast/backward.cpp new file mode 100644 index 000000000..d21f48082 --- /dev/null +++ b/src/library/blast/backward.cpp @@ -0,0 +1,148 @@ +/* +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 "kernel/instantiate.h" +#include "kernel/inductive/inductive.h" +#include "library/blast/blast.h" +#include "library/blast/proof_expr.h" +#include "library/blast/choice_point.h" + +namespace lean { +namespace blast { +struct backward_proof_step_cell : public proof_step_cell { + branch m_branch; + expr m_proof; + list m_mvars; + backward_proof_step_cell(branch const & b, expr const & pr, list const & mvars): + m_branch(b), m_proof(pr), m_mvars(mvars) { + lean_assert(!empty(m_mvars)); + } + + virtual ~backward_proof_step_cell() {} + + virtual action_result resolve(expr const & pr) const { + state & s = curr_state(); + s.set_branch(m_branch); + expr mvar = head(m_mvars); + if (!is_def_eq(mvar, pr)) + return action_result::failed(); + list new_mvars = tail(m_mvars); + if (empty(new_mvars)) { + // solved all branches + expr r = to_proof_expr(s.instantiate_urefs_mrefs(m_proof)); + r = unfold_hypotheses_ge(s, r); + return action_result::solved(r); + } else { + s.pop_proof_step(); + auto bcell = new backward_proof_step_cell(m_branch, m_proof, new_mvars); + s.push_proof_step(bcell); + expr new_target = s.instantiate_urefs_mrefs(infer_type(head(new_mvars))); + s.set_target(new_target); + return action_result::new_branch(); + } + } +}; + +static action_result try_lemma(name const & fname, bool prop_only_branches) { + state & s = curr_state(); + declaration const & fdecl = env().get(fname); + 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(mk_fresh_uref()); + levels ls = to_list(ls_buffer.begin(), ls_buffer.end()); + expr f = mk_constant(fname, ls); + expr type = instantiate_type_univ_params(fdecl, ls); + expr pr = f; + buffer mvars; + while (true) { + type = whnf(type); + if (!is_pi(type)) + break; + expr mvar = s.mk_metavar(binding_domain(type)); + mvars.push_back(mvar); + pr = mk_app(pr, mvar); + type = instantiate(binding_body(type), mvar); + } + expr target = s.get_target(); + if (!is_def_eq(target, type)) + return action_result::failed(); + bool has_unassigned = false; + buffer branches; + unsigned i = mvars.size(); + while (i > 0) { + --i; + if (!s.is_mref_assigned(mvars[i])) { + has_unassigned = true; + if (!prop_only_branches || is_prop(infer_type(mvars[i]))) { + branches.push_back(mvars[i]); + } + } + } + if (!has_unassigned) { + // all meta-variables have been assigned + return action_result::solved(to_proof_expr(s.instantiate_urefs_mrefs(pr))); + } + if (branches.empty()) { + // some meta-variables were not assigned, but they are not propositions, + // and since prop_only_branches == true, we only create branches for propositions + return action_result::failed(); + } + auto bcell = new backward_proof_step_cell(s.get_branch(), pr, to_list(branches)); + s.push_proof_step(bcell); + expr new_target = s.instantiate_urefs_mrefs(infer_type(branches[0])); + s.set_target(new_target); + return action_result::new_branch(); +} + +class backward_choice_point_cell : public choice_point_cell { + state m_state; + list m_fnames; + bool m_prop_only; +public: + backward_choice_point_cell(state const & s, list const & fnames, bool prop_only): + m_state(s), m_fnames(fnames), m_prop_only(prop_only) {} + + virtual action_result next() { + while (!empty(m_fnames)) { + curr_state() = m_state; + name fname = head(m_fnames); + m_fnames = tail(m_fnames); + action_result r = try_lemma(fname, m_prop_only); + if (!failed(r)) + return r; + } + return action_result::failed(); + } +}; + +action_result backward_action(list const & fnames, bool prop_only_branches) { + state s = curr_state(); + auto it = fnames; + while (!empty(it)) { + action_result r = try_lemma(head(it), prop_only_branches); + it = tail(it); + if (!failed(r)) { + // create choice point + if (!empty(it)) + push_choice_point(choice_point(new backward_choice_point_cell(s, it, prop_only_branches))); + return r; + } + curr_state() = s; + } + return action_result::failed(); +} + +action_result constructor_action(bool prop_only_branches) { + state s = curr_state(); + expr I = get_app_fn(s.get_target()); + if (!is_constant(I) || !inductive::is_inductive_decl(env(), const_name(I))) + return action_result::failed(); + buffer c_names; + get_intro_rule_names(env(), const_name(I), c_names); + return backward_action(to_list(c_names), prop_only_branches); +} +}} diff --git a/src/library/blast/backward.h b/src/library/blast/backward.h new file mode 100644 index 000000000..f667c5dcb --- /dev/null +++ b/src/library/blast/backward.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/action_result.h" + +namespace lean { +namespace blast { +action_result backward_action(list const & fnames, bool prop_only_branches = true); +action_result constructor_action(bool prop_only_branches = true); +}} diff --git a/src/library/blast/choice_point.cpp b/src/library/blast/choice_point.cpp index c3a8b6c6c..0198b798f 100644 --- a/src/library/blast/choice_point.cpp +++ b/src/library/blast/choice_point.cpp @@ -20,15 +20,14 @@ void push_choice_point(choice_point const & c) { get_choice_points().push_back(c); } -bool next_choice_point() { +action_result next_choice_point() { auto & cs = get_choice_points(); while (true) { if (cs.empty()) - return false; - if (auto r = cs.back().next()) { - curr_state() = *r; - return true; - } + return action_result::failed(); + action_result r = cs.back().next(); + if (!failed(r)) + return r; cs.pop_back(); } } diff --git a/src/library/blast/choice_point.h b/src/library/blast/choice_point.h index 3688a7e12..28692ec5d 100644 --- a/src/library/blast/choice_point.h +++ b/src/library/blast/choice_point.h @@ -20,11 +20,11 @@ class choice_point_cell { MK_LEAN_RC(); // Declare m_rc counter void dealloc() { delete this; } public: - virtual ~choice_point_cell(); - /** \brief Return the next proof state. This method may + virtual ~choice_point_cell() {} + /** \brief Update next proof state. This method may perform destructive updates, choice points are not shared objects. */ - virtual optional next() = 0; + virtual action_result next() = 0; }; /** \brief Smart pointer for choice points */ @@ -39,7 +39,7 @@ public: choice_point & operator=(choice_point const & s) { LEAN_COPY_REF(s); } choice_point & operator=(choice_point && s) { LEAN_MOVE_REF(s); } - optional next() { + action_result next() { lean_assert(m_ptr); return m_ptr->next(); } @@ -49,9 +49,11 @@ public: void init_choice_points(); /** \brief Add choice point to the top of the stack */ void push_choice_point(choice_point const & c); -/** \brief If there is another choice point, then update the current state and return true. - Otherwise, return false. */ -bool next_choice_point(); +inline void push_choice_point(choice_point_cell * cell) { + push_choice_point(choice_point(cell)); +} +/** \brief Keep executing choice points until one of them doesn't fail. */ +action_result next_choice_point(); /** \brief Return size of the choice point stack */ unsigned get_num_choice_points(); /** \brief Shrink the size of the choice point stack. diff --git a/src/library/blast/intros.cpp b/src/library/blast/intros.cpp index 1d4ece5ad..984e34653 100644 --- a/src/library/blast/intros.cpp +++ b/src/library/blast/intros.cpp @@ -14,9 +14,9 @@ namespace blast { struct intros_proof_step_cell : public proof_step_cell { list m_new_hs; virtual ~intros_proof_step_cell() {} - virtual optional resolve(state & s, expr const & pr) const { - expr new_pr = mk_proof_lambda(s, m_new_hs, unfold_hypotheses_ge(s, pr)); - return some_expr(new_pr); + virtual action_result resolve(expr const & pr) const { + expr new_pr = mk_proof_lambda(curr_state(), m_new_hs, unfold_hypotheses_ge(curr_state(), pr)); + return action_result::solved(new_pr); } }; @@ -26,7 +26,7 @@ bool intros_action() { if (!is_pi(target)) return false; auto pcell = new intros_proof_step_cell(); - s.push_proof_step(proof_step(pcell)); + s.push_proof_step(pcell); buffer new_hs; while (is_pi(target)) { expr href = s.mk_hypothesis(binding_name(target), binding_domain(target)); diff --git a/src/library/blast/simple_strategy.cpp b/src/library/blast/simple_strategy.cpp index 5ec9270b4..089a14d83 100644 --- a/src/library/blast/simple_strategy.cpp +++ b/src/library/blast/simple_strategy.cpp @@ -9,6 +9,7 @@ Author: Leonardo de Moura #include "library/blast/choice_point.h" #include "library/blast/assumption.h" #include "library/blast/intros.h" +#include "library/blast/backward.h" namespace lean { namespace blast { @@ -25,52 +26,66 @@ class simple_strategy { return curr_state().activate_hypothesis(); } - pair next_action() { - if (intros_action()) { - return mk_pair(Continue, expr()); - } else if (activate_hypothesis()) { + action_result next_action() { + if (intros_action()) + return action_result::new_branch(); + + if (activate_hypothesis()) { // TODO(Leo): we should probably eagerly simplify the activated hypothesis. - return mk_pair(Continue, expr()); - } else if (auto pr = assumption_action()) { - return mk_pair(ClosedBranch, *pr); - } else { - // TODO(Leo): add more actions... - return mk_pair(NoAction, expr()); + return action_result::new_branch(); } + + if (auto pr = assumption_action()) { + return action_result::solved(*pr); + } + + action_result r = constructor_action(); + if (!failed(r)) return r; + + // TODO(Leo): add more actions... + return action_result::failed(); } - optional resolve(expr pr) { + action_result next_branch(expr pr) { while (curr_state().has_proof_steps()) { - proof_step s = curr_state().top_proof_step(); - if (auto new_pr = s.resolve(curr_state(), pr)) { - pr = *new_pr; + proof_step s = curr_state().top_proof_step(); + action_result r = s.resolve(pr); + switch (r.get_kind()) { + case action_result::Failed: + return r; + case action_result::Solved: + pr = r.get_proof(); curr_state().pop_proof_step(); - } else { - return none_expr(); // continue the search + break; + case action_result::NewBranch: + return action_result::new_branch(); } } - return some_expr(pr); // closed all branches + return action_result::solved(pr); } optional search_upto(unsigned depth) { + action_result r = next_action(); while (true) { - if (curr_state().get_proof_depth() > depth) { - // maximum depth reached - if (!next_choice_point()) { + if (curr_state().get_proof_depth() > depth) + r = action_result::failed(); + switch (r.get_kind()) { + case action_result::Failed: + r = next_choice_point(); + if (failed(r)) { + // all choice points failed... return none_expr(); } - } - auto s = next_action(); - switch (s.first) { - case NoAction: - if (!next_choice_point()) - return none_expr(); break; - case ClosedBranch: - if (auto pr = resolve(s.second)) - return pr; + case action_result::Solved: + r = next_branch(r.get_proof()); + if (r.get_kind() == action_result::Solved) { + // all branches have been solved + return some_expr(r.get_proof()); + } break; - case Continue: + case action_result::NewBranch: + r = next_action(); break; } } @@ -79,14 +94,17 @@ class simple_strategy { optional search() { state s = curr_state(); unsigned d = m_init_depth; - while (d <= m_max_depth) { + while (true) { if (auto r = search_upto(d)) return r; d += m_inc_depth; + if (d > m_max_depth) { + display_curr_state(); + return none_expr(); + } curr_state() = s; clear_choice_points(); } - return none_expr(); } public: diff --git a/src/library/blast/state.cpp b/src/library/blast/state.cpp index a3dd6d662..a70308f32 100644 --- a/src/library/blast/state.cpp +++ b/src/library/blast/state.cpp @@ -369,23 +369,23 @@ struct hypothesis_dep_depth_lt { }; void state::get_sorted_hypotheses(hypothesis_idx_buffer & r) const { - m_hyp_decls.for_each([&](unsigned hidx, hypothesis const &) { + m_branch.m_hyp_decls.for_each([&](unsigned hidx, hypothesis const &) { r.push_back(hidx); }); std::sort(r.begin(), r.end(), hypothesis_dep_depth_lt(*this)); } void state::add_forward_dep(unsigned hidx_user, unsigned hidx_provider) { - if (auto s = m_forward_deps.find(hidx_provider)) { + if (auto s = m_branch.m_forward_deps.find(hidx_provider)) { if (!s->contains(hidx_user)) { hypothesis_idx_set new_s(*s); new_s.insert(hidx_user); - m_forward_deps.insert(hidx_provider, new_s); + m_branch.m_forward_deps.insert(hidx_provider, new_s); } } else { hypothesis_idx_set new_s; new_s.insert(hidx_user); - m_forward_deps.insert(hidx_provider, new_s); + m_branch.m_forward_deps.insert(hidx_provider, new_s); } } @@ -407,7 +407,7 @@ void state::add_deps(expr const & e, hypothesis & h_user, unsigned hidx_user) { } return false; } else if (is_mref(l)) { - m_mvar_idxs.insert(mref_index(l)); + m_branch.m_mvar_idxs.insert(mref_index(l)); return false; } else { return true; @@ -436,11 +436,11 @@ expr state::mk_hypothesis(unsigned new_hidx, name const & n, expr const & type, new_h.m_self = r; new_h.m_proof_depth = m_proof_depth; add_deps(new_h, new_hidx); - m_hyp_decls.insert(new_hidx, new_h); + m_branch.m_hyp_decls.insert(new_hidx, new_h); if (new_h.is_assumption()) - m_assumption.insert(new_hidx); + m_branch.m_assumption.insert(new_hidx); double w = compute_weight(new_hidx, type); - m_todo_queue.insert(w, new_hidx); + m_branch.m_todo_queue.insert(w, new_hidx); return r; } @@ -468,18 +468,18 @@ void state::update_indices(unsigned /* hidx */) { } optional state::activate_hypothesis() { - if (m_todo_queue.empty()) { + if (m_branch.m_todo_queue.empty()) { return optional(); } else { - unsigned hidx = m_todo_queue.erase_min(); - m_active.insert(hidx); + unsigned hidx = m_branch.m_todo_queue.erase_min(); + m_branch.m_active.insert(hidx); update_indices(hidx); return optional(hidx); } } bool state::hidx_depends_on(unsigned hidx_user, unsigned hidx_provider) const { - if (auto s = m_forward_deps.find(hidx_provider)) { + if (auto s = m_branch.m_forward_deps.find(hidx_provider)) { return s->contains(hidx_user); } else { return false; @@ -487,17 +487,17 @@ bool state::hidx_depends_on(unsigned hidx_user, unsigned hidx_provider) const { } void state::set_target(expr const & t) { - m_target = t; - m_target_deps.clear(); + m_branch.m_target = t; + m_branch.m_target_deps.clear(); if (has_href(t) || has_mref(t)) { for_each(t, [&](expr const & e, unsigned) { if (!has_href(e) && !has_mref(e)) { return false; } else if (is_href(e)) { - m_target_deps.insert(href_index(e)); + m_branch.m_target_deps.insert(href_index(e)); return false; } else if (is_mref(e)) { - m_mvar_idxs.insert(mref_index(e)); + m_branch.m_mvar_idxs.insert(mref_index(e)); return false; } else { return true; diff --git a/src/library/blast/state.h b/src/library/blast/state.h index 51e67018d..31f328148 100644 --- a/src/library/blast/state.h +++ b/src/library/blast/state.h @@ -8,6 +8,7 @@ Author: Leonardo de Moura #include "util/rb_map.h" #include "kernel/expr.h" #include "library/tactic/goal.h" +#include "library/blast/action_result.h" #include "library/blast/hypothesis.h" namespace lean { @@ -44,15 +45,16 @@ public: virtual ~proof_step_cell() {} /** \brief Every proof-step must provide a resolve method. When the branch created by the proof-step is closed, - a proof pr is provided, and the proof-step can perform two operations - 1- setup the next branch and return none_expr - 2- finish and return a new proof + a proof pr is provided, and the proof-step can: + 1- setup the next branch, or + 2- fail, or + 3- finish and return a new proof \remark Proof steps may be shared, i.e., they may ocurren the proof-step stack of different proof state objects. So, resolve must not perform destructive updates. This is why we marked it as const. */ - virtual optional resolve(state & s, expr const & pr) const = 0; + virtual action_result resolve(expr const & pr) const = 0; }; /** \brief Smart pointer for proof steps */ @@ -67,35 +69,18 @@ public: proof_step & operator=(proof_step const & s) { LEAN_COPY_REF(s); } proof_step & operator=(proof_step && s) { LEAN_MOVE_REF(s); } - optional resolve(state & s, expr const & pr) const { + action_result resolve(expr const & pr) const { lean_assert(m_ptr); - return m_ptr->resolve(s, pr); + return m_ptr->resolve(pr); } }; -/** \brief Proof state for the blast tactic */ -class state { +/** \brief Information associated with the current branch of the proof state. + This is essentially a mechanism for creating snapshots of the current branch. */ +class branch { + friend class state; typedef hypothesis_idx_map forward_deps; typedef rb_map todo_queue; - typedef metavar_idx_map metavar_decls; - typedef metavar_idx_map eassignment; - typedef metavar_idx_map uassignment; - typedef hypothesis_idx_map fixed_by; - typedef list proof_steps; - uassignment m_uassignment; - metavar_decls m_metavar_decls; - eassignment m_eassignment; - // In the following mapping, each entry (h -> {m_1 ... m_n}) means that hypothesis `h` cannot be cleared - // in any branch where the metavariables m_1 ... m_n have not been replaced with the values assigned to them. - // That is, to be able to clear `h` in a branch `B`, we first need to check whether it - // is contained in this mapping or not. If it is, we should check whether any of the - // metavariables `m_1` ... `m_n` occur in `B` (this is a relatively quick check since - // `B` contains an over-approximation of all meta-variables occuring in it (i.e., m_mvar_idxs). - // If this check fails, then we should replace any assigned `m_i` with its value, if the intersection is still - // non-empty, then we cannot clear `h`. - fixed_by m_fixed_by; - unsigned m_proof_depth{0}; - proof_steps m_proof_steps; // 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: @@ -119,6 +104,30 @@ class state { expr m_target; hypothesis_idx_set m_target_deps; metavar_idx_set m_mvar_idxs; +}; + +/** \brief Proof state for the blast tactic */ +class state { + typedef metavar_idx_map metavar_decls; + typedef metavar_idx_map eassignment; + typedef metavar_idx_map uassignment; + typedef hypothesis_idx_map fixed_by; + typedef list proof_steps; + uassignment m_uassignment; + metavar_decls m_metavar_decls; + eassignment m_eassignment; + // In the following mapping, each entry (h -> {m_1 ... m_n}) means that hypothesis `h` cannot be cleared + // in any branch where the metavariables m_1 ... m_n have not been replaced with the values assigned to them. + // That is, to be able to clear `h` in a branch `B`, we first need to check whether it + // is contained in this mapping or not. If it is, we should check whether any of the + // metavariables `m_1` ... `m_n` occur in `B` (this is a relatively quick check since + // `B` contains an over-approximation of all meta-variables occuring in it (i.e., m_mvar_idxs). + // If this check fails, then we should replace any assigned `m_i` with its value, if the intersection is still + // non-empty, then we cannot clear `h`. + fixed_by m_fixed_by; + unsigned m_proof_depth{0}; + 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); @@ -164,7 +173,13 @@ public: metavar_decl const * get_metavar_decl(unsigned 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)); } - bool has_mvar(expr const & e) const { return m_mvar_idxs.contains(mref_index(e)); } + bool has_mvar(expr const & e) const { return m_branch.m_mvar_idxs.contains(mref_index(e)); } + + /************************ + Save/Restore branch + *************************/ + branch const & get_branch() const { return m_branch; } + void set_branch(branch const & b) { m_branch = b; } /************************ Hypotheses @@ -179,12 +194,12 @@ public: \c hidx_provider. */ bool hidx_depends_on(unsigned hidx_user, unsigned hidx_provider) const; - hypothesis const * get_hypothesis_decl(unsigned hidx) const { return m_hyp_decls.find(hidx); } + hypothesis const * get_hypothesis_decl(unsigned 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_hyp_decls.for_each(fn); } + 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_active.find_if([&](unsigned hidx) { + return m_branch.m_active.find_if([&](unsigned hidx) { return fn(hidx, *get_hypothesis_decl(hidx)); }); } @@ -197,7 +212,7 @@ public: expr expand_hrefs(expr const & e, list const & hrefs) const; - hypothesis_idx_set get_assumptions() const { return m_assumption; } + hypothesis_idx_set get_assumptions() const { return m_branch.m_assumption; } /************************ Abstracting hypotheses @@ -226,9 +241,9 @@ public: /** \brief Set target (aka conclusion, aka type of the goal, aka type of the term that must be synthesize in the current branch) */ void set_target(expr const & t); - expr const & get_target() const { return m_target; } + expr const & get_target() const { return m_branch.m_target; } /** \brief Return true iff the target depends on the given hypothesis */ - bool target_depends_on(expr const & h) const { return m_target_deps.contains(href_index(h)); } + bool target_depends_on(expr const & h) const { return m_branch.m_target_deps.contains(href_index(h)); } /************************ Proof steps @@ -239,6 +254,10 @@ public: m_proof_steps = cons(ps, m_proof_steps); } + void push_proof_step(proof_step_cell * cell) { + push_proof_step(proof_step(cell)); + } + bool has_proof_steps() const { return static_cast(m_proof_steps); } diff --git a/tests/lean/run/blast3.lean b/tests/lean/run/blast3.lean new file mode 100644 index 000000000..88899736c --- /dev/null +++ b/tests/lean/run/blast3.lean @@ -0,0 +1,35 @@ +set_option blast.init_depth 10 + +example (a b c : Prop) : b → c → b ∧ c := +by blast + +example (a b c : Prop) : b → c → c ∧ b := +by blast + +example (a b : Prop) : a → a ∨ b := +by blast + +example (a b : Prop) : b → a ∨ b := +by blast + +example (a b : Prop) : b → a ∨ a ∨ b := +by blast + +example (a b c : Prop) : b → c → a ∨ a ∨ (b ∧ c) := +by blast + +example (p q : nat → Prop) (a b : nat) : p a → q b → ∃ x, p x := +by blast + +example {A : Type} (p q : A → Prop) (a b : A) : q a → p b → ∃ x, p x := +by blast + +lemma foo₁ {A : Type} (p q : A → Prop) (a b : A) : q a → p b → ∃ x, (p x ∧ x = b) ∨ q x := +by blast + +lemma foo₂ {A : Type} (p q : A → Prop) (a b : A) : p b → ∃ x, q x ∨ (p x ∧ x = b) := +by blast + +reveal foo₁ foo₂ +print foo₁ +print foo₂