From c379783c84c980ab009dbef9ef8eeaa80c7ca2b7 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 6 Jul 2016 07:34:34 -0700 Subject: [PATCH] chore(library/old_tactic/tactic): remove old code It has already been ported to new tactic framework. --- .../old_tactic/tactic/induction_tactic.cpp | 432 ------------------ .../old_tactic/tactic/induction_tactic.h | 11 - 2 files changed, 443 deletions(-) delete mode 100644 src/library/old_tactic/tactic/induction_tactic.cpp delete mode 100644 src/library/old_tactic/tactic/induction_tactic.h diff --git a/src/library/old_tactic/tactic/induction_tactic.cpp b/src/library/old_tactic/tactic/induction_tactic.cpp deleted file mode 100644 index 0b79bf119c..0000000000 --- a/src/library/old_tactic/tactic/induction_tactic.cpp +++ /dev/null @@ -1,432 +0,0 @@ -/* -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 "kernel/abstract.h" -#include "kernel/instantiate.h" -#include "kernel/inductive/inductive.h" -#include "library/util.h" -#include "library/old_util.h" -#include "library/user_recursors.h" -#include "library/constants.h" -#include "library/reducible.h" -#include "library/locals.h" -#include "library/class_instance_resolution.h" -#include "library/tactic/tactic.h" -#include "library/tactic/expr_to_tactic.h" -#include "library/tactic/generalize_tactic.h" - -namespace lean { -class induction_tac { - environment const & m_env; - io_state const & m_ios; - old_type_checker & m_tc; - name m_h_name; - optional m_rec_name; - list m_ids; - substitution m_subst; - bool m_throw_ex; - bool m_standard; - constraint_seq m_cs; - expr m_ref; // reference expression for location information - - void assign(goal const & g, expr const & val) { - ::lean::assign(m_subst, g, val); - } - - /** \brief Split hyps into two "telescopes". - - non_deps : hypotheses that do not depend on H nor its indices - - deps : hypotheses that depend on H or its indices (directly or indirectly) - */ - void split_deps(buffer const & hyps, expr const & h, buffer const & indices, - buffer & non_deps, buffer & deps) { - for (expr const & hyp : hyps) { - if (hyp == h) { - // we clear h - } else if (std::find(indices.begin(), indices.end(), hyp) != indices.end()) { - // hyp is an index - non_deps.push_back(hyp); - } else if (depends_on(hyp, h) || depends_on_any(hyp, indices) || depends_on_any(hyp, deps)) { - deps.push_back(hyp); - } else { - non_deps.push_back(hyp); - } - } - } - - void throw_ill_formed_recursor(recursor_info const & rec_info) { - throw tactic_exception(sstream() << "invalid 'induction' tactic, recursor '" << rec_info.get_name() - << "' is ill-formed"); - } - - expr mk_type_class_param(goal const & g, expr const & type) { - bool use_local_insts = true; - bool is_strict = false; - old_local_context ctx = g.to_local_context(); - auto mc = mk_class_instance_elaborator( - m_env, m_ios, ctx, optional(), - use_local_insts, is_strict, - some_expr(type), m_ref.get_tag(), nullptr); - m_cs += mc.second; - return mc.first; - } - - expr mk_type_class_param(goal const & g, expr const & rec, recursor_info const & rec_info) { - expr rec_type = m_tc.whnf(m_tc.infer(rec, m_cs), m_cs); - if (!is_pi(rec_type)) { - throw_ill_formed_recursor(rec_info); - } - return mk_type_class_param(g, binding_domain(rec_type)); - } - - goals apply_recursor(goal const & g, unsigned num_deps, expr const & h, expr const & h_type, - buffer> const & params, buffer const & indices, - recursor_info const & rec_info) { - expr const & g_type = g.get_type(); - level g_lvl = sort_level(m_tc.ensure_type(g_type, m_cs)); - buffer rec_lvls; - expr const & I = get_app_fn(h_type); - buffer I_lvls; - to_buffer(const_levels(I), I_lvls); - bool found_g_lvl = false; - for (unsigned idx : rec_info.get_universe_pos()) { - if (idx == recursor_info::get_motive_univ_idx()) { - rec_lvls.push_back(g_lvl); - found_g_lvl = true; - } else { - if (idx >= I_lvls.size()) - throw_ill_formed_recursor(rec_info); - rec_lvls.push_back(I_lvls[idx]); - } - } - if (!found_g_lvl && !is_zero(g_lvl)) { - throw tactic_exception(sstream() << "invalid 'induction' tactic, recursor '" << rec_info.get_name() - << "' can only eliminate into Prop"); - } - expr rec = mk_constant(rec_info.get_name(), to_list(rec_lvls)); - for (optional const & p : params) { - if (p) { - rec = mk_app(rec, *p); - } else { - rec = mk_app(rec, mk_type_class_param(g, rec, rec_info)); - } - } - expr motive = g_type; - if (rec_info.has_dep_elim()) - motive = Fun(h, motive); - motive = Fun(indices, motive); - rec = mk_app(rec, motive); - buffer hyps; - g.get_hyps(hyps); - buffer new_hyps; - for (expr const & curr_h : hyps) { - if (mlocal_name(curr_h) != mlocal_name(h) && - std::all_of(indices.begin(), indices.end(), - [&](expr const & idx) { return mlocal_name(curr_h) != mlocal_name(idx); })) { - new_hyps.push_back(curr_h); - } - } - expr rec_type = m_tc.whnf(m_tc.infer(rec, m_cs), m_cs); - unsigned curr_pos = params.size() + 1 /* motive */; - unsigned first_idx_pos = rec_info.get_first_index_pos(); - bool consumed_major = false; - buffer new_goals; - list produce_motive = rec_info.get_produce_motive(); - while (is_pi(rec_type) && curr_pos < rec_info.get_num_args()) { - if (first_idx_pos == curr_pos) { - for (expr const & idx : indices) { - rec = mk_app(rec, idx); - rec_type = m_tc.whnf(instantiate(binding_body(rec_type), idx), m_cs); - if (!is_pi(rec_type)) { - throw_ill_formed_recursor(rec_info); - } - curr_pos++; - } - rec = mk_app(rec, h); - rec_type = m_tc.whnf(instantiate(binding_body(rec_type), h), m_cs); - consumed_major = true; - curr_pos++; - } else { - if (!produce_motive) - throw_ill_formed_recursor(rec_info); - buffer new_goal_hyps; - new_goal_hyps.append(new_hyps); - expr new_type = binding_domain(rec_type); - expr rec_arg; - if (binding_info(rec_type).is_inst_implicit()) { - rec_arg = mk_type_class_param(g, binding_domain(rec_type)); - } else { - unsigned arity = get_arity(new_type); - // introduce minor arguments - buffer minor_args; - for (unsigned i = 0; i < arity; i++) { - expr arg_type = head_beta_reduce(binding_domain(new_type)); - name arg_name; - if (m_ids) { - arg_name = head(m_ids); - m_ids = tail(m_ids); - } else { - arg_name = binding_name(new_type); - } - expr new_h = mk_local(mk_fresh_name(), get_unused_name(arg_name, new_goal_hyps), - arg_type, binder_info()); - minor_args.push_back(new_h); - new_goal_hyps.push_back(new_h); - new_type = instantiate(binding_body(new_type), new_h); - } - new_type = head_beta_reduce(new_type); - buffer new_deps; - if (head(produce_motive)) { - // introduce deps - for (unsigned i = 0; i < num_deps; i++) { - if (!is_pi(new_type)) { - throw_ill_formed_recursor(rec_info); - } - expr dep_type = binding_domain(new_type); - expr new_dep = mk_local(mk_fresh_name(), - get_unused_name(binding_name(new_type), new_goal_hyps), - dep_type, binder_info()); - new_deps.push_back(new_dep); - new_goal_hyps.push_back(new_dep); - new_type = instantiate(binding_body(new_type), new_dep); - } - } - expr new_meta = mk_app(mk_metavar(mk_fresh_name(), Pi(new_goal_hyps, new_type)), new_goal_hyps); - goal new_g(new_meta, new_type); - new_goals.push_back(new_g); - rec_arg = Fun(minor_args, Fun(new_deps, new_meta)); - } - produce_motive = tail(produce_motive); - rec = mk_app(rec, rec_arg); - rec_type = m_tc.whnf(instantiate(binding_body(rec_type), rec_arg), m_cs); - curr_pos++; - } - } - if (!consumed_major) { - throw_ill_formed_recursor(rec_info); - } - assign(g, rec); - return to_list(new_goals); - } - - optional execute(goal const & g, expr const & h, expr const & h_type, name const & rec) { - try { - recursor_info rec_info = get_recursor_info(m_env, rec); - buffer h_type_args; - get_app_args(h_type, h_type_args); - buffer> params; - for (optional const & pos : rec_info.get_params_pos()) { - if (!pos) { - params.push_back(none_expr()); - } else if (*pos >= h_type_args.size()) { - throw tactic_exception("invalid 'induction' tactic, major premise type is ill-formed"); - } else { - params.push_back(some_expr(h_type_args[*pos])); - } - } - buffer indices; - list const & idx_pos = rec_info.get_indices_pos(); - for (unsigned pos : idx_pos) { - if (pos >= h_type_args.size()) { - throw tactic_exception("invalid 'induction' tactic, major premise type is ill-formed"); - } - expr const & idx = h_type_args[pos]; - if (!is_local(idx)) { - throw tactic_exception(sstream() << "invalid 'induction' tactic, argument #" - << pos+1 << " of major premise '" << h << "' type is not a variable"); - } - for (unsigned i = 0; i < h_type_args.size(); i++) { - if (i != pos && is_local(h_type_args[i]) && mlocal_name(h_type_args[i]) == mlocal_name(idx)) { - throw tactic_exception(sstream() << "invalid 'induction' tactic, argument #" - << pos+1 << " of major premise '" << h << "' type is an index, " - << "but it occurs more than once"); - } - if (i < pos && depends_on(h_type_args[i], idx)) { - throw tactic_exception(sstream() << "invalid 'induction' tactic, argument #" - << pos+1 << " of major premise '" << h << "' type is an index, " - << "but it occurs in previous arguments"); - } - if (i > pos && // occurs after idx - std::find(idx_pos.begin(), idx_pos.end(), i) != idx_pos.end() && // it is also an index - is_local(h_type_args[i]) && // if it is not an index, it will fail anyway. - depends_on(mlocal_type(idx), h_type_args[i])) { - throw tactic_exception(sstream() << "invalid 'induction' tactic, argument #" - << pos+1 << " of major premise '" << h << "' type is an index, " - << "but its type depends on the index at position #" << i+1); - } - } - indices.push_back(idx); - } - if (!rec_info.has_dep_elim() && depends_on(g.get_type(), h)) { - throw tactic_exception(sstream() << "invalid 'induction' tactic, recursor '" << rec - << "' does not support dependent elimination, but conclusion " - << "depends on major premise '" << h << "'"); - } - buffer hyps, non_deps, deps; - g.get_hyps(hyps); - split_deps(hyps, h, indices, non_deps, deps); - buffer & new_hyps = non_deps; - new_hyps.push_back(h); - expr new_type = Pi(deps, g.get_type()); - expr new_meta = mk_app(mk_metavar(mk_fresh_name(), Pi(new_hyps, new_type)), new_hyps); - goal new_g(new_meta, new_type); - expr val = mk_app(new_meta, deps); - assign(g, val); - return optional(apply_recursor(new_g, deps.size(), h, h_type, params, indices, rec_info)); - } catch (exception const & ex) { - throw tactic_exception(sstream() << "invalid 'induction' tactic, " << ex.what()); - } - } - -public: - induction_tac(environment const & env, io_state const & ios, - old_type_checker & tc, substitution const & subst, name const & h_name, - optional const & rec_name, list const & ids, - bool throw_ex, expr const & ref): - m_env(env), m_ios(ios), m_tc(tc), m_h_name(h_name), m_rec_name(rec_name), m_ids(ids), - m_subst(subst), m_throw_ex(throw_ex), m_ref(ref) { - m_standard = is_standard(env); - } - - substitution const & get_subst() const { return m_subst; } - - constraint_seq get_new_constraints() const { return m_cs; } - - expr normalize_H_type(expr const & H) { - lean_assert(is_local(H)); - expr H_type = m_subst.instantiate_all(mlocal_type(H)); - if (m_rec_name) { - recursor_info info = get_recursor_info(m_env, *m_rec_name); - name tname = info.get_type_name(); - old_type_checker_ptr aux_tc = mk_type_checker(m_env, [=](name const & n) { return n == tname; }); - return aux_tc->whnf(H_type).first; - } else { - has_recursors_pred pred(m_env); - old_type_checker_ptr aux_tc = mk_type_checker(m_env, pred); - return aux_tc->whnf(H_type).first; - } - } - - optional execute(goal const & g) { - try { - auto p = g.find_hyp(m_h_name); - if (!p) - throw tactic_exception(sstream() << "invalid 'induction' tactic, unknown hypothesis '" << m_h_name << "'"); - expr H = p->first; - expr H_type = normalize_H_type(H); - expr I = get_app_fn(H_type); - if (is_constant(I)) { - if (m_rec_name) { - return execute(g, H, H_type, *m_rec_name); - } else if (inductive::is_inductive_decl(m_env, const_name(I))) { - return execute(g, H, H_type, inductive::get_elim_name(const_name(I))); - } else if (list rs = get_recursors_for(m_env, const_name(I))) { - while (rs) { - name r = head(rs); - rs = tail(rs); - if (!rs) { - // last one - return execute(g, H, H_type, r); - } else { - list saved_ids = m_ids; - constraint_seq saved_cs = m_cs; - substitution saved_subst = m_subst; - try { - return execute(g, H, H_type, r); - } catch (exception &) { - m_ids = saved_ids; - m_cs = saved_cs; - m_subst = saved_subst; - } - } - } - } - } - throw tactic_exception(sstream() << "invalid 'induction' tactic, hypothesis '" << m_h_name - << "' must have a type that is associated with a recursor"); - } catch (tactic_exception & ex) { - if (m_throw_ex) - throw; - return optional(); - } catch (exception & ex) { - if (m_throw_ex) - throw tactic_exception(sstream() << "invalid 'induction' tactic, " << ex.what()); - return optional(); - } - } -}; - -tactic induction_tactic(name const & H, optional rec, list const & ids, expr const & ref) { - auto fn = [=](environment const & env, io_state const & ios, proof_state const & ps) -> optional { - goals const & gs = ps.get_goals(); - if (empty(gs)) { - throw_no_goal_if_enabled(ps); - return none_proof_state(); - } - goal g = head(gs); - goals tail_gs = tail(gs); - std::unique_ptr tc = mk_type_checker(env); - induction_tac tac(env, ios, *tc, ps.get_subst(), H, rec, ids, ps.report_failure(), ref); - if (auto res = tac.execute(g)) { - proof_state new_s(ps, append(*res, tail_gs), tac.get_subst()); - if (solve_constraints(env, ios, new_s, tac.get_new_constraints())) - return some_proof_state(new_s); - else - return none_proof_state(); - } else { - return none_proof_state(); - } - }; - return tactic01(fn); -} - -tactic induction_tactic(elaborate_fn const & elab, expr const & H, optional rec, list const & ids, expr const & ref) { - auto fn = [=](environment const & env, io_state const & ios, proof_state const & ps) { - name Haux{"H", "ind"}; - auto new_ps = generalize_core(env, ios, elab, H, Haux, ps, "induction", true); - if (!new_ps) - return proof_state_seq(); - goal g = head(new_ps->get_goals()); - expr new_H = app_arg(g.get_meta()); - lean_assert(is_local(new_H)); - name H_name = local_pp_name(new_H); - return induction_tactic(H_name, rec, ids, ref)(env, ios, *new_ps); - }; - return tactic(fn); -} - -void initialize_induction_tactic() { - register_tac(name{"tactic", "induction"}, - [](old_type_checker &, elaborate_fn const & elab, expr const & e, pos_info_provider const *) { - buffer args; - get_app_args(e, args); - if (args.size() != 3) - throw expr_to_tactic_exception(e, "invalid 'induction' tactic, insufficient number of arguments"); - check_tactic_expr(args[0], "invalid 'induction' tactic, argument must be an expression"); - expr H = get_tactic_expr_expr(args[0]); - buffer ids; - get_tactic_id_list_elements(args[2], ids, "invalid 'induction' tactic, list of identifiers expected"); - check_tactic_expr(args[1], "invalid 'induction' tactic, invalid argument"); - expr rec = get_tactic_expr_expr(args[1]); - if (!is_constant(rec)) { - throw expr_to_tactic_exception(args[1], "invalid 'induction' tactic, constant expected"); - } - name const & cname = const_name(rec); - if (cname == get_tactic_none_expr_name()) { - if (is_local(H)) - return induction_tactic(local_pp_name(H), optional(), to_list(ids.begin(), ids.end()), e); - else - return induction_tactic(elab, H, optional(), to_list(ids.begin(), ids.end()), e); - } else { - if (is_local(H)) - return induction_tactic(local_pp_name(H), optional(cname), to_list(ids.begin(), ids.end()), e); - else - return induction_tactic(elab, H, optional(), to_list(ids.begin(), ids.end()), e); - } - }); -} -void finalize_induction_tactic() { -} -} diff --git a/src/library/old_tactic/tactic/induction_tactic.h b/src/library/old_tactic/tactic/induction_tactic.h deleted file mode 100644 index 72baf5b86a..0000000000 --- a/src/library/old_tactic/tactic/induction_tactic.h +++ /dev/null @@ -1,11 +0,0 @@ -/* -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_induction_tactic(); -void finalize_induction_tactic(); -}