diff --git a/src/library/tactic/boolean.cpp b/src/library/tactic/boolean.cpp index 7be21c4e4..f915a1cfa 100644 --- a/src/library/tactic/boolean.cpp +++ b/src/library/tactic/boolean.cpp @@ -19,6 +19,17 @@ namespace lean { bool is_app_of(expr const & e, expr const & f) { return is_app(e) && arg(e, 0) == f; } + +bool is_app_of(expr const & e, expr const & f, expr & arg1, expr & arg2) { + if (is_app_of(e, f)) { + arg1 = arg(e, 1); + arg2 = arg(e, 2); + return true; + } else { + return false; + } +} + tactic conj_tactic(bool all) { return mk_tactic01([=](environment const &, io_state const &, proof_state const & s) -> optional { expr andfn = mk_and_fn(); @@ -29,12 +40,13 @@ tactic conj_tactic(bool all) { check_interrupted(); goal const & g = p.second; expr const & c = g.get_conclusion(); - if ((all || !found) && is_app_of(c, andfn)) { + expr c1, c2; + if ((all || !found) && is_app_of(c, andfn, c1, c2)) { found = true; name const & n = p.first; proof_info.emplace_front(n, c); - new_goals_buf.emplace_back(name(n, 1), goal(g.get_hypotheses(), arg(c, 1))); - new_goals_buf.emplace_back(name(n, 2), goal(g.get_hypotheses(), arg(c, 2))); + new_goals_buf.emplace_back(name(n, 1), update(g, c1)); + new_goals_buf.emplace_back(name(n, 2), update(g, c2)); } else { new_goals_buf.push_back(p); } @@ -47,13 +59,15 @@ tactic conj_tactic(bool all) { name const & n = nc.first; expr const & c = nc.second; new_m.insert(n, Conj(arg(c, 1), arg(c, 2), find(m, name(n, 1)), find(m, name(n, 2)))); + new_m.erase(name(n, 1)); + new_m.erase(name(n, 2)); } return p(new_m, env, a); }); goals new_goals = to_list(new_goals_buf.begin(), new_goals_buf.end()); - return some(proof_state(s, new_goals, new_p)); + return some_proof_state(s, new_goals, new_p); } else { - return optional(); + return none_proof_state(); } }); } @@ -62,15 +76,14 @@ tactic imp_tactic(name const & H_name, bool all) { expr impfn = mk_implies_fn(); bool found = false; list> proof_info; - goals new_goals = map_goals(s, [&](name const & ng, goal const & g) -> goal { + goals new_goals = map_goals(s, [&](name const & g_name, goal const & g) -> goal { expr const & c = g.get_conclusion(); - if ((all || !found) && is_app_of(c, impfn)) { + expr new_h, new_c; + if ((all || !found) && is_app_of(c, impfn, new_h, new_c)) { found = true; - name new_hn = g.mk_unique_hypothesis_name(H_name); - proof_info.emplace_front(ng, new_hn, c); - expr new_h = arg(c, 1); - expr new_c = arg(c, 2); - return goal(cons(mk_pair(new_hn, new_h), g.get_hypotheses()), new_c); + name new_h_name = g.mk_unique_hypothesis_name(H_name); + proof_info.emplace_front(g_name, new_h_name, c); + return goal(add_hypothesis(new_h_name, new_h, g.get_hypotheses()), new_c); } else { return g; } @@ -79,20 +92,20 @@ tactic imp_tactic(name const & H_name, bool all) { proof_builder p = s.get_proof_builder(); proof_builder new_p = mk_proof_builder([=](proof_map const & m, environment const & env, assignment const & a) -> expr { proof_map new_m(m); - for (auto info : proof_info) { - name const & gn = std::get<0>(info); // goal name - name const & hn = std::get<1>(info); // new hypothesis name - expr const & old_c = std::get<2>(info); // old conclusion of the form H => C - expr const & h = arg(old_c, 1); // new hypothesis: antencedent of the old conclusion - expr const & c = arg(old_c, 2); // new conclusion: consequent of the old conclusion - expr const & c_pr = find(m, gn); // proof for the new conclusion - new_m.insert(gn, Discharge(h, c, Fun(hn, h, c_pr))); + for (auto const & info : proof_info) { + name const & goal_name = std::get<0>(info); + name const & hyp_name = std::get<1>(info); // new hypothesis name + expr const & old_c = std::get<2>(info); // old conclusion of the form H => C + expr const & h = arg(old_c, 1); // new hypothesis: antencedent of the old conclusion + expr const & c = arg(old_c, 2); // new conclusion: consequent of the old conclusion + expr const & c_pr = find(m, goal_name); // proof for the new conclusion + new_m.insert(goal_name, Discharge(h, c, Fun(hyp_name, h, c_pr))); } return p(new_m, env, a); }); - return some(proof_state(s, new_goals, new_p)); + return some_proof_state(s, new_goals, new_p); } else { - return optional(); + return none_proof_state(); } }); } @@ -100,26 +113,27 @@ tactic conj_hyp_tactic(bool all) { return mk_tactic01([=](environment const &, io_state const &, proof_state const & s) -> optional { expr andfn = mk_and_fn(); bool found = false; - list>>> proof_info; // goal name, list(hypothesis name, hypothesis prop) + list> proof_info; // goal name -> expanded hypotheses goals new_goals = map_goals(s, [&](name const & ng, goal const & g) -> goal { if (all || !found) { - buffer> new_hyp_buf; - list> proof_info_data; + buffer new_hyp_buf; + hypotheses proof_info_data; for (auto const & p : g.get_hypotheses()) { name const & H_name = p.first; expr const & H_prop = p.second; - if ((all || !found) && is_app_of(H_prop, andfn)) { + expr H1, H2; + if ((all || !found) && is_app_of(H_prop, andfn, H1, H2)) { found = true; - proof_info_data.emplace_front(H_name, H_prop); - new_hyp_buf.emplace_back(name(H_name, 1), arg(H_prop, 1)); - new_hyp_buf.emplace_back(name(H_name, 2), arg(H_prop, 2)); + proof_info_data = add_hypothesis(p, proof_info_data); + new_hyp_buf.emplace_back(name(H_name, 1), H1); + new_hyp_buf.emplace_back(name(H_name, 2), H2); } else { new_hyp_buf.push_back(p); } } if (proof_info_data) { proof_info.emplace_front(ng, proof_info_data); - return goal(to_list(new_hyp_buf.begin(), new_hyp_buf.end()), g.get_conclusion()); + return update(g, new_hyp_buf); } else { return g; } @@ -138,8 +152,8 @@ tactic conj_hyp_tactic(bool all) { for (auto const & H_name_prop : expanded_hyp) { name const & H_name = H_name_prop.first; expr const & H_prop = H_name_prop.second; - expr const & H_1 = mk_constant(name(H_name, 1), arg(H_prop, 1)); - expr const & H_2 = mk_constant(name(H_name, 2), arg(H_prop, 2)); + expr const & H_1 = mk_constant(name(H_name, 1)); + expr const & H_2 = mk_constant(name(H_name, 2)); if (occurs(H_1, pr)) pr = Let(H_1, Conjunct1(arg(H_prop, 1), arg(H_prop, 2), mk_constant(H_name)), pr); if (occurs(H_2, pr)) @@ -149,9 +163,9 @@ tactic conj_hyp_tactic(bool all) { } return p(new_m, env, a); }); - return some(proof_state(s, new_goals, new_p)); + return some_proof_state(s, new_goals, new_p); } else { - return optional(); + return none_proof_state(); } }); } diff --git a/src/library/tactic/goal.cpp b/src/library/tactic/goal.cpp index 078aa64dc..51ef82b32 100644 --- a/src/library/tactic/goal.cpp +++ b/src/library/tactic/goal.cpp @@ -17,13 +17,13 @@ Author: Leonardo de Moura namespace lean { -goal::goal(list> const & h, expr const & c):m_hypotheses(h), m_conclusion(c) {} +goal::goal(hypotheses const & hs, expr const & c):m_hypotheses(hs), m_conclusion(c) {} format goal::pp(formatter const & fmt, options const & opts) const { unsigned indent = get_pp_indent(opts); bool unicode = get_pp_unicode(opts); format turnstile = unicode ? format("\u22A2") /* ⊢ */ : format("|-"); - buffer> tmp; + buffer tmp; to_buffer(m_hypotheses, tmp); bool first = true; format r; @@ -105,7 +105,7 @@ std::pair to_goal(environment const & env, context const & buffer entries; for (auto const & e : ctx) entries.push_back(e); - buffer> hypotheses; // normalized names and types of the entries processed so far + buffer hypotheses; // normalized names and types of the entries processed so far buffer bodies; // normalized bodies of the entries processed so far std::vector consts; // cached consts[i] == mk_constant(names[i], hypotheses[i]) auto replace_vars = [&](expr const & e, unsigned offset) -> expr { diff --git a/src/library/tactic/goal.h b/src/library/tactic/goal.h index 72cd7148a..5c446b4e4 100644 --- a/src/library/tactic/goal.h +++ b/src/library/tactic/goal.h @@ -15,19 +15,31 @@ Author: Leonardo de Moura #include "kernel/environment.h" namespace lean { +typedef std::pair hypothesis; +typedef list hypotheses; class goal { - list> m_hypotheses; - expr m_conclusion; + hypotheses m_hypotheses; + expr m_conclusion; public: goal() {} - goal(list> const & h, expr const & c); - list> const & get_hypotheses() const { return m_hypotheses; } + goal(hypotheses const & hs, expr const & c); + hypotheses const & get_hypotheses() const { return m_hypotheses; } expr const & get_conclusion() const { return m_conclusion; } operator bool() const { return m_conclusion; } format pp(formatter const & fmt, options const & opts) const; name mk_unique_hypothesis_name(name const & suggestion) const; }; +inline goal update(goal const & g, expr const & c) { return goal(g.get_hypotheses(), c); } +inline goal update(goal const & g, hypotheses const & hs) { return goal(hs, g.get_conclusion()); } +inline goal update(goal const & g, buffer const & hs) { return goal(to_list(hs.begin(), hs.end()), g.get_conclusion()); } +inline hypotheses add_hypothesis(name const & h_name, expr const & h, hypotheses const & hs) { + return cons(mk_pair(h_name, h), hs); +} +inline hypotheses add_hypothesis(hypothesis const & h, hypotheses const & hs) { + return cons(h, hs); +} + /** \brief Functor for converting a proof for a goal \c g produced using to_goal(env, ctx, T) into a term of type \c t. diff --git a/src/library/tactic/proof_builder.cpp b/src/library/tactic/proof_builder.cpp index 7657e9490..3cffbd1ea 100644 --- a/src/library/tactic/proof_builder.cpp +++ b/src/library/tactic/proof_builder.cpp @@ -4,6 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ +#include "util/exception.h" +#include "util/sstream.h" #include "library/tactic/proof_builder.h" namespace lean { @@ -11,7 +13,6 @@ expr find(proof_map const & m, name const & n) { expr * r = const_cast(m).splay_find(n); if (r) return *r; - else - return expr(); + throw exception(sstream() << "proof for goal '" << n << "' not found"); } } diff --git a/src/library/tactic/proof_state.h b/src/library/tactic/proof_state.h index 15740eebc..f92a53448 100644 --- a/src/library/tactic/proof_state.h +++ b/src/library/tactic/proof_state.h @@ -6,6 +6,8 @@ Author: Leonardo de Moura */ #pragma once #include +#include "util/interrupt.h" +#include "util/optional.h" #include "library/tactic/goal.h" #include "library/tactic/proof_builder.h" @@ -31,9 +33,15 @@ void swap(proof_state & s1, proof_state & s2); proof_state to_proof_state(environment const & env, context const & ctx, expr const & t); +inline optional some_proof_state(proof_state const & s, goals const & gs, proof_builder const & p) { + return some(proof_state(s, gs, p)); +} +inline optional none_proof_state() { return optional (); } + template goals map_goals(proof_state const & s, F && f) { return map_filter(s.get_goals(), [=](std::pair const & in, std::pair & out) -> bool { + check_interrupted(); goal new_goal = f(in.first, in.second); if (new_goal) { out.first = in.first;