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

feat(library/tactic): new apply tactic

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-07-02 13:14:50 -07:00
parent cc3fb0c51f
commit 0f27856e4a
16 changed files with 114 additions and 138 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
library/standard/tactic.lean
View file

@ -31,4 +31,5 @@ definition trace (s : string) : tactic := tactic_value
infixl `;`:200 := and_then
infixl `|`:100 := or_else
notation `!`:max t:max := repeat t
notation `⟦` t `⟧` := apply t
end

6
src/frontends/lean/elaborator.cpp
View file

@ -663,12 +663,12 @@ public:
mvar = update_mlocal(mvar, subst.instantiate_metavars_wo_jst(mlocal_type(mvar)));
meta = ::lean::mk_app(mvar, locals);
expr type = m_tc.infer(*meta);
proof_state ps = to_proof_state(*meta, type, m_ngen.mk_child());
proof_state ps(goals(goal(*meta, type)), subst, m_ngen.mk_child());
if (optional<tactic> t = get_tactic_for(subst, mvar)) {
proof_state_seq seq = (*t)(m_env, m_ios, ps);
if (auto r = seq.pull()) {
substitution s = r->first.get_subst();
expr v = s.instantiate_metavars_wo_jst(mvar);
subst = r->first.get_subst();
expr v = subst.instantiate_metavars_wo_jst(mvar);
if (has_metavar(v)) {
display_unsolved_proof_state(mvar, r->first, "unsolved subgoals");
} else {

122
src/library/tactic/apply_tactic.cpp
View file

@ -37,84 +37,66 @@ bool collect_simple_metas(expr const & e, buffer<expr> & result) {
return !failed;
}
tactic apply_tactic(expr const & e) {
return tactic([=](environment const &, io_state const &, proof_state const & s) {
std::cout << e << "\n";
return s;
#if 0
if (s.is_final_state()) {
return proof_state_seq();
unsigned get_expect_num_args(type_checker & tc, expr e) {
unsigned r = 0;
while (true) {
e = tc.whnf(e);
if (!is_pi(e))
return r;
e = binding_body(e);
r++;
}
}
void collect_simple_meta(expr const & e, buffer<expr> & metas) {
for_each(e, [&](expr const & e, unsigned) {
if (is_meta(e)) {
if (is_simple_meta(e))
metas.push_back(e);
return false; /* do not visit its type */
}
goals const & gs = s.get_goals();
name gname = head(gs).first;
goal g = head(gs).second;
goals rest_gs = tail(gs);
expr const & C = g.get_conclusion();
name_generator ngen = s.ngen();
return has_metavar(e);
});
}
tactic apply_tactic(expr const & _e) {
return tactic([=](environment const & env, io_state const & ios, proof_state const & s) {
goals const & gs = s.get_goals();
if (empty(gs))
return proof_state_seq();
name_generator ngen = s.get_ngen();
type_checker tc(env, ngen.mk_child());
expr new_e = e;
expr new_e_type = tc.infer(new_e);
buffer<expr> meta_buffer;
if (!collect_simple_metas(new_e, meta_buffer))
return proof_state_seq();
// add more metavariables while new_e_type is a Pi
while (is_pi(new_e_type)) {
expr meta = g.mk_meta(ngen.next(), binding_domain(new_e_type));
meta_buffer.push_back(meta);
new_e = mk_app(new_e, meta);
new_e_type = instantiate(binding_body(new_e_type), meta);
goal g = head(gs);
goals tail_gs = tail(gs);
expr t = g.get_type();
expr e = _e;
expr e_t = tc.infer(e);
unsigned num_t = get_expect_num_args(tc, t);
unsigned num_e_t = get_expect_num_args(tc, e_t);
if (num_t > num_e_t)
return proof_state_seq(); // no hope to unify then
for (unsigned i = 0; i < num_e_t - num_t; i++) {
e_t = tc.whnf(e_t);
expr meta = g.mk_meta(ngen.next(), binding_domain(e_t));
e = mk_app(e, meta);
e_t = instantiate(binding_body(e_t), meta);
}
list<expr> metas = to_list(meta_buffer.begin(), meta_buffer.end());
// TODO(Leo): we should use unifier plugin
lazy_list<substitution> substs = unify(env, C, new_e_type, ngen.mk_child(), ios.get_options());
lazy_list<substitution> substs = unify(env, t, e_t, ngen.mk_child(), s.get_subst(), ios.get_options());
return map2<proof_state>(substs, [=](substitution const & subst) -> proof_state {
// apply substitution to remaining goals
name_generator new_ngen(ngen);
type_checker tc(env, new_ngen.mk_child());
goals new_gs = map(rest_gs, [&](named_goal const & ng) {
return named_goal(ng.first, ng.second.instantiate_metavars(subst));
});
expr P = subst.instantiate_metavars_wo_jst(new_e);
goal tmp_g = g.instantiate_metavars(subst);
unsigned subgoal_idx = 1;
buffer<std::pair<name, expr>> trace_buffer;
// add unassigned metavariables as new goals
buffer<named_goal> subgoals;
for (expr const & meta : metas) {
if (!subst.is_assigned(get_app_fn(meta))) {
name new_gname(gname, subgoal_idx);
expr new_C = subst.instantiate_metavars_wo_jst(tc.infer(meta));
goal new_g(tmp_g.get_hypotheses(), new_C);
subgoals.emplace_back(new_gname, new_g);
trace_buffer.emplace_back(new_gname, meta);
subgoal_idx++;
}
expr new_e = subst.instantiate_metavars_wo_jst(e);
substitution new_subst = subst.assign(g.get_name(), g.abstract(new_e));
buffer<expr> metas;
collect_simple_meta(new_e, metas);
goals new_gs = tail_gs;
unsigned i = metas.size();
while (i > 0) {
--i;
new_gs = cons(goal(metas[i], subst.instantiate_metavars_wo_jst(tc.infer(metas[i]))), new_gs);
}
new_gs = to_list(subgoals.begin(), subgoals.end(), new_gs);
list<std::pair<name, expr>> trace = to_list(trace_buffer.begin(), trace_buffer.end());
proof_builder pb = s.get_pb();
proof_builder new_pb([=](proof_map const & m, substitution const & pb_subst) {
proof_map new_m(m);
substitution new_subst;
for (auto const & p : trace) {
expr pr = find(new_m, p.first);
expr meta = p.second;
buffer<expr> meta_args;
expr mvar = get_app_args(meta, meta_args);
unsigned i = meta_args.size();
while (i > 0) {
--i;
pr = Fun(meta_args[i], pr);
}
new_subst = new_subst.assign(mlocal_name(mvar), pr, justification());
new_m.erase(p.first);
}
new_m.insert(gname, new_subst.instantiate_metavars_wo_jst(P));
return pb(new_m, pb_subst);
});
return proof_state(s, new_gs, new_pb, new_ngen);
return proof_state(new_gs, new_subst, new_ngen);
});
#endif
});
}

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

@ -175,6 +175,7 @@ tactic take(tactic const & t, unsigned k) {
tactic assumption_tactic() {
return tactic01([](environment const &, io_state const &, proof_state const & s) -> optional<proof_state> {
substitution subst = s.get_subst();
bool solved = false;
goals new_gs = map_goals(s, [&](goal const & g) -> optional<goal> {
expr const & t = g.get_type();
optional<expr> h;
@ -187,13 +188,17 @@ tactic assumption_tactic() {
}
}
if (h) {
subst = subst.assign(g.get_mvar(), g.abstract(*h), justification());
subst = subst.assign(g.get_mvar(), g.abstract(*h), justification());
solved = true;
return optional<goal>();
} else {
return some(g);
}
});
return some(proof_state(s, new_gs, subst));
if (solved)
return some(proof_state(s, new_gs, subst));
else
return none_proof_state();
});
}

49
src/library/unifier.cpp
View file

@ -1186,8 +1186,7 @@ lazy_list<substitution> unify(environment const & env, unsigned num_cs, constrai
}
lazy_list<substitution> unify(environment const & env, expr const & lhs, expr const & rhs, name_generator const & ngen, unifier_plugin const & p,
unsigned max_steps) {
substitution s;
substitution const & s, unsigned max_steps) {
name_generator new_ngen(ngen);
type_checker tc(env, new_ngen.mk_child());
if (!tc.is_def_eq(lhs, rhs))
@ -1204,16 +1203,18 @@ lazy_list<substitution> unify(environment const & env, expr const & lhs, expr co
}
lazy_list<substitution> unify(environment const & env, expr const & lhs, expr const & rhs, name_generator const & ngen, unifier_plugin const & p,
options const & o) {
return unify(env, lhs, rhs, ngen, p, get_unifier_max_steps(o));
substitution const & s, options const & o) {
return unify(env, lhs, rhs, ngen, p, s, get_unifier_max_steps(o));
}
lazy_list<substitution> unify(environment const & env, expr const & lhs, expr const & rhs, name_generator const & ngen, unsigned max_steps) {
return unify(env, lhs, rhs, ngen, [](constraint const &, name_generator const &) { return lazy_list<constraints>(); }, max_steps);
lazy_list<substitution> unify(environment const & env, expr const & lhs, expr const & rhs, name_generator const & ngen,
substitution const & s, unsigned max_steps) {
return unify(env, lhs, rhs, ngen, [](constraint const &, name_generator const &) { return lazy_list<constraints>(); }, s, max_steps);
}
lazy_list<substitution> unify(environment const & env, expr const & lhs, expr const & rhs, name_generator const & ngen, options const & o) {
return unify(env, lhs, rhs, ngen, get_unifier_max_steps(o));
lazy_list<substitution> unify(environment const & env, expr const & lhs, expr const & rhs, name_generator const & ngen,
substitution const & s, options const & o) {
return unify(env, lhs, rhs, ngen, s, get_unifier_max_steps(o));
}
static int unify_simple(lua_State * L) {
@ -1335,39 +1336,15 @@ static int unify(lua_State * L) {
lazy_list<substitution> r;
environment const & env = to_environment(L, 1);
if (is_expr(L, 2)) {
if (nargs == 3)
r = unify(env, to_expr(L, 2), to_expr(L, 3), name_generator(g_tmp_prefix));
else if (nargs == 4 && is_options(L, 4))
r = unify(env, to_expr(L, 2), to_expr(L, 3), name_generator(g_tmp_prefix), to_options(L, 4));
else if (nargs == 4 && is_name_generator(L, 4))
r = unify(env, to_expr(L, 2), to_expr(L, 3), to_name_generator(L, 4));
else if (nargs == 4)
r = unify(env, to_expr(L, 2), to_expr(L, 3), name_generator(g_tmp_prefix), to_unifier_plugin(L, 4));
else if (nargs == 5 && is_name_generator(L, 4) && is_options(L, 5))
r = unify(env, to_expr(L, 2), to_expr(L, 3), to_name_generator(L, 4), to_options(L, 5));
else if (nargs == 5 && is_options(L, 5))
r = unify(env, to_expr(L, 2), to_expr(L, 3), name_generator(g_tmp_prefix), to_unifier_plugin(L, 4), to_options(L, 5));
else if (nargs == 5)
r = unify(env, to_expr(L, 2), to_expr(L, 3), to_name_generator(L, 4), to_unifier_plugin(L, 5));
if (nargs == 6 && is_substitution(L, 5))
r = unify(env, to_expr(L, 2), to_expr(L, 3), to_name_generator(L, 4), to_substitution(L, 5), to_options(L, 6));
else
r = unify(env, to_expr(L, 2), to_expr(L, 3), to_name_generator(L, 4), to_unifier_plugin(L, 5), to_options(L, 6));
r = unify(env, to_expr(L, 2), to_expr(L, 3), to_name_generator(L, 4), to_unifier_plugin(L, 5), to_substitution(L, 6), to_options(L, 7));
} else {
buffer<constraint> cs;
to_constraint_buffer(L, 2, cs);
if (nargs == 2)
r = unify(env, cs.size(), cs.data(), name_generator(g_tmp_prefix));
else if (nargs == 3 && is_name_generator(L, 3))
r = unify(env, cs.size(), cs.data(), to_name_generator(L, 3));
else if (nargs == 3 && is_options(L, 3))
r = unify(env, cs.size(), cs.data(), name_generator(g_tmp_prefix), to_options(L, 3));
else if (nargs == 3)
r = unify(env, cs.size(), cs.data(), name_generator(g_tmp_prefix), to_unifier_plugin(L, 3));
else if (nargs == 4 && is_name_generator(L, 3) && is_options(L, 4))
if (nargs == 4 && is_options(L, 4))
r = unify(env, cs.size(), cs.data(), to_name_generator(L, 3), to_options(L, 4));
else if (nargs == 4 && is_options(L, 4))
r = unify(env, cs.size(), cs.data(), name_generator(g_tmp_prefix), to_unifier_plugin(L, 3), to_options(L, 4));
else if (nargs == 4)
r = unify(env, cs.size(), cs.data(), to_name_generator(L, 3), to_unifier_plugin(L, 4));
else
r = unify(env, cs.size(), cs.data(), to_name_generator(L, 3), to_unifier_plugin(L, 4), to_options(L, 5));
}

8
src/library/unifier.h
View file

@ -52,13 +52,13 @@ lazy_list<substitution> unify(environment const & env, unsigned num_cs, constrai
lazy_list<substitution> unify(environment const & env, unsigned num_cs, constraint const * cs, name_generator const & ngen,
options const & o);
lazy_list<substitution> unify(environment const & env, expr const & lhs, expr const & rhs, name_generator const & ngen, unifier_plugin const & p,
unsigned max_steps = LEAN_DEFAULT_UNIFIER_MAX_STEPS);
substitution const & s = substitution(), unsigned max_steps = LEAN_DEFAULT_UNIFIER_MAX_STEPS);
lazy_list<substitution> unify(environment const & env, expr const & lhs, expr const & rhs, name_generator const & ngen,
unsigned max_sharing = LEAN_DEFAULT_UNIFIER_MAX_STEPS);
substitution const & s = substitution(), unsigned max_steps = LEAN_DEFAULT_UNIFIER_MAX_STEPS);
lazy_list<substitution> unify(environment const & env, expr const & lhs, expr const & rhs, name_generator const & ngen, unifier_plugin const & p,
options const & o);
substitution const & s, options const & o);
lazy_list<substitution> unify(environment const & env, expr const & lhs, expr const & rhs, name_generator const & ngen,
options const & o);
substitution const & s, options const & o);
class unifier_exception : public exception {
justification m_jst;

12
tests/lean/run/tactic10.lean
View file

@ -1,7 +1,9 @@
import logic
import standard
using tactic
exit -- TODO
theorem tst (a b : Bool) (H : a ↔ b) : b ↔ a
:= by (apply iff_intro,
assume Hb, iff_mp_right H Hb,
assume Ha, iff_mp_left H Ha)
:= by apply iff_intro;
⟦ assume Hb, iff_mp_right H Hb ⟧;
⟦ assume Ha, iff_mp_left H Ha ⟧
check tst

13
tests/lean/run/tactic7.lean
View file

@ -1,5 +1,12 @@
import logic
import standard
using tactic
exit -- TODO
theorem tst {A B : Bool} (H1 : A) (H2 : B) : A ∧ B ∧ A
:= by (print, apply and_intro, print, exact, apply and_intro, print, !exact)
:= by apply and_intro; state; exact; apply and_intro; !exact
check tst
theorem tst2 {A B : Bool} (H1 : A) (H2 : B) : A ∧ B ∧ A
:= by !((apply @and_intro | exact) ; trace "STEP"; state; trace "----------")
check tst2

11
tests/lean/run/tactic8.lean
View file

@ -1,8 +1,9 @@
import logic
import standard
using tactic
exit -- TODO
theorem tst {A B : Bool} (H1 : A) (H2 : B) : A ∧ B ∧ A
:= by (apply and_intro,
show A, from H1,
show B ∧ A, from and_intro H2 H1)
:= by (apply @and_intro;
apply (show A, from H1);
apply (show B ∧ A, from and_intro H2 H1))
check @tst

7
tests/lean/run/tactic9.lean
View file

@ -1,5 +1,6 @@
import logic
import standard
using tactic
exit -- TODO
theorem tst {A B : Bool} (H1 : A) (H2 : B) : ((fun x : Bool, x) A) ∧ B ∧ A
:= by (apply and_intro, beta, exact, apply and_intro, !exact)
:= by apply and_intro; beta; exact; apply and_intro; !exact

2
tests/lua/unify2.lua
View file

@ -1,6 +1,6 @@
function test_unify(env, lhs, rhs, num_s)
print(tostring(lhs) .. " =?= " .. tostring(rhs) .. ", expected: " .. tostring(num_s))
local ss = unify(env, lhs, rhs)
local ss = unify(env, lhs, rhs, name_generator(), substitution(), options())
local n = 0
for s in ss do
print("solution: ")

4
tests/lua/unify3.lua
View file

@ -15,7 +15,7 @@ local m = mk_metavar("m", mk_metavar("m_ty", mk_sort(mk_meta_univ("u"))))
local cs = { mk_eq_cnstr(carrier(m), real) }
local o = options({"unifier", "use_exceptions"}, false)
print(o)
assert(not unify(env, cs, o)())
assert(not unify(env, cs, name_generator(), o)())
function hint(c, ngen)
local lhs = c:lhs()
@ -44,4 +44,4 @@ function display_solutions(ss)
end
end
display_solutions(unify(env, cs, hint, o))
display_solutions(unify(env, cs, name_generator(), hint, o))

2
tests/lua/unify4.lua
View file

@ -1,6 +1,6 @@
function test_unify(env, m, lhs, rhs, num_s)
print(tostring(lhs) .. " =?= " .. tostring(rhs) .. ", expected: " .. tostring(num_s))
local ss = unify(env, lhs, rhs)
local ss = unify(env, lhs, rhs, name_generator(), substitution(), options())
local n = 0
for s in ss do
print("solution: " .. tostring(s:instantiate(m)))

2
tests/lua/unify5.lua
View file

@ -34,4 +34,4 @@ cs = { mk_eq_cnstr(m1, f(m2, f(m3, m4))),
mk_choice_cnstr(m4, function(e, s, ngen) return {a, b} end)
}
display_solutions(m1, unify(env, cs, o))
display_solutions(m1, unify(env, cs, name_generator(), o))

2
tests/lua/unify6.lua
View file

@ -24,4 +24,4 @@ cs = { mk_level_eq_cnstr(m1, max_univ(m2, max_univ(m2, l1, 1))),
mk_level_eq_cnstr(m3+1, m2+1)
}
display_solutions(m1, unify(env, cs, o))
display_solutions(m1, unify(env, cs, name_generator(), o))

2
tests/lua/unify7.lua
View file

@ -11,7 +11,7 @@ local m = mk_metavar("m", mk_arrow(N, N, Type))
local cs = { mk_eq_cnstr(m(a, a), t) }
local o = options({"unifier", "use_exceptions"}, false)
ss = unify(env, cs, o)
ss = unify(env, cs, name_generator(), o)
local n = 0
for s in ss do
print("solution: " .. tostring(s:instantiate(m)))