feat(library/tactic): add unfold tactic
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
parent
737e634556
commit
ca53a5a1cc
5 changed files with 82 additions and 5 deletions
|
@ -9,8 +9,6 @@ Author: Leonardo de Moura
|
||||||
#include "kernel/type_checker.h"
|
#include "kernel/type_checker.h"
|
||||||
#include "library/basic_thms.h"
|
#include "library/basic_thms.h"
|
||||||
|
|
||||||
#include "kernel/kernel_exception.h"
|
|
||||||
|
|
||||||
namespace lean {
|
namespace lean {
|
||||||
|
|
||||||
MK_CONSTANT(trivial, name("Trivial"));
|
MK_CONSTANT(trivial, name("Trivial"));
|
||||||
|
|
|
@ -12,6 +12,8 @@ Author: Leonardo de Moura
|
||||||
#include "util/sstream.h"
|
#include "util/sstream.h"
|
||||||
#include "util/interrupt.h"
|
#include "util/interrupt.h"
|
||||||
#include "util/lazy_list_fn.h"
|
#include "util/lazy_list_fn.h"
|
||||||
|
#include "kernel/replace_visitor.h"
|
||||||
|
#include "kernel/instantiate.h"
|
||||||
#include "library/kernel_bindings.h"
|
#include "library/kernel_bindings.h"
|
||||||
#include "library/tactic/tactic.h"
|
#include "library/tactic/tactic.h"
|
||||||
|
|
||||||
|
@ -180,7 +182,7 @@ tactic suppress_trace(tactic const & t) {
|
||||||
tactic assumption_tactic() {
|
tactic assumption_tactic() {
|
||||||
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> {
|
||||||
list<std::pair<name, expr>> proofs;
|
list<std::pair<name, expr>> proofs;
|
||||||
goals new_goals = map_goals(s, [&](name const & ng, goal const & g) -> goal {
|
goals new_gs = map_goals(s, [&](name const & gname, goal const & g) -> goal {
|
||||||
expr const & c = g.get_conclusion();
|
expr const & c = g.get_conclusion();
|
||||||
expr pr;
|
expr pr;
|
||||||
for (auto const & p : g.get_hypotheses()) {
|
for (auto const & p : g.get_hypotheses()) {
|
||||||
|
@ -191,7 +193,7 @@ tactic assumption_tactic() {
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
if (pr) {
|
if (pr) {
|
||||||
proofs.emplace_front(ng, pr);
|
proofs.emplace_front(gname, pr);
|
||||||
return goal();
|
return goal();
|
||||||
} else {
|
} else {
|
||||||
return g;
|
return g;
|
||||||
|
@ -200,7 +202,7 @@ tactic assumption_tactic() {
|
||||||
if (empty(proofs))
|
if (empty(proofs))
|
||||||
return none_proof_state();
|
return none_proof_state();
|
||||||
proof_builder new_pb = add_proofs(s.get_proof_builder(), proofs);
|
proof_builder new_pb = add_proofs(s.get_proof_builder(), proofs);
|
||||||
return some(proof_state(s, new_goals, new_pb));
|
return some(proof_state(s, new_gs, new_pb));
|
||||||
});
|
});
|
||||||
}
|
}
|
||||||
|
|
||||||
|
@ -348,6 +350,60 @@ tactic focus(tactic const & t, int i) {
|
||||||
});
|
});
|
||||||
}
|
}
|
||||||
|
|
||||||
|
class unfold_fn : public replace_visitor {
|
||||||
|
protected:
|
||||||
|
name const & m_name;
|
||||||
|
expr const & m_def;
|
||||||
|
bool m_unfolded;
|
||||||
|
|
||||||
|
virtual expr visit_constant(expr const & c, context const &) {
|
||||||
|
if (const_name(c) == m_name) {
|
||||||
|
m_unfolded = true;
|
||||||
|
return m_def;
|
||||||
|
} else {
|
||||||
|
return c;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
virtual expr visit_app(expr const & e, context const & ctx) {
|
||||||
|
expr const & f = arg(e, 0);
|
||||||
|
if (is_constant(f) && const_name(f) == m_name) {
|
||||||
|
buffer<expr> new_args;
|
||||||
|
for (unsigned i = 0; i < num_args(e); i++)
|
||||||
|
new_args.push_back(visit(arg(e, i), ctx));
|
||||||
|
if (is_lambda(new_args[0]))
|
||||||
|
return apply_beta(new_args[0], new_args.size() - 1, new_args.data() + 1);
|
||||||
|
else
|
||||||
|
return mk_app(new_args);
|
||||||
|
} else {
|
||||||
|
return replace_visitor::visit_app(e, ctx);
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
public:
|
||||||
|
unfold_fn(name const & n, expr const & d):m_name(n), m_def(d), m_unfolded(false) {}
|
||||||
|
bool unfolded() const { return m_unfolded; }
|
||||||
|
};
|
||||||
|
|
||||||
|
tactic unfold_tactic(name const & n) {
|
||||||
|
return mk_tactic01([=](environment const & env, io_state const &, proof_state const & s) -> optional<proof_state> {
|
||||||
|
object const & obj = env.find_object(n);
|
||||||
|
if (!obj || !obj.is_definition())
|
||||||
|
return none_proof_state(); // tactic failed
|
||||||
|
unfold_fn fn(n, obj.get_value());
|
||||||
|
goals new_gs = map_goals(s, [&](name const &, goal const & g) -> goal {
|
||||||
|
hypotheses new_hs = map(g.get_hypotheses(), [&](hypothesis const & h) { return hypothesis(h.first, fn(h.second)); });
|
||||||
|
expr new_c = fn(g.get_conclusion());
|
||||||
|
return goal(new_hs, new_c);
|
||||||
|
});
|
||||||
|
if (fn.unfolded()) {
|
||||||
|
return proof_state(s, new_gs);
|
||||||
|
} else {
|
||||||
|
return none_proof_state();
|
||||||
|
}
|
||||||
|
});
|
||||||
|
}
|
||||||
|
|
||||||
DECL_UDATA(proof_state_seq)
|
DECL_UDATA(proof_state_seq)
|
||||||
|
|
||||||
static const struct luaL_Reg proof_state_seq_m[] = {
|
static const struct luaL_Reg proof_state_seq_m[] = {
|
||||||
|
@ -622,6 +678,7 @@ static int mk_fail_tactic(lua_State * L) { return push_tactic(L, fail_ta
|
||||||
static int mk_trace_tactic(lua_State * L) { return push_tactic(L, trace_tactic(luaL_checkstring(L, 1))); }
|
static int mk_trace_tactic(lua_State * L) { return push_tactic(L, trace_tactic(luaL_checkstring(L, 1))); }
|
||||||
static int mk_assumption_tactic(lua_State * L) { return push_tactic(L, assumption_tactic()); }
|
static int mk_assumption_tactic(lua_State * L) { return push_tactic(L, assumption_tactic()); }
|
||||||
static int mk_trace_state_tactic(lua_State * L) { return push_tactic(L, trace_state_tactic()); }
|
static int mk_trace_state_tactic(lua_State * L) { return push_tactic(L, trace_state_tactic()); }
|
||||||
|
static int mk_unfold_tactic(lua_State * L) { return push_tactic(L, unfold_tactic(to_name_ext(L, 1))); }
|
||||||
|
|
||||||
static const struct luaL_Reg tactic_m[] = {
|
static const struct luaL_Reg tactic_m[] = {
|
||||||
{"__gc", tactic_gc}, // never throws
|
{"__gc", tactic_gc}, // never throws
|
||||||
|
@ -673,6 +730,7 @@ void open_tactic(lua_State * L) {
|
||||||
SET_GLOBAL_FUN(mk_trace_state_tactic, "show_tactic");
|
SET_GLOBAL_FUN(mk_trace_state_tactic, "show_tactic");
|
||||||
SET_GLOBAL_FUN(mk_assumption_tactic, "assumption_tactic");
|
SET_GLOBAL_FUN(mk_assumption_tactic, "assumption_tactic");
|
||||||
SET_GLOBAL_FUN(mk_assumption_tactic, "assump_tactic");
|
SET_GLOBAL_FUN(mk_assumption_tactic, "assump_tactic");
|
||||||
|
SET_GLOBAL_FUN(mk_unfold_tactic, "unfold_tactic");
|
||||||
SET_GLOBAL_FUN(mk_lua_tactic01, "tactic");
|
SET_GLOBAL_FUN(mk_lua_tactic01, "tactic");
|
||||||
|
|
||||||
// HOL-like tactic names
|
// HOL-like tactic names
|
||||||
|
|
|
@ -287,6 +287,10 @@ tactic focus(tactic const & t, name const & gname);
|
||||||
*/
|
*/
|
||||||
tactic focus(tactic const & t, int i);
|
tactic focus(tactic const & t, int i);
|
||||||
inline tactic focus(tactic const & t) { return focus(t, 1); }
|
inline tactic focus(tactic const & t) { return focus(t, 1); }
|
||||||
|
/**
|
||||||
|
\brief Return a tactic that unfolds the definition named \c n.
|
||||||
|
*/
|
||||||
|
tactic unfold_tactic(name const & n);
|
||||||
|
|
||||||
UDATA_DEFS_CORE(proof_state_seq)
|
UDATA_DEFS_CORE(proof_state_seq)
|
||||||
UDATA_DEFS(tactic);
|
UDATA_DEFS(tactic);
|
||||||
|
|
11
tests/lean/tactic9.lean
Normal file
11
tests/lean/tactic9.lean
Normal file
|
@ -0,0 +1,11 @@
|
||||||
|
Definition f(a : Bool) : Bool := not a.
|
||||||
|
|
||||||
|
Theorem T (a b : Bool) : a \/ b => (f b) => a := _.
|
||||||
|
apply imp_tactic
|
||||||
|
apply imp_tactic
|
||||||
|
apply disj_hyp_tactic
|
||||||
|
apply (** unfold_tactic("f") **)
|
||||||
|
apply assumption_tactic
|
||||||
|
apply absurd_tactic
|
||||||
|
done
|
||||||
|
Show Environment 1.
|
6
tests/lean/tactic9.lean.expected.out
Normal file
6
tests/lean/tactic9.lean.expected.out
Normal file
|
@ -0,0 +1,6 @@
|
||||||
|
Set: pp::colors
|
||||||
|
Set: pp::unicode
|
||||||
|
Defined: f
|
||||||
|
Proved: T
|
||||||
|
Theorem T (a b : Bool) : a ∨ b ⇒ (f b) ⇒ a :=
|
||||||
|
Discharge (λ H : a ∨ b, Discharge (λ H::1 : f b, DisjCases H (λ H : a, H) (λ H : b, AbsurdImpAny b a H H::1)))
|
Loading…
Add table
Reference in a new issue