From a3f23d5233e4c76aff8a365ece6b37c114aa7206 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 25 May 2015 15:03:59 -0700 Subject: [PATCH] feat(library/tactic): add improved 'subst' tactic --- src/library/tactic/CMakeLists.txt | 2 +- src/library/tactic/init_module.cpp | 3 + src/library/tactic/rewrite_tactic.cpp | 81 ----------- src/library/tactic/subst_tactic.cpp | 194 ++++++++++++++++++++++++++ src/library/tactic/subst_tactic.h | 11 ++ tests/lean/hott/subst_tac.hlean | 27 +++- 6 files changed, 235 insertions(+), 83 deletions(-) create mode 100644 src/library/tactic/subst_tactic.cpp create mode 100644 src/library/tactic/subst_tactic.h diff --git a/src/library/tactic/CMakeLists.txt b/src/library/tactic/CMakeLists.txt index 46398ce6a..019033227 100644 --- a/src/library/tactic/CMakeLists.txt +++ b/src/library/tactic/CMakeLists.txt @@ -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}) diff --git a/src/library/tactic/init_module.cpp b/src/library/tactic/init_module.cpp index 7d7d33a6f..c4a4c7546 100644 --- a/src/library/tactic/init_module.cpp +++ b/src/library/tactic/init_module.cpp @@ -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(); diff --git a/src/library/tactic/rewrite_tactic.cpp b/src/library/tactic/rewrite_tactic.cpp index f5e8a3559..6e11f1814 100644 --- a/src/library/tactic/rewrite_tactic.cpp +++ b/src/library/tactic/rewrite_tactic.cpp @@ -1537,81 +1537,6 @@ tactic mk_rewrite_tactic(elaborate_fn const & elab, buffer const & elems) }); } -tactic mk_simple_rewrite_tactic(buffer 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 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 rw_elems; - rw_elems.push_back(rw_elem); - return mk_simple_rewrite_tactic(rw_elems); -} - -tactic mk_subst_tactic(list 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> 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 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 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() { diff --git a/src/library/tactic/subst_tactic.cpp b/src/library/tactic/subst_tactic.cpp new file mode 100644 index 000000000..fa727cada --- /dev/null +++ b/src/library/tactic/subst_tactic.cpp @@ -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 +#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 const & hyps, expr const & x, expr const & h, + buffer & non_deps, buffer & 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 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 new_hyps; + buffer 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 saved_ex(static_cast(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 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> 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 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 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() { +} +} diff --git a/src/library/tactic/subst_tactic.h b/src/library/tactic/subst_tactic.h new file mode 100644 index 000000000..91e191445 --- /dev/null +++ b/src/library/tactic/subst_tactic.h @@ -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(); +} diff --git a/tests/lean/hott/subst_tac.hlean b/tests/lean/hott/subst_tac.hlean index cd8532504..10e049034 100644 --- a/tests/lean/hott/subst_tac.hlean +++ b/tests/lean/hott/subst_tac.hlean @@ -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