michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

refactor(library/tactic): cleanup

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-11-25 01:06:11 -08:00
parent 03791b099c
commit 2c65fdb346
5 changed files with 78 additions and 43 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

76
src/library/tactic/boolean.cpp
View file

@ -19,6 +19,17 @@ namespace lean {
bool is_app_of(expr const & e, expr const & f) { bool is_app_of(expr const & e, expr const & f) {
return is_app(e) && arg(e, 0) == 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) { tactic conj_tactic(bool all) {
return mk_tactic01([=](environment const &, io_state const &, proof_state const & s) -> optional<proof_state> { return mk_tactic01([=](environment const &, io_state const &, proof_state const & s) -> optional<proof_state> {
expr andfn = mk_and_fn(); expr andfn = mk_and_fn();
@ -29,12 +40,13 @@ tactic conj_tactic(bool all) {
check_interrupted(); check_interrupted();
goal const & g = p.second; goal const & g = p.second;
expr const & c = g.get_conclusion(); 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; found = true;
name const & n = p.first; name const & n = p.first;
proof_info.emplace_front(n, c); 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, 1), update(g, c1));
new_goals_buf.emplace_back(name(n, 2), goal(g.get_hypotheses(), arg(c, 2))); new_goals_buf.emplace_back(name(n, 2), update(g, c2));
} else { } else {
new_goals_buf.push_back(p); new_goals_buf.push_back(p);
} }
@ -47,13 +59,15 @@ tactic conj_tactic(bool all) {
name const & n = nc.first; name const & n = nc.first;
expr const & c = nc.second; 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.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); return p(new_m, env, a);
}); });
goals new_goals = to_list(new_goals_buf.begin(), new_goals_buf.end()); 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 { } else {
return optional<proof_state>(); return none_proof_state();
} }
}); });
} }
@ -62,15 +76,14 @@ tactic imp_tactic(name const & H_name, bool all) {
expr impfn = mk_implies_fn(); expr impfn = mk_implies_fn();
bool found = false; bool found = false;
list<std::tuple<name, name, expr>> proof_info; list<std::tuple<name, name, expr>> 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(); 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; found = true;
name new_hn = g.mk_unique_hypothesis_name(H_name); name new_h_name = g.mk_unique_hypothesis_name(H_name);
proof_info.emplace_front(ng, new_hn, c); proof_info.emplace_front(g_name, new_h_name, c);
expr new_h = arg(c, 1); return goal(add_hypothesis(new_h_name, new_h, g.get_hypotheses()), new_c);
expr new_c = arg(c, 2);
return goal(cons(mk_pair(new_hn, new_h), g.get_hypotheses()), new_c);
} else { } else {
return g; return g;
} }
@ -79,20 +92,20 @@ tactic imp_tactic(name const & H_name, bool all) {
proof_builder p = s.get_proof_builder(); 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_builder new_p = mk_proof_builder([=](proof_map const & m, environment const & env, assignment const & a) -> expr {
proof_map new_m(m); proof_map new_m(m);
for (auto info : proof_info) { for (auto const & info : proof_info) {
name const & gn = std::get<0>(info); // goal name name const & goal_name = std::get<0>(info);
name const & hn = std::get<1>(info); // new hypothesis name 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 & 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 & 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 = arg(old_c, 2); // new conclusion: consequent of the old conclusion
expr const & c_pr = find(m, gn); // proof for the new conclusion expr const & c_pr = find(m, goal_name); // proof for the new conclusion
new_m.insert(gn, Discharge(h, c, Fun(hn, h, c_pr))); new_m.insert(goal_name, Discharge(h, c, Fun(hyp_name, h, c_pr)));
} }
return p(new_m, env, a); 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 { } else {
return optional<proof_state>(); 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<proof_state> { return mk_tactic01([=](environment const &, io_state const &, proof_state const & s) -> optional<proof_state> {
expr andfn = mk_and_fn(); expr andfn = mk_and_fn();
bool found = false; bool found = false;
list<std::pair<name, list<std::pair<name, expr>>>> proof_info; // goal name, list(hypothesis name, hypothesis prop) list<std::pair<name, hypotheses>> proof_info; // goal name -> expanded hypotheses
goals new_goals = map_goals(s, [&](name const & ng, goal const & g) -> goal { goals new_goals = map_goals(s, [&](name const & ng, goal const & g) -> goal {
if (all || !found) { if (all || !found) {
buffer<std::pair<name, expr>> new_hyp_buf; buffer<hypothesis> new_hyp_buf;
list<std::pair<name, expr>> proof_info_data; hypotheses proof_info_data;
for (auto const & p : g.get_hypotheses()) { for (auto const & p : g.get_hypotheses()) {
name const & H_name = p.first; name const & H_name = p.first;
expr const & H_prop = p.second; 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; found = true;
proof_info_data.emplace_front(H_name, H_prop); proof_info_data = add_hypothesis(p, proof_info_data);
new_hyp_buf.emplace_back(name(H_name, 1), arg(H_prop, 1)); new_hyp_buf.emplace_back(name(H_name, 1), H1);
new_hyp_buf.emplace_back(name(H_name, 2), arg(H_prop, 2)); new_hyp_buf.emplace_back(name(H_name, 2), H2);
} else { } else {
new_hyp_buf.push_back(p); new_hyp_buf.push_back(p);
} }
} }
if (proof_info_data) { if (proof_info_data) {
proof_info.emplace_front(ng, 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 { } else {
return g; return g;
} }
@ -138,8 +152,8 @@ tactic conj_hyp_tactic(bool all) {
for (auto const & H_name_prop : expanded_hyp) { for (auto const & H_name_prop : expanded_hyp) {
name const & H_name = H_name_prop.first; name const & H_name = H_name_prop.first;
expr const & H_prop = H_name_prop.second; 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_1 = mk_constant(name(H_name, 1));
expr const & H_2 = mk_constant(name(H_name, 2), arg(H_prop, 2)); expr const & H_2 = mk_constant(name(H_name, 2));
if (occurs(H_1, pr)) if (occurs(H_1, pr))
pr = Let(H_1, Conjunct1(arg(H_prop, 1), arg(H_prop, 2), mk_constant(H_name)), pr); pr = Let(H_1, Conjunct1(arg(H_prop, 1), arg(H_prop, 2), mk_constant(H_name)), pr);
if (occurs(H_2, pr)) if (occurs(H_2, pr))
@ -149,9 +163,9 @@ tactic conj_hyp_tactic(bool all) {
} }
return p(new_m, env, a); 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 { } else {
return optional<proof_state>(); return none_proof_state();
} }
}); });
} }

6
src/library/tactic/goal.cpp
View file

@ -17,13 +17,13 @@ Author: Leonardo de Moura
namespace lean { namespace lean {
goal::goal(list<std::pair<name, expr>> 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 { format goal::pp(formatter const & fmt, options const & opts) const {
unsigned indent = get_pp_indent(opts); unsigned indent = get_pp_indent(opts);
bool unicode = get_pp_unicode(opts); bool unicode = get_pp_unicode(opts);
format turnstile = unicode ? format("\u22A2") /* ⊢ */ : format("|-"); format turnstile = unicode ? format("\u22A2") /* ⊢ */ : format("|-");
buffer<std::pair<name, expr>> tmp; buffer<hypothesis> tmp;
to_buffer(m_hypotheses, tmp); to_buffer(m_hypotheses, tmp);
bool first = true; bool first = true;
format r; format r;
@ -105,7 +105,7 @@ std::pair<goal, goal_proof_fn> to_goal(environment const & env, context const &
buffer<context_entry> entries; buffer<context_entry> entries;
for (auto const & e : ctx) for (auto const & e : ctx)
entries.push_back(e); entries.push_back(e);
buffer<std::pair<name, expr>> hypotheses; // normalized names and types of the entries processed so far buffer<hypothesis> hypotheses; // normalized names and types of the entries processed so far
buffer<expr> bodies; // normalized bodies of the entries processed so far buffer<expr> bodies; // normalized bodies of the entries processed so far
std::vector<expr> consts; // cached consts[i] == mk_constant(names[i], hypotheses[i]) std::vector<expr> consts; // cached consts[i] == mk_constant(names[i], hypotheses[i])
auto replace_vars = [&](expr const & e, unsigned offset) -> expr { auto replace_vars = [&](expr const & e, unsigned offset) -> expr {

18
src/library/tactic/goal.h
View file

@ -15,19 +15,31 @@ Author: Leonardo de Moura
#include "kernel/environment.h" #include "kernel/environment.h"
namespace lean { namespace lean {
typedef std::pair<name, expr> hypothesis;
typedef list<hypothesis> hypotheses;
class goal { class goal {
list<std::pair<name, expr>> m_hypotheses; hypotheses m_hypotheses;
expr m_conclusion; expr m_conclusion;
public: public:
goal() {} goal() {}
goal(list<std::pair<name, expr>> const & h, expr const & c); goal(hypotheses const & hs, expr const & c);
list<std::pair<name, expr>> const & get_hypotheses() const { return m_hypotheses; } hypotheses const & get_hypotheses() const { return m_hypotheses; }
expr const & get_conclusion() const { return m_conclusion; } expr const & get_conclusion() const { return m_conclusion; }
operator bool() const { return m_conclusion; } operator bool() const { return m_conclusion; }
format pp(formatter const & fmt, options const & opts) const; format pp(formatter const & fmt, options const & opts) const;
name mk_unique_hypothesis_name(name const & suggestion) 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<hypothesis> 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 <tt>to_goal(env, ctx, T)</tt> \brief Functor for converting a proof for a goal \c g produced using <tt>to_goal(env, ctx, T)</tt>
into a term of type \c t. into a term of type \c t.

5
src/library/tactic/proof_builder.cpp
View file

@ -4,6 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura Author: Leonardo de Moura
*/ */
#include "util/exception.h"
#include "util/sstream.h"
#include "library/tactic/proof_builder.h" #include "library/tactic/proof_builder.h"
namespace lean { namespace lean {
@ -11,7 +13,6 @@ expr find(proof_map const & m, name const & n) {
expr * r = const_cast<proof_map&>(m).splay_find(n); expr * r = const_cast<proof_map&>(m).splay_find(n);
if (r) if (r)
return *r; return *r;
else throw exception(sstream() << "proof for goal '" << n << "' not found");
return expr();
} }
} }

8
src/library/tactic/proof_state.h
View file

@ -6,6 +6,8 @@ Author: Leonardo de Moura
*/ */
#pragma once #pragma once
#include <utility> #include <utility>
#include "util/interrupt.h"
#include "util/optional.h"
#include "library/tactic/goal.h" #include "library/tactic/goal.h"
#include "library/tactic/proof_builder.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); proof_state to_proof_state(environment const & env, context const & ctx, expr const & t);
inline optional<proof_state> some_proof_state(proof_state const & s, goals const & gs, proof_builder const & p) {
return some(proof_state(s, gs, p));
}
inline optional<proof_state> none_proof_state() { return optional<proof_state> (); }
template<typename F> template<typename F>
goals map_goals(proof_state const & s, F && f) { goals map_goals(proof_state const & s, F && f) {
return map_filter(s.get_goals(), [=](std::pair<name, goal> const & in, std::pair<name, goal> & out) -> bool { return map_filter(s.get_goals(), [=](std::pair<name, goal> const & in, std::pair<name, goal> & out) -> bool {
check_interrupted();
goal new_goal = f(in.first, in.second); goal new_goal = f(in.first, in.second);
if (new_goal) { if (new_goal) {
out.first = in.first; out.first = in.first;