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

feat(library/tactic): add conj_tactic and imp_tactic

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-11-24 16:29:04 -08:00
parent 1c607f3350
commit 9c42a05b08
8 changed files with 232 additions and 39 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/library/tactic/CMakeLists.txt
View file

@ -1,2 +1,2 @@
add_library(tactic goal.cpp proof_builder.cpp proof_state.cpp tactic.cpp)
add_library(tactic goal.cpp proof_builder.cpp proof_state.cpp tactic.cpp boolean.cpp)
target_link_libraries(tactic ${LEAN_LIBS})

98
src/library/tactic/boolean.cpp Normal file
View file

@ -0,0 +1,98 @@
/*
Copyright (c) 2013 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include <utility>
#include "util/interrupt.h"
#include "kernel/builtin.h"
#include "kernel/abstract.h"
#include "library/basic_thms.h"
#include "library/tactic/goal.h"
#include "library/tactic/proof_builder.h"
#include "library/tactic/proof_state.h"
#include "library/tactic/tactic.h"
namespace lean {
bool is_app_of(expr const & e, expr const & f) {
return is_app(e) && arg(e, 0) == f;
}
tactic conj_tactic(bool all) {
return mk_tactic01([=](environment const &, io_state const &, proof_state const & s) -> optional<proof_state> {
expr andfn = mk_and_fn();
bool found = false;
buffer<std::pair<name, goal>> new_goals_buf;
list<std::pair<name, expr>> proof_info;
for (auto const & p : s.get_goals()) {
check_interrupted();
goal const & g = p.second;
expr const & c = g.get_conclusion();
if ((all || !found) && is_app_of(c, andfn)) {
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)));
} else {
new_goals_buf.push_back(p);
}
}
if (found) {
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 nc : proof_info) {
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))));
}
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));
} else {
return optional<proof_state>();
}
});
}
tactic imp_tactic(name const & H_name, bool all) {
return mk_tactic01([=](environment const &, io_state const &, proof_state const & s) -> optional<proof_state> {
expr impfn = mk_implies_fn();
bool found = false;
list<std::tuple<name, name, expr>> proof_info;
goals new_goals = map_goals(s, [&](name const & ng, goal const & g) -> goal {
expr const & c = g.get_conclusion();
if ((all || !found) && is_app_of(c, impfn)) {
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);
} else {
return g;
}
});
if (found) {
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)));
}
return p(new_m, env, a);
});
return some(proof_state(s, new_goals, new_p));
} else {
return optional<proof_state>();
}
});
}
}

12
src/library/tactic/boolean.h Normal file
View file

@ -0,0 +1,12 @@
/*
Copyright (c) 2013 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/tactic/tactic.h"
namespace lean {
tactic conj_tactic(bool all = true);
tactic imp_tactic(name const & H_name = name("H"), bool all = true);
}

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

@ -41,6 +41,26 @@ format goal::pp(formatter const & fmt, options const & opts) const {
return group(r);
}
name goal::mk_unique_hypothesis_name(name const & suggestion) const {
name n = suggestion;
unsigned i = 0;
while (true) {
bool ok = true;
for (auto const & p : m_hypotheses) {
if (n == p.first) {
ok = false;
break;
}
}
if (ok) {
return n;
} else {
i++;
n = name(suggestion, i);
}
}
}
goal_proof_fn::goal_proof_fn(std::vector<expr> && consts):
m_constants(consts) {
}

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

@ -25,6 +25,7 @@ public:
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;
};
/**

37
src/library/tactic/tactic.cpp
View file

@ -39,7 +39,7 @@ expr tactic::solve(environment const & env, io_state const & io, context const &
}
tactic id_tactic() {
return mk_simple_tactic([](environment const &, io_state const &, proof_state const & s) -> proof_state {
return mk_tactic1([](environment const &, io_state const &, proof_state const & s) -> proof_state {
return s;
});
}
@ -60,7 +60,7 @@ tactic now_tactic() {
}
tactic trace_tactic(std::string const & msg) {
return mk_simple_tactic([=](environment const &, io_state const & io, proof_state const & s) -> proof_state {
return mk_tactic1([=](environment const &, io_state const & io, proof_state const & s) -> proof_state {
io.get_diagnostic_channel() << msg << "\n";
io.get_diagnostic_channel().get_stream().flush();
return s;
@ -75,8 +75,17 @@ tactic trace_tactic(char const * msg) {
return trace_tactic(std::string(msg));
}
tactic suppress_trace(tactic const & t) {
return mk_tactic([=](environment const & env, io_state const & io, proof_state const & s) -> proof_state_seq {
io_state new_io(io);
std::shared_ptr<output_channel> out(new string_output_channel());
new_io.set_diagnostic_channel(out);
return t(env, new_io, s);
});
}
tactic assumption_tactic() {
return mk_simple_tactic([](environment const &, io_state const &, proof_state const & s) -> proof_state {
return mk_tactic1([](environment const &, io_state const &, proof_state const & s) -> proof_state {
list<std::pair<name, expr>> proofs;
goals new_goals = map_goals(s, [&](name const & ng, goal const & g) -> goal {
expr const & c = g.get_conclusion();
@ -84,7 +93,7 @@ tactic assumption_tactic() {
for (auto const & p : g.get_hypotheses()) {
check_interrupted();
if (p.second == c) {
pr = mk_constant(p.first);
pr = mk_constant(p.first, p.second);
break;
}
}
@ -122,6 +131,14 @@ tactic orelse(tactic const & t1, tactic const & t2) {
});
}
tactic using_params(tactic const & t, options const & opts) {
return mk_tactic([=](environment const & env, io_state const & io, proof_state const & s) -> proof_state_seq {
io_state new_io(io);
new_io.set_options(join(opts, io.get_options()));
return t(env, new_io, s);
});
}
tactic try_for(tactic const & t, unsigned ms, unsigned check_ms) {
return mk_tactic([=](environment const & env, io_state const & io, proof_state const & s) -> proof_state_seq {
return timeout(t(env, io, s), ms, check_ms);
@ -167,16 +184,4 @@ tactic take(tactic const & t, unsigned k) {
return take(k, t(env, io, s));
});
}
tactic force(tactic const & t) {
return mk_tactic([=](environment const & env, io_state const & io, proof_state const & s) -> proof_state_seq {
proof_state_seq r = t(env, io, s);
buffer<proof_state> buf;
for_each(r, [&](proof_state const & s2) {
buf.push_back(s2);
check_interrupted();
});
return to_lazy(to_list(buf.begin(), buf.end()));
});
}
}

51
src/library/tactic/tactic.h
View file

@ -71,8 +71,9 @@ inline proof_state_seq mk_proof_state_seq(F && f) {
}
/**
\brief Create a tactic using the given functor.
\brief Create a tactic that produces exactly one output state.
The functor f must contain the method:
<code>
proof_state operator()(environment const & env, io_state const & io, proof_state const & s)
</code>
@ -80,13 +81,37 @@ inline proof_state_seq mk_proof_state_seq(F && f) {
\remark The functor is invoked on demand.
*/
template<typename F>
tactic mk_simple_tactic(F && f) {
tactic mk_tactic1(F && f) {
return
mk_tactic([=](environment const & env, io_state const & io, proof_state const & s) {
return mk_proof_state_seq([=]() { return some(mk_pair(f(env, io, s), proof_state_seq())); });
});
}
/**
\brief Create a tactic that produces at most one output state.
The functor f must contain the method:
<code>
optional<proof_state> operator()(environment const & env, io_state const & io, proof_state const & s)
</code>
\remark The functor is invoked on demand.
*/
template<typename F>
tactic mk_tactic01(F && f) {
return
mk_tactic([=](environment const & env, io_state const & io, proof_state const & s) {
return mk_proof_state_seq([=]() {
auto r = f(env, io, s);
if (r)
return some(mk_pair(*r, proof_state_seq()));
else
return proof_state_seq::maybe_pair();
});
});
}
inline proof_state_seq to_proof_state_seq(proof_state const & s) {
return mk_proof_state_seq([=]() { return some(mk_pair(s, proof_state_seq())); });
}
@ -123,6 +148,10 @@ tactic trace_tactic(char const * msg);
class sstream;
tactic trace_tactic(sstream const & msg);
tactic trace_tactic(std::string const & msg);
/**
\brief Create a tactic that applies \c t, but suppressing diagnostic messages.
*/
tactic suppress_trace(tactic const & t);
/**
\brief Return a tactic that performs \c t1 followed by \c t2.
@ -135,6 +164,11 @@ inline tactic operator<<(tactic const & t1, tactic const & t2) { return then(t1,
*/
tactic orelse(tactic const & t1, tactic const & t2);
inline tactic operator||(tactic const & t1, tactic const & t2) { return orelse(t1, t2); }
/**
\brief Return a tactic that appies \c t, but using the additional set of options
\c opts.
*/
tactic using_params(tactic const & t, options const & opts);
/**
\brief Return a tactic that tries the tactic \c t for at most \c ms milliseconds.
If the tactic does not terminate in \c ms milliseconds, then the empty
@ -194,19 +228,6 @@ tactic take(tactic const & t, unsigned k);
\brief Syntax sugar for take(t, 1)
*/
inline tactic determ(tactic const & t) { return take(t, 1); }
/**
\brief Return a tactic that forces \c t to produce all
the elements in the resultant sequence.
\remark proof_state_seq is a lazy-list, that is, their
elements are produced on demand. This tactic forces
all the elements in the sequence to be computed eagerly.
\remark The sequence may be infinite. So, consider
combining this tactical with \c take if the sequence
may be infinite or too big.
*/
tactic force(tactic const & t);
/**
\brief Return a tactic that applies the predicate \c p to the input state.
If \c p returns true, then applies \c t1. Otherwise, applies \c t2.

50
src/tests/library/tactic/tactic.cpp
View file

@ -13,11 +13,11 @@ Author: Leonardo de Moura
#include "library/tactic/proof_builder.h"
#include "library/tactic/proof_state.h"
#include "library/tactic/tactic.h"
#include "library/tactic/tactic_exception.h"
#include "library/tactic/boolean.h"
using namespace lean;
tactic loop_tactic() {
return mk_simple_tactic([=](environment const &, io_state const &, proof_state const & s) -> proof_state {
return mk_tactic1([=](environment const &, io_state const &, proof_state const & s) -> proof_state {
while (true) {
check_interrupted();
}
@ -26,12 +26,20 @@ tactic loop_tactic() {
}
tactic set_tactic(std::atomic<bool> * flag) {
return mk_simple_tactic([=](environment const &, io_state const &, proof_state const & s) -> proof_state {
return mk_tactic1([=](environment const &, io_state const &, proof_state const & s) -> proof_state {
*flag = true;
return s;
});
}
tactic show_opts_tactic() {
return mk_tactic1([=](environment const &, io_state const & io, proof_state const & s) -> proof_state {
io.get_diagnostic_channel() << "options: " << io.get_options() << "\n";
io.get_diagnostic_channel().get_stream().flush();
return s;
});
}
static void check_failure(tactic t, environment const & env, io_state const & io, context const & ctx, expr const & ty) {
try {
t.solve(env, io, ctx, ty);
@ -90,9 +98,6 @@ static void tst1() {
(trace_tactic("hello3.1") || trace_tactic("hello3.2")) <<
assumption_tactic()).solve(env, io, ctx, q) << "\n";
std::cout << "------------------\n";
std::cout << "proof 2: " << force(take(repeat_at_most(interleave(id_tactic(), id_tactic()), 100) << trace_tactic("foo") << t,
5)).solve(env, io, ctx, q) << "\n";
std::cout << "proof 2: " << then(cond([](environment const &, io_state const &, proof_state const &) { return true; },
trace_tactic("then branch.1") + trace_tactic("then branch.2"),
trace_tactic("else branch")),
@ -101,11 +106,42 @@ static void tst1() {
std::cout << "proof 2: " << then(when([](environment const &, io_state const &, proof_state const &) { return true; },
trace_tactic("when branch.1") + trace_tactic("when branch.2")),
t).solve(env, io, ctx, q) << "\n";
std::cout << "------------------\n";
std::cout << "proof 2: " << (suppress_trace(trace_tactic("msg1") << trace_tactic("msg2")) <<
trace_tactic("msg3") << t).solve(env, io, ctx, q) << "\n";
std::cout << "------------------\n";
std::cout << "proof 2: " << (show_opts_tactic() << using_params(show_opts_tactic(), options(name({"pp", "colors"}), true)) <<
show_opts_tactic() << t).solve(env, io, ctx, q) << "\n";
std::cout << "done\n";
}
static void tst2() {
environment env;
io_state io(options(), mk_simple_formatter());
import_all(env);
env.add_var("p", Bool);
env.add_var("q", Bool);
expr p = Const("p");
expr q = Const("q");
context ctx;
ctx = extend(ctx, "H1", p);
ctx = extend(ctx, "H2", q);
std::cout << "proof: " << (repeat(conj_tactic()) << assumption_tactic()).solve(env, io, ctx, And(And(p, q), And(p, p)))
<< "\n";
// Theorem to be proved
expr F = Implies(p, Implies(q, And(And(p, q), And(p, p))));
// Tactic
tactic T = repeat(conj_tactic() || imp_tactic()) << assumption_tactic();
// Generate proof using tactic
expr pr = T.solve(env, io, context(), F);
// Print proof
std::cout << pr << "\n";
// Check whether the proof is correct or not.
std::cout << env.infer_type(pr) << "\n";
}
int main() {
tst1();
tst2();
return has_violations() ? 1 : 0;
}