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

feat(library/tactic): add improved 'subst' tactic

Browse source
This commit is contained in:
Leonardo de Moura 2015-05-25 15:03:59 -07:00
parent 24b35eefe6
commit a3f23d5233
6 changed files with 235 additions and 83 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -6,6 +6,6 @@ assert_tactic.cpp clear_tactic.cpp expr_to_tactic.cpp location.cpp
rewrite_tactic.cpp util.cpp class_instance_synth.cpp init_module.cpp
change_tactic.cpp check_expr_tactic.cpp let_tactic.cpp contradiction_tactic.cpp
exfalso_tactic.cpp constructor_tactic.cpp injection_tactic.cpp
congruence_tactic.cpp relation_tactics.cpp induction_tactic.cpp)
congruence_tactic.cpp relation_tactics.cpp induction_tactic.cpp subst_tactic.cpp)
target_link_libraries(tactic ${LEAN_LIBS})

3
src/library/tactic/init_module.cpp
View file

@ -30,6 +30,7 @@ Author: Leonardo de Moura
#include "library/tactic/congruence_tactic.h"
#include "library/tactic/relation_tactics.h"
#include "library/tactic/induction_tactic.h"
#include "library/tactic/subst_tactic.h"
namespace lean {
void initialize_tactic_module() {
@ -59,9 +60,11 @@ void initialize_tactic_module() {
initialize_congruence_tactic();
initialize_relation_tactics();
initialize_induction_tactic();
initialize_subst_tactic();
}
void finalize_tactic_module() {
finalize_subst_tactic();
finalize_induction_tactic();
finalize_relation_tactics();
finalize_congruence_tactic();

81
src/library/tactic/rewrite_tactic.cpp
View file

@ -1537,81 +1537,6 @@ tactic mk_rewrite_tactic(elaborate_fn const & elab, buffer<expr> const & elems)
});
}
tactic mk_simple_rewrite_tactic(buffer<expr> const & rw_elems) {
auto fn = [=](environment const & env, io_state const & ios, proof_state const & s) {
// dummy elaborator
auto elab = [](goal const &, name_generator const &, expr const & H,
optional<expr> const &, substitution const & s, bool) -> elaborate_result {
return elaborate_result(H, s, constraints());
};
return rewrite_fn(env, ios, elab, s)(rw_elems);
};
return tactic(fn);
}
tactic mk_simple_rewrite_tactic(expr const & rw_elem) {
buffer<expr> rw_elems;
rw_elems.push_back(rw_elem);
return mk_simple_rewrite_tactic(rw_elems);
}
tactic mk_subst_tactic(list<name> const & ids) {
auto fn = [=](environment const & env, io_state const & ios, proof_state const & s) {
if (!ids)
return proof_state_seq(s);
goals const & gs = s.get_goals();
if (empty(gs))
return proof_state_seq();
goal const & g = head(gs);
name const & id = head(ids);
auto apply_rewrite = [&](expr const & H, bool symm) {
tactic tac = then(mk_simple_rewrite_tactic(mk_rewrite_once(none_expr(), H, symm, location::mk_everywhere())),
then(clear_tactic(local_pp_name(H)),
mk_subst_tactic(tail(ids))));
return tac(env, ios, s);
};
optional<pair<expr, unsigned>> p = g.find_hyp(id);
if (!p) {
throw_tactic_exception_if_enabled(s, sstream() << "invalid 'subst' tactic, there is no hypothesis named '"
<< id << "'");
return proof_state_seq();
}
expr const & H = p->first;
expr lhs, rhs;
if (is_eq(mlocal_type(H), lhs, rhs)) {
if (is_local(lhs)) {
return apply_rewrite(H, false);
} else if (is_local(rhs)) {
return apply_rewrite(H, true);
} else {
throw_tactic_exception_if_enabled(s, sstream() << "invalid 'subst' tactic, hypothesis '"
<< id << "' is not of the form (x = t) or (t = x)");
return proof_state_seq();
}
} else if (is_local(H)) {
expr const & x = H;
buffer<expr> hyps;
g.get_hyps(hyps);
for (expr const & H : hyps) {
expr lhs, rhs;
if (is_eq(mlocal_type(H), lhs, rhs)) {
if (is_local(lhs) && mlocal_name(lhs) == mlocal_name(x)) {
return apply_rewrite(H, false);
} else if (is_local(rhs) && mlocal_name(rhs) == mlocal_name(x)) {
return apply_rewrite(H, true);
}
}
}
}
throw_tactic_exception_if_enabled(s, sstream() << "invalid 'subst' tactic, hypothesis '"
<< id << "' is not a variable nor an equation of the form (x = t) or (t = x)");
return proof_state_seq();
};
return tactic(fn);
}
void initialize_rewrite_tactic() {
g_rewriter_max_iterations = new name{"rewriter", "max_iter"};
register_unsigned_option(*g_rewriter_max_iterations, LEAN_DEFAULT_REWRITER_MAX_ITERATIONS,
@ -1681,12 +1606,6 @@ void initialize_rewrite_tactic() {
bool fail_if_metavars = true;
return then(mk_rewrite_tactic(elab, args), try_tactic(refl_tactic(elab, fail_if_metavars)));
});
register_tac(name{"tactic", "subst"},
[](type_checker &, elaborate_fn const & elab, expr const & e, pos_info_provider const *) {
buffer<name> ns;
get_tactic_id_list_elements(app_arg(e), ns, "invalid 'subst' tactic, list of identifiers expected");
return then(mk_subst_tactic(to_list(ns)), try_tactic(refl_tactic(elab)));
});
}
void finalize_rewrite_tactic() {

194
src/library/tactic/subst_tactic.cpp Normal file
View file

@ -0,0 +1,194 @@
/*
Copyright (c) 2015 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include <algorithm>
#include "kernel/abstract.h"
#include "kernel/instantiate.h"
#include "kernel/inductive/inductive.h"
#include "kernel/kernel_exception.h"
#include "library/constants.h"
#include "library/reducible.h"
#include "library/util.h"
#include "library/locals.h"
#include "library/tactic/expr_to_tactic.h"
#include "library/tactic/relation_tactics.h"
#include "library/tactic/proof_state.h"
namespace lean {
static void split_deps(buffer<expr> const & hyps, expr const & x, expr const & h,
buffer<expr> & non_deps, buffer<expr> & deps) {
for (expr const & hyp : hyps) {
if (hyp == h || hyp == x) {
// we clear h and x
} else if (depends_on(hyp, x) || depends_on(hyp, h) || depends_on_any(hyp, deps)) {
deps.push_back(hyp);
} else {
non_deps.push_back(hyp);
}
}
}
tactic mk_subst_tactic_core(name const & h_name, bool symm) {
auto fn = [=](environment const & env, io_state const &, proof_state const & s) {
goals const & gs = s.get_goals();
if (empty(gs))
return none_proof_state();
goal g = head(gs);
auto opt_h = g.find_hyp_from_internal_name(h_name);
if (!opt_h)
return none_proof_state();
expr const & h = opt_h->first;
expr lhs, rhs;
if (!is_eq(mlocal_type(h), lhs, rhs))
return none_proof_state();
name_generator ngen = s.get_ngen();
auto tc = mk_type_checker(env, ngen.mk_child());
if (symm)
std::swap(lhs, rhs);
if (!is_local(lhs))
return none_proof_state();
buffer<expr> hyps, deps, non_deps;
g.get_hyps(hyps);
split_deps(hyps, lhs, h, non_deps, deps);
// revert dependencies
expr type = Pi(deps, g.get_type());
// substitute
bool has_dep_elim = inductive::has_dep_elim(env, get_eq_name());
expr motive, new_type;
new_type = instantiate(abstract_local(type, mlocal_name(lhs)), rhs);
if (has_dep_elim) {
new_type = instantiate(abstract_local(new_type, mlocal_name(h)), mk_refl(*tc, rhs));
if (symm) {
motive = Fun(lhs, Fun(h, type));
} else {
expr Heq = mk_local(ngen.next(), local_pp_name(h), mk_eq(*tc, rhs, lhs), binder_info());
motive = Fun(lhs, Fun(Heq, type));
}
} else {
motive = Fun(lhs, type);
}
buffer<expr> new_hyps;
buffer<expr> intros_hyps;
new_hyps.append(non_deps);
// reintroduce dependencies
expr new_goal_type = new_type;
for (expr const & d : deps) {
if (!is_pi(new_goal_type))
return none_proof_state();
expr new_h = mk_local(ngen.next(), local_pp_name(d), binding_domain(new_goal_type), binder_info());
new_hyps.push_back(new_h);
intros_hyps.push_back(new_h);
new_goal_type = instantiate(binding_body(new_goal_type), new_h);
}
// create new goal
expr new_metavar = mk_metavar(ngen.next(), Pi(new_hyps, new_goal_type));
expr new_meta_core = mk_app(new_metavar, non_deps);
expr new_meta = mk_app(new_meta_core, intros_hyps);
goal new_g(new_meta, new_goal_type);
// create eqrec term
substitution new_subst = s.get_subst();
expr major = symm ? h : mk_symm(*tc, h);
expr minor = new_meta_core;
expr A = tc->infer(lhs).first;
level l1 = sort_level(tc->ensure_type(new_type).first);
level l2 = sort_level(tc->ensure_type(A).first);
expr eqrec = mk_app({mk_constant(get_eq_rec_name(), {l1, l2}), A, rhs, motive, minor, lhs, major});
if (has_dep_elim) {
try {
check_term(env, g.abstract(eqrec));
} catch (kernel_exception & ex) {
if (!s.report_failure())
return none_proof_state();
std::shared_ptr<kernel_exception> saved_ex(static_cast<kernel_exception*>(ex.clone()));
throw tactic_exception("rewrite step failed", none_expr(), s,
[=](formatter const & fmt) {
format r;
r += format("invalid 'subst' tactic, "
"produced type incorrect term, details: ");
r += saved_ex->pp(fmt);
r += line();
return r;
});
}
}
expr new_val = mk_app(eqrec, deps);
assign(new_subst, g, new_val);
lean_assert(new_subst.is_assigned(g.get_mvar()));
proof_state new_s(s, goals(new_g, tail(gs)), new_subst, ngen);
return some_proof_state(new_s);
};
return tactic01(fn);
}
tactic mk_subst_tactic(list<name> const & ids) {
auto fn = [=](environment const & env, io_state const & ios, proof_state const & s) {
if (!ids)
return proof_state_seq(s);
goals const & gs = s.get_goals();
if (empty(gs))
return proof_state_seq();
goal const & g = head(gs);
name const & id = head(ids);
auto apply_rewrite = [&](expr const & H, bool symm) {
tactic tac = then(mk_subst_tactic_core(mlocal_name(H), symm), mk_subst_tactic(tail(ids)));
return tac(env, ios, s);
};
optional<pair<expr, unsigned>> p = g.find_hyp(id);
if (!p) {
throw_tactic_exception_if_enabled(s, sstream() << "invalid 'subst' tactic, there is no hypothesis named '"
<< id << "'");
return proof_state_seq();
}
expr const & H = p->first;
expr lhs, rhs;
if (is_eq(mlocal_type(H), lhs, rhs)) {
if (is_local(rhs)) {
return apply_rewrite(H, true);
} else if (is_local(lhs)) {
return apply_rewrite(H, false);
} else {
throw_tactic_exception_if_enabled(s, sstream() << "invalid 'subst' tactic, hypothesis '"
<< id << "' is not of the form (x = t) or (t = x)");
return proof_state_seq();
}
} else if (is_local(H)) {
expr const & x = H;
buffer<expr> hyps;
g.get_hyps(hyps);
for (expr const & H : hyps) {
expr lhs, rhs;
if (is_eq(mlocal_type(H), lhs, rhs)) {
if (is_local(lhs) && mlocal_name(lhs) == mlocal_name(x)) {
return apply_rewrite(H, false);
} else if (is_local(rhs) && mlocal_name(rhs) == mlocal_name(x)) {
return apply_rewrite(H, true);
}
}
}
}
throw_tactic_exception_if_enabled(s, sstream() << "invalid 'subst' tactic, hypothesis '"
<< id << "' is not a variable nor an equation of the form (x = t) or (t = x)");
return proof_state_seq();
};
return tactic(fn);
}
void initialize_subst_tactic() {
register_tac(name{"tactic", "subst"},
[](type_checker &, elaborate_fn const & elab, expr const & e, pos_info_provider const *) {
buffer<name> ns;
get_tactic_id_list_elements(app_arg(e), ns, "invalid 'subst' tactic, list of identifiers expected");
return then(mk_subst_tactic(to_list(ns)), try_tactic(refl_tactic(elab)));
});
}
void finalize_subst_tactic() {
}
}

11
src/library/tactic/subst_tactic.h Normal file
View file

@ -0,0 +1,11 @@
/*
Copyright (c) 2015 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#pragma once
namespace lean {
void initialize_subst_tactic();
void finalize_subst_tactic();
}

27
tests/lean/hott/subst_tac.hlean
View file

@ -1,9 +1,34 @@
open nat
example (A B : Type) (a : A) (b : B) (h₁ : A = B) (h₂ : eq.rec_on h₁ a = b) : b = eq.rec_on h₁ a :=
begin
subst h₁ h₂
end
example (A B : Type) (a : A) (b : B) (h₁ : A = B) (h₂ : eq.rec_on h₁ a = b) : b = eq.rec_on h₁ a :=
begin
subst B h₂
end
example (a b c : nat) (a0 : a = 0) (b1 : b = 1 + a) (ab : a = b) : empty :=
begin
subst a0,
subst b1,
contradiction
end
example (a : nat) : a = 0 → a = 1 → empty :=
begin
intro a0 a1,
subst a0,
contradiction
end
example (a b c : nat) : a = 0 → b = 1 + a → a = b → empty :=
begin
intro a0 b1 ab,
subst a0 b1,
subst a0,
rewrite b1 at *,
state,
contradiction
end