diff --git a/src/library/tactic/CMakeLists.txt b/src/library/tactic/CMakeLists.txt index a233d11771..947d3adbd8 100644 --- a/src/library/tactic/CMakeLists.txt +++ b/src/library/tactic/CMakeLists.txt @@ -6,5 +6,5 @@ add_library(tactic OBJECT occurrences.cpp kabstract.cpp tactic_state.cpp induction_tactic.cpp cases_tactic.cpp generalize_tactic.cpp rewrite_tactic.cpp unfold_tactic.cpp hsubstitution.cpp gexpr.cpp elaborate.cpp init_module.cpp - simp_result.cpp eval.cpp simp_lemmas.cpp eqn_lemmas.cpp dsimplify.cpp simplify.cpp + simp_result.cpp eval.cpp simp_lemmas.cpp eqn_lemmas.cpp dsimplify.cpp destruct_tactic.cpp elaborator_exception.cpp tactic_evaluator.cpp) diff --git a/src/library/tactic/init_module.cpp b/src/library/tactic/init_module.cpp index 865390b5f8..5b1ff9d400 100644 --- a/src/library/tactic/init_module.cpp +++ b/src/library/tactic/init_module.cpp @@ -27,7 +27,6 @@ Author: Leonardo de Moura #include "library/tactic/simp_lemmas.h" #include "library/tactic/eqn_lemmas.h" #include "library/tactic/dsimplify.h" -#include "library/tactic/simplify.h" #include "library/tactic/destruct_tactic.h" namespace lean { @@ -50,7 +49,6 @@ void initialize_tactic_module() { initialize_generalize_tactic(); initialize_rewrite_tactic(); initialize_unfold_tactic(); - initialize_simplify(); initialize_elaborate(); initialize_eval(); initialize_simp_lemmas(); @@ -65,7 +63,6 @@ void finalize_tactic_module() { finalize_simp_lemmas(); finalize_eval(); finalize_elaborate(); - finalize_simplify(); finalize_unfold_tactic(); finalize_rewrite_tactic(); finalize_generalize_tactic(); diff --git a/src/library/tactic/simplify.cpp b/src/library/tactic/simplify.cpp deleted file mode 100644 index b4086b7695..0000000000 --- a/src/library/tactic/simplify.cpp +++ /dev/null @@ -1,1320 +0,0 @@ -/* -Copyright (c) 2015 Daniel Selsam. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Author: Daniel Selsam, Leonardo de Moura -*/ -#include -#include -#include -#include "runtime/interrupt.h" -#include "runtime/flet.h" -#include "runtime/optional.h" -#include "util/freset.h" -#include "util/pair.h" -#include "util/sexpr/option_declarations.h" -#include "kernel/abstract.h" -#include "kernel/expr_maps.h" -#include "kernel/find_fn.h" -#include "kernel/instantiate.h" -#include "library/trace.h" -#include "library/annotation.h" -#include "library/pp_options.h" -#include "library/constants.h" -#include "library/normalize.h" -#include "library/expr_lt.h" -#include "library/locals.h" -#include "library/num.h" -#include "library/idx_metavar.h" -#include "library/util.h" -#include "library/attribute_manager.h" -#include "library/defeq_canonizer.h" -#include "library/relation_manager.h" -#include "library/app_builder.h" -#include "library/congr_lemma.h" -#include "library/fun_info.h" -#include "library/constructions/constructor.h" -#include "library/constructions/injective.h" -#include "library/inductive_compiler/ginductive.h" -#include "library/vm/vm_expr.h" -#include "library/vm/vm_option.h" -#include "library/vm/vm_list.h" -#include "library/vm/vm_nat.h" -#include "library/vm/vm_name.h" -#include "library/tactic/eqn_lemmas.h" -#include "library/tactic/tactic_state.h" -#include "library/tactic/app_builder_tactics.h" -#include "library/tactic/simp_lemmas.h" -#include "library/tactic/simplify.h" -#include "library/tactic/dsimplify.h" -#include "library/tactic/simp_util.h" - -#ifndef LEAN_DEFAULT_SIMPLIFY_MAX_STEPS -#define LEAN_DEFAULT_SIMPLIFY_MAX_STEPS 1000000 -#endif -#ifndef LEAN_DEFAULT_SIMPLIFY_CONTEXTUAL -#define LEAN_DEFAULT_SIMPLIFY_CONTEXTUAL true -#endif -#ifndef LEAN_DEFAULT_SIMPLIFY_REWRITE -#define LEAN_DEFAULT_SIMPLIFY_REWRITE true -#endif -#ifndef LEAN_DEFAULT_SIMPLIFY_LIFT_EQ -#define LEAN_DEFAULT_SIMPLIFY_LIFT_EQ true -#endif - -namespace lean { - -simp_config::simp_config(): - m_max_steps(LEAN_DEFAULT_SIMPLIFY_MAX_STEPS), - m_contextual(LEAN_DEFAULT_SIMPLIFY_CONTEXTUAL), - m_lift_eq(LEAN_DEFAULT_SIMPLIFY_LIFT_EQ), - m_canonize_instances(true), - m_canonize_proofs(false), - m_use_axioms(false), - m_zeta(false), - m_beta(false), - m_eta(true), - m_proj(true), - m_iota(true), - m_iota_eqn(false), - m_constructor_eq(true), - m_single_pass(false), - m_fail_if_unchanged(true), - m_memoize(true) { -} - -simp_config::simp_config(vm_obj const & obj) { - m_max_steps = force_to_unsigned(cfield(obj, 0)); - m_contextual = to_bool(cfield(obj, 1)); - m_lift_eq = to_bool(cfield(obj, 2)); - m_canonize_instances = to_bool(cfield(obj, 3)); - m_canonize_proofs = to_bool(cfield(obj, 4)); - m_use_axioms = to_bool(cfield(obj, 5)); - m_zeta = to_bool(cfield(obj, 6)); - m_beta = to_bool(cfield(obj, 7)); - m_eta = to_bool(cfield(obj, 8)); - m_proj = to_bool(cfield(obj, 9)); - m_iota = to_bool(cfield(obj, 10)); - m_iota_eqn = to_bool(cfield(obj, 11)); - m_constructor_eq = to_bool(cfield(obj, 12)); - m_single_pass = to_bool(cfield(obj, 13)); - m_fail_if_unchanged = to_bool(cfield(obj, 14)); - m_memoize = to_bool(cfield(obj, 15)); -} - -/* ----------------------------------- - Core simplification procedure. - ------------------------------------ */ - -simp_result simplify_core_fn::join(simp_result const & r1, simp_result const & r2) { - return ::lean::join(m_ctx, m_rel, r1, r2); -} - -void simplify_core_fn::inc_num_steps() { - m_num_steps++; - if (m_num_steps > m_cfg.m_max_steps) - throw exception("simplify failed, maximum number of steps exceeded"); -} - -bool simplify_core_fn::is_dependent_fn(expr const & f) { - expr f_type = m_ctx.relaxed_whnf(m_ctx.infer(f)); - lean_assert(is_pi(f_type)); - return !is_arrow(f_type); -} - -class simp_prover { - simplify_core_fn & m_simp; -public: - simp_prover(simplify_core_fn & s):m_simp(s) {} - - optional operator()(tmp_type_context &, expr const & e) { - return m_simp.prove(e); - } -}; - -bool simplify_core_fn::instantiate_emetas(tmp_type_context & tmp_ctx, list const & emetas, - list const & instances) { - simp_prover prover(*this); - return instantiate_emetas_fn(prover)(tmp_ctx, emetas, instances); -} - -simp_result simplify_core_fn::lift_from_eq(simp_result const & r_eq) { - if (!r_eq.has_proof()) return r_eq; - expr new_pr = ::lean::lift_from_eq(m_ctx, m_rel, r_eq.get_proof()); - return simp_result(r_eq.get_new(), new_pr); -} - -simp_lemmas simplify_core_fn::add_to_slss(simp_lemmas const & _slss, buffer const & ls) { - simp_lemmas slss = _slss; - for (unsigned i = 0; i < ls.size(); i++) { - expr const & l = ls[i]; - try { - slss = add(m_ctx, slss, local_name(l), m_ctx.infer(l), l, LEAN_DEFAULT_PRIORITY); - lean_simp_trace(m_ctx, name({"simplify", "context"}), - tout() << local_name(l) << " : " << m_ctx.infer(l) << "\n";); - } catch (exception & e) {} - } - return slss; -} - -/* Given the application 'e', remove unnecessary casts of the form (eq.nrec a rfl) and (eq.drec a rfl) */ -expr simplify_core_fn::remove_unnecessary_casts(expr const & e) { - buffer args; - expr f = get_app_args(e, args); - ss_param_infos ss_infos = get_specialized_subsingleton_info(m_ctx, e); - int i = -1; - bool modified = false; - for (ss_param_info const & ss_info : ss_infos) { - i++; - if (ss_info.is_subsingleton()) { - while (is_constant(get_app_fn(args[i]))) { - buffer cast_args; - expr f_cast = get_app_args(args[i], cast_args); - name n_f = const_name(f_cast); - if (n_f == get_eq_ndrec_name() || n_f == get_eq_rec_name()) { - lean_assert(cast_args.size() == 6); - expr major_premise = cast_args[5]; - expr f_major_premise = get_app_fn(major_premise); - if (is_constant(f_major_premise) && const_name(f_major_premise) == get_eq_refl_name()) { - args[i] = cast_args[3]; - modified = true; - } else { - break; - } - } else { - break; - } - } - } - } - return modified ? mk_app(f, args) : e; -} - -expr simplify_core_fn::defeq_canonize_args_step(expr const & e) { - buffer args; - bool modified = false; - expr f = get_app_args(e, args); - fun_info info = get_fun_info(m_ctx, f, args.size()); - unsigned i = 0; - for (param_info const & pinfo : info.get_params_info()) { - lean_assert(i < args.size()); - expr new_a; - if ((m_cfg.m_canonize_instances && pinfo.is_inst_implicit()) || - (m_cfg.m_canonize_proofs && pinfo.is_prop())) { - new_a = m_defeq_canonizer.canonize(args[i], m_need_restart); - lean_simp_trace(m_ctx, name({"simplify", "canonize"}), - tout() << "\n" << args[i] << "\n==>\n" << new_a << "\n";); - if (new_a != args[i]) { - modified = true; - args[i] = new_a; - } - } - i++; - } - - return modified ? mk_app(f, args) : e; -} - -/* Try user defined congruence lemmas */ -simp_result simplify_core_fn::try_user_congrs(expr const & e) { - simp_lemmas_for const * sls = m_slss.find(m_rel); - if (!sls) return simp_result(e); - - if (auto cls = sls->find_congr(e)) { - for (simp_lemma const & cl : *cls) { - simp_result r = try_user_congr(e, cl); - if (r.get_new() != e) - return r; - } - } - - if (auto cls = sls->find_congr(head_index(expr_kind::MVar))) { - for (simp_lemma const & cl : *cls) { - simp_result r = try_user_congr(e, cl); - if (r.get_new() != e) - return r; - } - } - - return simp_result(e); -} - -simp_result simplify_core_fn::try_user_congr(expr const & e, simp_lemma const & cl) { - tmp_type_context tmp_ctx(m_ctx, cl.get_num_umeta(), cl.get_num_emeta()); - if (!tmp_ctx.is_def_eq(cl.get_lhs(), e)) - return simp_result(e); - - lean_simp_trace(tmp_ctx, name({"debug", "simplify", "try_congruence"}), - tout() << "(" << cl.get_id() << ") " << e << "\n";); - - bool simplified = false; - - buffer congr_hyps; - to_buffer(cl.get_congr_hyps(), congr_hyps); - - buffer factories; - buffer relations; - for (expr const & m : congr_hyps) { - factories.emplace_back(m_ctx); - type_context_old::tmp_locals & local_factory = factories.back(); - expr m_type = tmp_ctx.instantiate_mvars(tmp_ctx.infer(m)); - - while (is_pi(m_type)) { - expr d = instantiate_rev(binding_domain(m_type), local_factory.as_buffer().size(), - local_factory.as_buffer().data()); - expr l = local_factory.push_local(binding_name(m_type), d, binding_info(m_type)); - lean_assert(!has_idx_metavar(l)); - m_type = binding_body(m_type); - } - m_type = instantiate_rev(m_type, local_factory.as_buffer().size(), local_factory.as_buffer().data()); - - expr h_rel, h_lhs, h_rhs; - lean_verify(is_simp_relation(tmp_ctx.env(), m_type, h_rel, h_lhs, h_rhs) && is_constant(h_rel)); - { - relations.push_back(const_name(h_rel)); - flet set_slss(m_slss, m_cfg.m_contextual ? add_to_slss(m_slss, local_factory.as_buffer()) : m_slss); - - h_lhs = tmp_ctx.instantiate_mvars(h_lhs); - lean_assert(!has_idx_metavar(h_lhs)); - - simp_result r_congr_hyp; - if (m_cfg.m_contextual || m_rel != const_name(h_rel)) { - flet set_name(m_rel, const_name(h_rel)); - freset reset_cache(m_cache); - r_congr_hyp = visit(h_lhs, some_expr(e)); - } else { - r_congr_hyp = visit(h_lhs, some_expr(e)); - } - - if (r_congr_hyp.has_proof()) - simplified = true; - - lean_assert(is_metavar_app(h_rhs)); - buffer new_val_meta_args; - expr new_val_meta = get_app_args(h_rhs, new_val_meta_args); - lean_assert(is_metavar(new_val_meta)); - expr new_val = tmp_ctx.mk_lambda(new_val_meta_args, r_congr_hyp.get_new()); - tmp_ctx.assign(new_val_meta, new_val); - - expr pf_body = finalize(m_ctx, const_name(h_rel), r_congr_hyp).get_proof(); - expr pf = local_factory.mk_lambda(pf_body); - if (!tmp_ctx.is_def_eq(m, pf)) { - lean_simp_trace(tmp_ctx, name({"simplify", "congruence"}), - tout() << "failed to unify proof " << pf << " of " << tmp_ctx.infer(pf);); - return simp_result(e); - } - } - } - - if (!simplified) - return simp_result(e); - - if (!instantiate_emetas(tmp_ctx, cl.get_emetas(), cl.get_instances())) - return simp_result(e); - - for (unsigned i = 0; i < cl.get_num_umeta(); i++) { - if (!tmp_ctx.is_uassigned(i)) - return simp_result(e); - } - - expr e_s = tmp_ctx.instantiate_mvars(cl.get_rhs()); - expr pf = tmp_ctx.instantiate_mvars(cl.get_proof()); - - simp_result r(e_s, pf); - - lean_simp_trace(tmp_ctx, name({"simplify", "congruence"}), - tout() << "(" << cl.get_id() << ") " - << "[" << e << " ==> " << e_s << "]\n";); - - return r; -} - -/* Try to use congruence lemmas generated by the congr_lemma module. - \remark these lemmas are for the equality relation. */ -optional simplify_core_fn::try_auto_eq_congr(expr const & e) { - lean_assert(m_rel == get_eq_name()); - lean_assert(is_app(e)); - buffer args; - expr f = get_app_args(e, args); - auto congr_lemma = mk_specialized_congr_simp(m_ctx, e); - if (!congr_lemma || length(congr_lemma->get_arg_kinds()) < args.size()) - return optional(); - - buffer r_args; - buffer new_args; - bool has_proof = false; - bool has_cast = false; - bool has_simplified = false; - - unsigned i = 0; - - // First pass, try to simplify all the Eq arguments - for (congr_arg_kind const & ckind : congr_lemma->get_arg_kinds()) { - switch (ckind) { - case congr_arg_kind::HEq: - lean_unreachable(); - case congr_arg_kind::Fixed: - case congr_arg_kind::FixedNoParam: - new_args.emplace_back(args[i]); - break; - case congr_arg_kind::Eq: - { - r_args.emplace_back(visit(args[i], some_expr(e))); - simp_result & r_arg = r_args.back(); - new_args.emplace_back(r_arg.get_new()); - if (r_arg.has_proof()) - has_proof = true; - if (r_arg.get_new() != args[i]) - has_simplified = true; - } - break; - case congr_arg_kind::Cast: - has_cast = true; - new_args.emplace_back(args[i]); - break; - } - i++; - } - - if (!has_simplified) { - simp_result r = simp_result(e); - return optional(r); - } - - if (!has_proof) { - simp_result r = simp_result(mk_app(f, new_args)); - return optional(r); - } - - // We have a proof, so we need to build the congruence lemma - expr proof = congr_lemma->get_proof(); - expr type = congr_lemma->get_type(); - buffer subst; - - i = 0; - unsigned i_eq = 0; - for (congr_arg_kind const & ckind : congr_lemma->get_arg_kinds()) { - switch (ckind) { - case congr_arg_kind::HEq: - lean_unreachable(); - case congr_arg_kind::Fixed: - proof = mk_app(proof, args[i]); - subst.push_back(args[i]); - type = binding_body(type); - break; - case congr_arg_kind::FixedNoParam: - break; - case congr_arg_kind::Eq: - proof = mk_app(proof, args[i]); - subst.push_back(args[i]); - type = binding_body(type); - { - simp_result r_arg = finalize(m_ctx, m_rel, r_args[i_eq]); - proof = mk_app(proof, r_arg.get_new(), r_arg.get_proof()); - subst.push_back(r_arg.get_new()); - subst.push_back(r_arg.get_proof()); - } - type = binding_body(binding_body(type)); - i_eq++; - break; - case congr_arg_kind::Cast: - lean_assert(has_cast); - proof = mk_app(proof, args[i]); - subst.push_back(args[i]); - type = binding_body(type); - break; - } - i++; - } - lean_assert(is_eq(type)); - expr rhs = instantiate_rev(app_arg(type), subst.size(), subst.data()); - simp_result r(rhs, proof); - - if (has_cast) { - r.update(remove_unnecessary_casts(r.get_new())); - } - - return optional(r); -} - -simp_result simplify_core_fn::congr_fun_arg(simp_result const & r_f, simp_result const & r_arg) { - if (!r_f.has_proof() && !r_arg.has_proof()) return simp_result(mk_app(r_f.get_new(), r_arg.get_new())); - else if (!r_f.has_proof()) return congr_arg(r_f.get_new(), r_arg); - else if (!r_arg.has_proof()) return congr_fun(r_f, r_arg.get_new()); - else return congr(r_f, r_arg); -} - -simp_result simplify_core_fn::congr(simp_result const & r_f, simp_result const & r_arg) { - lean_assert(r_f.has_proof() && r_arg.has_proof()); - // theorem congr {A B : Type} {f₁ f₂ : A → B} {a₁ a₂ : A} (H₁ : f₁ = f₂) (H₂ : a₁ = a₂) : f₁ a₁ = f₂ a₂ - expr e = mk_app(r_f.get_new(), r_arg.get_new()); - expr pf = mk_congr(m_ctx, r_f.get_proof(), r_arg.get_proof()); - return simp_result(e, pf); -} - -simp_result simplify_core_fn::congr_fun(simp_result const & r_f, expr const & arg) { - lean_assert(r_f.has_proof()); - // theorem congr_fun {A : Type} {B : A → Type} {f g : Π x, B x} (H : f = g) (a : A) : f a = g a - expr e = mk_app(r_f.get_new(), arg); - expr pf = mk_congr_fun(m_ctx, r_f.get_proof(), arg); - return simp_result(e, pf); -} - -simp_result simplify_core_fn::congr_arg(expr const & f, simp_result const & r_arg) { - lean_assert(r_arg.has_proof()); - // theorem congr_arg {A B : Type} {a₁ a₂ : A} (f : A → B) : a₁ = a₂ → f a₁ = f a₂ - expr e = mk_app(f, r_arg.get_new()); - expr pf = mk_congr_arg(m_ctx, f, r_arg.get_proof()); - return simp_result(e, pf); -} - -simp_result simplify_core_fn::congr_funs(simp_result const & r_f, buffer const & args) { - expr e = r_f.get_new(); - for (unsigned i = 0; i < args.size(); ++i) { - e = mk_app(e, args[i]); - } - if (!r_f.has_proof()) - return simp_result(e); - expr pf = r_f.get_proof(); - for (unsigned i = 0; i < args.size(); ++i) { - pf = mk_congr_fun(m_ctx, pf, args[i]); - } - return simp_result(e, pf); -} - -simp_result simplify_core_fn::rewrite(expr const & e) { - simp_lemmas_for const * sr = m_slss.find(m_rel); - if (!sr) return simp_result(e); - - list const * srs = sr->find(e); - if (!srs) { - return simp_result(e); - } - - for (simp_lemma const & lemma : *srs) { - simp_result r = rewrite(e, lemma); - if (!is_eqp(r.get_new(), e)) { - lean_simp_trace_d(m_ctx, name({"simplify", "rewrite"}), - tout() << "[" << lemma.get_id() << "]: " - << e << " ==> " << r.get_new() << "\n";); - return r; - } - } - - return simp_result(e); -} - -bool simplify_core_fn::match(tmp_type_context & ctx, simp_lemma const & sl, expr const & t) { - return ctx.match(sl.get_lhs(), t); -} - -/* If both e and sl.get_lhs() are of the form (f ...), - then we only trace the failure if the number of arguments is the same. - - This is simple filter to minimize the number of rewriting failures. */ -static bool should_trace_failure(expr const & e, simp_lemma const & sl) { - expr const & p = sl.get_lhs(); - expr const & fn = get_app_fn(p); - if (!is_constant(fn)) return true; - expr const & e_fn = get_app_fn(e); - if (!is_constant(e_fn) || const_name(fn) != const_name(e_fn)) return true; - return get_app_num_args(e) == get_app_num_args(p); -} - -simp_result simplify_core_fn::rewrite_core(expr const & e, simp_lemma const & sl) { - tmp_type_context tmp_ctx(m_ctx, sl.get_num_umeta(), sl.get_num_emeta()); - - if (!match(tmp_ctx, sl, e)) { - if (lean_is_trace_enabled(name({"simplify", "rewrite_failure"})) && - should_trace_failure(e, sl)) { - lean_simp_trace_d(m_ctx, name({"simplify", "rewrite_failure"}), - tout() << "fail to match '" << sl.get_id() << "':\n" - << e << "\n=?=\n" << sl.get_lhs() << "\n--------------\n";); - } - return simp_result(e); - } - - if (!instantiate_emetas(tmp_ctx, sl.get_emetas(), sl.get_instances())) { - lean_simp_trace_d(m_ctx, name({"simplify", "failure"}), - lean_trace_init_bool(name({"simplify", "failure"}), get_pp_implicit_name(), true); - tout() << "fail to instantiate emetas: '" << sl.get_id() << "' at\n" - << e << "\npartially instantiated lemma:\n" << tmp_ctx.instantiate_mvars(sl.get_proof()) << "\n";); - return simp_result(e); - } - - for (unsigned i = 0; i < sl.get_num_umeta(); i++) { - if (!tmp_ctx.is_uassigned(i)) { - lean_simp_trace_d(m_ctx, name({"simplify", "failure"}), - lean_trace_init_bool(name({"simplify", "failure"}), get_pp_universes_name(), true); - tout() << "fail to instantiate umetas: '" << sl.get_id() << "'\n";); - return simp_result(e); - } - } - - expr new_lhs = tmp_ctx.instantiate_mvars(sl.get_lhs()); - expr new_rhs = tmp_ctx.instantiate_mvars(sl.get_rhs()); - - if (new_rhs == e) { - /* TODO(Leo): remove after we have arithmetic normalizer. - The unifier at type context has support for offset equalities. - So, it can match - ?x + 0 =?= t + 1 - by assigning - ?x := t + 1 */ - return simp_result(e); - } - - if (sl.is_permutation()) { - if (!is_lt(new_rhs, new_lhs, false, &m_ctx.lctx())) { - lean_simp_trace(tmp_ctx, name({"simplify", "perm"}), - tout() << "perm rejected: " << new_rhs << " !< " << new_lhs << "\n";); - return simp_result(e); - } - } - - expr pf = tmp_ctx.instantiate_mvars(sl.get_proof()); - return simp_result(new_rhs, pf); -} - -simp_result simplify_core_fn::rewrite(expr const & e, simp_lemma const & sl) { - if (!is_app(e)) - return rewrite_core(e, sl); - unsigned e_nargs = get_app_num_args(e); - unsigned lhs_nargs = get_app_num_args(sl.get_lhs()); - if (e_nargs == lhs_nargs) - return rewrite_core(e, sl); - if (e_nargs < lhs_nargs) - return simp_result(e); - buffer extra_args; - unsigned i = e_nargs; - auto it = e; - while (i > lhs_nargs) { - --i; - extra_args.push_back(app_arg(it)); - it = app_fn(it); - } - lean_assert(get_app_num_args(it) == lhs_nargs); - simp_result it_r = rewrite_core(it, sl); - if (it_r.get_new() == it) - return simp_result(e); - expr new_e = mk_rev_app(it_r.get_new(), extra_args); - new_e = reduce(new_e); - if (!it_r.has_proof()) - return simp_result(new_e); - expr pr = it_r.get_proof(); - i = extra_args.size(); - while (i > 0) { - --i; - pr = mk_congr_fun(m_ctx, pr, extra_args[i]); - } - return simp_result(new_e, pr); -} - -simp_result simplify_core_fn::propext_rewrite(expr const & e) { - if (m_rel != get_eq_name()) return simp_result(e); - flet set_rel(m_rel, get_iff_name()); - freset reset_cache(m_cache); - simp_result r = rewrite(e); - if (!r.has_proof()) return r; - expr new_pr = mk_app(m_ctx, get_propext_name(), r.get_proof()); - return simp_result(r.get_new(), new_pr); -} - -simp_result simplify_core_fn::visit(expr const & e, optional const & parent) { - check_system("simplify"); - inc_num_steps(); - lean_trace_inc_depth("simplify"); - lean_simp_trace(m_ctx, "simplify", tout() << m_rel << ": " << e << "\n";); - - if (m_cfg.m_memoize) { - auto it = m_cache.find(e); - if (it != m_cache.end()) - return it->second; - } - - simp_result curr_result(e); - if (auto r1 = pre(e, parent)) { - if (!r1->second) { - if (m_cfg.m_memoize) - m_cache.insert(mk_pair(e, r1->first)); - return r1->first; - } - curr_result = r1->first; - } - - while (true) { - simp_result new_result; - switch (curr_result.get_new().kind()) { - case expr_kind::FVar: - case expr_kind::Sort: - case expr_kind::Lit: - case expr_kind::Const: - new_result = curr_result; - break; - case expr_kind::MVar: - new_result = curr_result; - new_result.update(m_ctx.instantiate_mvars(new_result.get_new())); - break; - case expr_kind::BVar: - lean_unreachable(); - case expr_kind::Lambda: - new_result = join(curr_result, visit_lambda(curr_result.get_new())); - break; - case expr_kind::Pi: - new_result = join(curr_result, visit_pi(curr_result.get_new())); - break; - case expr_kind::App: - new_result = join(curr_result, visit_app(curr_result.get_new())); - break; - case expr_kind::Let: - new_result = join(curr_result, visit_let(curr_result.get_new())); - break; - case expr_kind::MData: - new_result = join(curr_result, visit(mdata_expr(e), some_expr(e))); - break; - case expr_kind::Proj: - new_result = curr_result; - break; - case expr_kind::Quote: - new_result = curr_result; - break; - } - - if (m_cfg.m_constructor_eq && simplify_constructor_eq_constructor(new_result)) { - curr_result = new_result; - /* continue simplifying */ - } else if (auto r2 = post(new_result.get_new(), parent)) { - if (!r2->second) { - curr_result = join(new_result, r2->first); - break; - } else if (r2->first.get_new() == curr_result.get_new()) { - break; - } else { - curr_result = join(new_result, r2->first); - if (m_cfg.m_single_pass) - break; - /* continue simplifying */ - } - } else { - curr_result = new_result; - break; - } - } - - if (m_cfg.m_lift_eq && m_rel != get_eq_name()) { - simp_result eq_result; - { - flet use_eq(m_rel, get_eq_name()); - freset reset_cache(m_cache); - eq_result = visit(curr_result.get_new(), parent); - } - if (eq_result.get_new() != curr_result.get_new()) { - curr_result = join(curr_result, lift_from_eq(eq_result)); - curr_result = join(curr_result, visit(curr_result.get_new(), parent)); - } - } - - if (m_cfg.m_memoize) - m_cache.insert(mk_pair(e, curr_result)); - return curr_result; -} - -simp_result simplify_core_fn::visit_fn(expr const & e) { - lean_assert(m_rel == get_eq_name()); - lean_assert(is_app(e)); - buffer args; - expr const & f = get_app_args(e, args); - simp_result r_f = visit(f, some_expr(e)); - return congr_funs(r_f, args); -} - -expr simplify_core_fn::reduce(expr e) { - return reduce_beta_eta_proj_iota(m_ctx, e, m_cfg.m_beta, m_cfg.m_eta, m_cfg.m_proj, m_cfg.m_iota); -} - -simp_result simplify_core_fn::reduce(simp_result r) { - r.update(reduce(r.get_new())); - return r; -} - -simp_result simplify_core_fn::visit_app(expr const & _e) { - lean_assert(is_app(_e)); - expr e = reduce(_e); - e = should_defeq_canonize() ? defeq_canonize_args_step(e) : e; - if (!is_app(e)) - return visit(e, none_expr()); - // (1) Try user-defined congruences - simp_result r_user = try_user_congrs(e); - if (r_user.has_proof()) { - if (m_rel == get_eq_name()) { - return reduce(join(r_user, visit_fn(r_user.get_new()))); - } else { - return reduce(r_user); - } - } - - if (m_rel == get_eq_name()) { - // (2) Synthesize congruence lemma - optional r_args = try_auto_eq_congr(e); - if (r_args) { - return reduce(join(*r_args, visit_fn(r_args->get_new()))); - } - - - // (3) Fall back on generic binary congruence - expr const & f = app_fn(e); - expr const & arg = app_arg(e); - - simp_result r_f = visit(f, some_expr(e)); - - if (is_dependent_fn(f)) { - if (r_f.has_proof()) return reduce(congr_fun(r_f, arg)); - else return reduce(mk_app(r_f.get_new(), arg)); - } else { - simp_result r_arg = visit(arg, some_expr(e)); - return reduce(congr_fun_arg(r_f, r_arg)); - } - } - - return simp_result(e); -} - -bool simplify_core_fn::simplify_constructor_eq_constructor(simp_result & r) { - if (m_rel != get_eq_name()) - return false; /* TODO(Leo): we can add support for <-> */ - expr A, lhs, rhs; - if (!is_eq(r.get_new(), A, lhs, rhs)) - return false; - optional c1 = is_gintro_rule_app(m_ctx.env(), lhs); - if (!c1) return false; - optional c2 = is_gintro_rule_app(m_ctx.env(), rhs); - if (!c2) return false; - - if (*c1 != *c2) { - if (optional not_eq_prf = mk_constructor_ne_constructor_proof(m_ctx, lhs, rhs)) { - expr eq_false_prf = mk_app(m_ctx, get_eq_false_intro_name(), *not_eq_prf); - simp_result new_r(mk_false(), eq_false_prf); - r = join_eq(m_ctx, r, new_r); - return true; - } else { - return false; - } - } else { - A = whnf_ginductive(m_ctx, A); - expr const & A_fn = get_app_fn(A); - if (!is_constant(A_fn) || !is_ginductive(m_ctx.env(), const_name(A_fn))) - return false; - unsigned A_nparams = get_ginductive_num_params(m_ctx.env(), const_name(A_fn)); - if (get_app_num_args(lhs) <= A_nparams) - return false; - name inj_eq_name = mk_injective_eq_name(*c1); - optional inj_eq_info = m_ctx.env().find(inj_eq_name); - if (!inj_eq_info) - return false; - /* We use the `*.inj` lemma for computing the arguments for `*.inj_eq` lemma. */ - try { - name inj_name = mk_injective_name(*c1); - optional inj_info = m_ctx.env().find(inj_name); - if (!inj_info) - return false; - unsigned inj_arity = get_arity(inj_info->get_type()); - type_context_old::tmp_locals locals(m_ctx); - expr H = locals.push_local("_h", r.get_new()); - expr inj = mk_app(m_ctx, inj_name, inj_arity, H); - buffer inj_args; - expr const & inj_fn = get_app_args(inj, inj_args); - expr inj_eq_pr = mk_app(mk_constant(inj_eq_name, const_levels(inj_fn)), inj_args.size() - 1, inj_args.data()); - expr inj_eq = m_ctx.infer(inj_eq_pr); - expr new_lhs, new_rhs; - lean_verify(is_eq(inj_eq, new_lhs, new_rhs)); - simp_result new_r(new_rhs, inj_eq_pr); - r = join_eq(m_ctx, r, new_r); - return true; - } catch (exception &) { - return false; - } - } -} - -optional simplify_core_fn::prove(expr const &) { - return none_expr(); -} - -simp_result simplify_core_fn::visit_lambda(expr const & e) { - return simp_result(reduce(e)); -} - -simp_result simplify_core_fn::visit_pi(expr const & e) { - return try_user_congrs(e); -} - -simp_result simplify_core_fn::visit_let(expr const & e) { - if (m_cfg.m_zeta) - return visit(instantiate(let_body(e), let_value(e)), none_expr()); - else - return simp_result(e); -} - -simp_result simplify_core_fn::visit_macro(expr const & e) { - return simp_result(e); -} - -optional> simplify_core_fn::pre(expr const &, optional const &) { - return optional>(); -} - -optional> simplify_core_fn::post(expr const &, optional const &) { - return optional>(); -} - -simplify_core_fn::simplify_core_fn(type_context_old & ctx, defeq_canonizer::state & dcs, simp_lemmas const & slss, - simp_config const & cfg): - m_ctx(ctx), m_defeq_canonizer(m_ctx, dcs), m_slss(slss), m_cfg(cfg) { -} - -simp_result simplify_core_fn::simplify(expr const & e) { - m_cache.clear(); - simp_result r(e); - while (true) { - m_need_restart = false; - r = join(r, visit(r.get_new(), none_expr())); - if (!m_need_restart || !should_defeq_canonize()) - return r; - m_cache.clear(); - } -} - -simp_result simplify_core_fn::operator()(name const & rel, expr const & e) { - if (m_rel != rel) { - flet _(m_rel, rel); - freset reset_cache(m_cache); - return simplify(e); - } else { - return simplify(e); - } -} - -static expr mk_mpr(type_context_old & ctx, name const & rel, expr const & h1, expr const & h2) { - lean_assert(rel == get_eq_name() || rel == get_iff_name()); - if (rel == get_eq_name()) - return mk_eq_mpr(ctx, h1, h2); - else - return mk_iff_mpr(ctx, h1, h2); -} - -optional simplify_core_fn::prove_by_simp(name const & rel, expr const & e) { - lean_assert(rel == get_eq_name() || rel == get_iff_name()); - simp_result r = operator()(rel, e); - name rrel; - expr lhs, rhs; - if (is_relation(m_ctx.env(), r.get_new(), rrel, lhs, rhs) && - is_refl_relation(m_ctx.env(), rrel) && - m_ctx.is_def_eq(lhs, rhs)) { - if (r.has_proof()) { - return some_expr(mk_mpr(m_ctx, rel, r.get_proof(), mk_refl(m_ctx, rrel, lhs))); - } else { - return some_expr(mk_refl(m_ctx, rrel, lhs)); - } - } else if (is_true(r.get_new())) { - if (r.has_proof()) { - return some_expr(mk_mpr(m_ctx, rel, r.get_proof(), mk_true_intro())); - } else { - return some_expr(mk_true_intro()); - } - } - lean_simp_trace(m_ctx, name({"simplify", "failure"}), tout() << "proof stuck at: " << r.get_new() << "\n";); - return none_expr(); -} - -/* ----------------------------------- - simplify_ext_core_fn - ------------------------------------ */ - -simplify_ext_core_fn::simplify_ext_core_fn(type_context_old & ctx, defeq_can_state & dcs, simp_lemmas const & slss, - simp_config const & cfg): - simplify_core_fn(ctx, dcs, slss, cfg) { -} - -simp_result simplify_ext_core_fn::visit_lambda(expr const & e) { - if (m_rel != get_eq_name() || !m_cfg.m_use_axioms) return simp_result(e); - type_context_old::tmp_locals locals(m_ctx); - expr it = e; - while (is_lambda(it)) { - expr d = instantiate_rev(binding_domain(it), locals.size(), locals.as_buffer().data()); - expr l = locals.push_local(binding_name(it), d, binding_info(it)); - it = binding_body(it); - } - it = instantiate_rev(it, locals.size(), locals.as_buffer().data()); - - simp_result r = visit(it, some_expr(e)); - expr new_body = r.get_new(); - - if (new_body == it) - return simp_result(reduce(e)); - - if (!r.has_proof()) - return reduce(simp_result(locals.mk_lambda(new_body))); - - /* TODO(Leo): the following code can be optimized using the same trick used at - forall_congr. */ - buffer const & ls = locals.as_buffer(); - unsigned i = ls.size(); - expr pr = r.get_proof(); - while (i > 0) { - --i; - expr const & l = ls[i]; - expr lam_pr = m_ctx.mk_lambda(l, pr); - pr = mk_funext(m_ctx, lam_pr); - } - return reduce(simp_result(locals.mk_lambda(new_body), pr)); -} - -simp_result simplify_ext_core_fn::forall_congr(expr const & e) { - lean_assert(m_rel == get_eq_name() || m_rel == get_iff_name()); - buffer pis; - type_context_old::tmp_locals locals(m_ctx); - expr it = e; - while (is_pi(it)) { - expr d = instantiate_rev(binding_domain(it), locals.as_buffer().size(), locals.as_buffer().data()); - if (m_ctx.is_prop(d)) - break; - pis.push_back(it); - locals.push_local(binding_name(it), d, binding_info(it)); - it = binding_body(it); - } - buffer const & ls = locals.as_buffer(); - lean_assert(pis.size() == ls.size()); - expr body = instantiate_rev(it, ls.size(), ls.data()); - simp_result body_r = visit(body, some_expr(e)); - expr new_body = body_r.get_new(); - expr abst_new_body = abstract(new_body, ls.size(), ls.data()); - name lemma_name = m_rel == get_eq_name() ? get_forall_congr_eq_name() : get_forall_congr_name(); - if (body_r.has_proof()) { - expr pr = body_r.get_proof(); - expr Pr = abstract(pr, ls.size(), ls.data()); - unsigned i = pis.size(); - expr Q = abst_new_body; - expr R = abst_new_body; - while (i > 0) { - --i; - expr pi = pis[i]; - expr A = binding_domain(pi); - level A_lvl = get_level(m_ctx, m_ctx.infer(ls[i])); - expr P = mk_lambda(binding_name(pi), A, binding_body(pi)); - expr Q = mk_lambda(binding_name(pi), A, R); - expr H = mk_lambda(binding_name(pi), A, Pr); - Pr = mk_app(mk_constant(lemma_name, {A_lvl}), A, P, Q, H); - R = update_binding(pi, A, R); - } - lean_assert(!has_loose_bvars(Pr)); - return simp_result(R, Pr); - } else if (new_body == body) { - return simp_result(e); - } else { - expr R = abst_new_body; - unsigned i = pis.size(); - while (i > 0) { - --i; - R = update_binding(pis[i], binding_domain(pis[i]), R); - } - return simp_result(R); - } - return simp_result(e); -} - -simp_result simplify_ext_core_fn::imp_congr(expr const & e) { - expr const & a = binding_domain(e); - expr const & b = binding_body(e); - simp_result r_a = visit(a, some_expr(e)); - if (m_cfg.m_contextual) { - type_context_old::tmp_locals locals(m_ctx); - expr h = locals.push_local("_h", r_a.get_new()); - flet set_slss(m_slss, add_to_slss(m_slss, locals.as_buffer())); - freset reset_cache(m_cache); - simp_result r_b = visit(b, some_expr(e)); - if (r_a.get_new() == a && r_b.get_new() == b) { - return e; - } else if (!r_a.has_proof() && !r_b.has_proof()) { - return simp_result(update_binding(e, r_a.get_new(), r_b.get_new())); - } else { - expr fn = mk_constant(m_rel == get_eq_name() ? get_imp_congr_ctx_eq_name() : get_imp_congr_ctx_name()); - expr pr_a = finalize(m_ctx, m_rel, r_a).get_proof(); - expr pr_b = locals.mk_lambda(finalize(m_ctx, m_rel, r_b).get_proof()); - expr pr = mk_app({fn, a, b, r_a.get_new(), r_b.get_new(), pr_a, pr_b}); - return simp_result(update_binding(e, r_a.get_new(), r_b.get_new()), pr); - } - } else { - simp_result r_b = visit(b, some_expr(e)); - if (r_a.get_new() == a && r_b.get_new() == b) { - return e; - } else if (!r_a.has_proof() && !r_b.has_proof()) { - return simp_result(update_binding(e, r_a.get_new(), r_b.get_new())); - } else { - expr fn = mk_constant(m_rel == get_eq_name() ? get_imp_congr_eq_name() : get_imp_congr_name()); - expr pr_a = finalize(m_ctx, m_rel, r_a).get_proof(); - expr pr_b = finalize(m_ctx, m_rel, r_b).get_proof(); - expr pr = mk_app({fn, a, b, r_a.get_new(), r_b.get_new(), pr_a, pr_b}); - return simp_result(update_binding(e, r_a.get_new(), r_b.get_new()), pr); - } - } -} - -simp_result simplify_ext_core_fn::visit_pi(expr const & e) { - if ((m_rel == get_eq_name() && m_cfg.m_use_axioms) || m_rel == get_iff_name()) { - if (m_ctx.is_prop(e)) { - if (!m_ctx.is_prop(binding_domain(e))) - return forall_congr(e); - else if (is_arrow(e)) - return imp_congr(e); - } - } - return simplify_core_fn::visit_pi(e); -} - -simp_result simplify_ext_core_fn::visit_macro(expr const & e) { - return simplify_core_fn::visit_macro(e); -} - -simp_result simplify_ext_core_fn::visit_let(expr const & e) { - /* TODO(Leo): when m_zeta is false, we need to implement efficient code for checking whether the abstraction of - a let-body is type correct or not */ - return simplify_core_fn::visit_let(e); -} - -static optional> to_ext_result(simp_result const & r) { - return optional>(r, true); -} - -static optional> no_ext_result() { - return optional>(); -} - -optional> simplify_fn::pre(expr const &, optional const &) { - return no_ext_result(); -} - -// TODO(Leo): move to a different file -static optional unfold_using_nontrivial_eqns(type_context_old & ctx, expr const & e) { - if (!is_app(e)) return none_expr(); - expr const & f = get_app_fn(e); - if (!is_constant(f)) return none_expr(); - if (has_simple_eqn_lemma(ctx.env(), const_name(f))) return none_expr(); - type_context_old::transparency_scope scope(ctx, transparency_mode::Semireducible); - return ctx.unfold_definition(e); -} - -optional> simplify_fn::post(expr const & e, optional const &) { - if (auto r = unfold_step(m_ctx, e, m_to_unfold, false)) - return to_ext_result(simp_result(*r)); - if (m_cfg.m_iota_eqn) { - if (auto r = unfold_using_nontrivial_eqns(m_ctx, e)) - return to_ext_result(simp_result(*r)); - } - simp_result r = rewrite(e); - if (r.get_new() != e) { - return to_ext_result(r); - } else if (!m_cfg.m_use_axioms) { - return no_ext_result(); - } else { - r = propext_rewrite(e); - if (r.get_new() != e) - return to_ext_result(r); - else - return no_ext_result(); - } -} - -optional simplify_fn::prove(expr const & e) { - return prove_by_simp(get_iff_name(), e); -} - -class vm_simplify_fn : public simplify_ext_core_fn { - vm_obj m_a; - vm_obj m_prove; - vm_obj m_pre; - vm_obj m_post; - tactic_state m_s; - - optional> invoke_fn(vm_obj const & fn, expr const & e, optional const & parent) { - m_s = set_mctx_lctx_dcs(m_s, m_ctx.mctx(), m_ctx.lctx(), m_defeq_canonizer.get_state()); - vm_obj r = invoke(fn, m_a, to_obj(m_slss), to_obj(m_rel), to_obj(parent), to_obj(e), to_obj(m_s)); - /* r : tactic_state (A × expr × option expr × bool) */ - if (optional new_s = tactic::is_success(r)) { - m_s = *new_s; - m_ctx.set_mctx(m_s.mctx()); - m_defeq_canonizer.set_state(m_s.dcs()); - vm_obj t = tactic::get_success_value(r); - /* t : A × expr × option expr × bool */ - m_a = cfield(t, 0); - vm_obj t1 = cfield(t, 1); - expr new_e = to_expr(cfield(t1, 0)); - vm_obj t2 = cfield(t1, 1); - optional new_pr; - vm_obj vpr = cfield(t2, 0); - if (!is_none(vpr)) - new_pr = to_expr(get_some_value(vpr)); - bool flag = to_bool(cfield(t2, 1)); - return optional>(simp_result(new_e, new_pr), flag); - } else { - return no_ext_result(); - } - } - - virtual optional> pre(expr const & e, optional const & parent) override { - return invoke_fn(m_pre, e, parent); - } - - virtual optional> post(expr const & e, optional const & parent) override { - return invoke_fn(m_post, e, parent); - } - - virtual optional prove(expr const & e) override { - auto s = mk_tactic_state_for(m_ctx.env(), m_ctx.get_options(), m_s.decl_name(), m_ctx.lctx(), e); - vm_obj r_obj = invoke(m_prove, m_a, to_obj(s)); - optional s_new = tactic::is_success(r_obj); - if (!s_new || s_new->goals()) return none_expr(); - metavar_context mctx = s_new->mctx(); - expr result = mctx.instantiate_mvars(s_new->main()); - if (has_expr_metavar(result)) return none_expr(); - m_a = cfield(r_obj, 0); - m_ctx.set_mctx(mctx); - return some_expr(result); - } - -public: - vm_simplify_fn(type_context_old & ctx, defeq_can_state & dcs, simp_lemmas const & slss, simp_config const & cfg, - vm_obj const & prove, vm_obj const & pre, vm_obj const & post, tactic_state const & s): - simplify_ext_core_fn(ctx, dcs, slss, cfg), - m_prove(prove), m_pre(pre), m_post(post), - m_s(s) {} - - pair operator()(vm_obj const & a, name const & rel, expr const & e) { - m_a = a; - auto r = simplify_ext_core_fn::operator()(rel, e); - return mk_pair(m_a, r); - } -}; - -class tactic_simplify_fn : public simplify_fn { - tactic_state m_s; - vm_obj m_prove; - - optional prove_core(expr const & e) { - auto s = mk_tactic_state_for(m_ctx.env(), m_ctx.get_options(), m_s.decl_name(), m_ctx.lctx(), e); - vm_obj r_obj = invoke(m_prove, to_obj(s)); - optional s_new = tactic::is_success(r_obj); - if (!s_new || s_new->goals()) return none_expr(); - metavar_context mctx = s_new->mctx(); - expr result = mctx.instantiate_mvars(s_new->main()); - if (has_expr_metavar(result)) return none_expr(); - m_ctx.set_mctx(mctx); - return some_expr(result); - } - - virtual optional prove(expr const & e) override { - if (auto r = prove_core(e)) - return r; - else - return simplify_fn::prove(e); - } - -public: - tactic_simplify_fn(type_context_old & ctx, defeq_canonizer::state & dcs, simp_lemmas const & slss, names const & to_unfold, - simp_config const & cfg, tactic_state const & s, vm_obj const & prove): - simplify_fn(ctx, dcs, slss, to_unfold, cfg), - m_s(s), - m_prove(prove) { - } -}; - -/* -meta constant simplify - (s : simp_lemmas) - (u : list name) - (e : expr) - (c : simp_config) - (r : name) - (prove : tactic unit) - : tactic (expr × expr) -*/ -vm_obj tactic_simplify(vm_obj const & slss, vm_obj const & u, vm_obj const & e, vm_obj const & c, vm_obj const & rel, - vm_obj const & prove, vm_obj const & _s) { - tactic_state s = tactic::to_state(_s); - try { - simp_config cfg(c); - tactic_state_context_cache cache(s); - type_context_old ctx = cache.mk_type_context(transparency_mode::Reducible); - defeq_can_state dcs = s.dcs(); - tactic_simplify_fn simp(ctx, dcs, to_simp_lemmas(slss), to_names(u), cfg, s, prove); - simp_result result = simp(to_name(rel), to_expr(e)); - if (!cfg.m_fail_if_unchanged || result.get_new() != to_expr(e)) { - result = finalize(ctx, to_name(rel), result); - tactic_state new_s = set_dcs(s, dcs); - return tactic::mk_success(mk_vm_pair(to_obj(result.get_new()), to_obj(result.get_proof())), new_s); - } else { - return tactic::mk_exception("simplify tactic failed to simplify", s); - } - } catch (exception & e) { - return tactic::mk_exception(std::current_exception(), s); - } -} - -static vm_obj ext_simplify_core(vm_obj const & a, vm_obj const & c, simp_lemmas const & slss, vm_obj const & prove, - vm_obj const & pre, vm_obj const & post, name const & r, expr const & e, - tactic_state s) { - try { - simp_config cfg(c); - tactic_state_context_cache cache(s); - type_context_old ctx = cache.mk_type_context(transparency_mode::Reducible); - defeq_can_state dcs = s.dcs(); - vm_simplify_fn simp(ctx, dcs, slss, cfg, prove, pre, post, s); - pair p = simp(a, r, e); - if (!cfg.m_fail_if_unchanged || p.second.get_new() != e) { - vm_obj const & a = p.first; - simp_result result = finalize(ctx, r, p.second); - tactic_state new_s = set_dcs(s, dcs); - return tactic::mk_success(mk_vm_pair(a, mk_vm_pair(to_obj(result.get_new()), to_obj(result.get_proof()))), new_s); - } else { - return tactic::mk_exception("simplify tactic failed to simplify", s); - } - } catch (exception & e) { - return tactic::mk_exception(std::current_exception(), s); - } -} - -/* -meta constant ext_simplify_core - {A : Type} - (a : A) - (c : simp_config) - (l : simp_lemmas) - (prove : A → tactic A) - (pre : A → name → simp_lemmas → option expr → expr → tactic (A × expr × option expr × bool)) - (post : A → name → simp_lemmas → option expr → expr → tactic (A × expr × option expr × bool)) - (r : name) : - expr → tactic (A × expr × expr) -*/ -vm_obj tactic_ext_simplify_core(unsigned DEBUG_CODE(num), vm_obj const * args) { - lean_assert(num == 10); - return ext_simplify_core(args[1], args[2], to_simp_lemmas(args[3]), args[4], args[5], args[6], - to_name(args[7]), to_expr(args[8]), tactic::to_state(args[9])); -} - -void initialize_simplify() { - register_trace_class("simplify"); - register_trace_class(name({"simplify", "failure"})); - register_trace_class(name({"simplify", "rewrite_failure"})); - register_trace_class(name({"simplify", "context"})); - register_trace_class(name({"simplify", "canonize"})); - register_trace_class(name({"simplify", "congruence"})); - register_trace_class(name({"simplify", "rewrite"})); - register_trace_class(name({"simplify", "perm"})); - register_trace_class(name({"debug", "simplify", "try_congruence"})); - - DECLARE_VM_BUILTIN(name({"tactic", "simplify"}), tactic_simplify); - declare_vm_builtin(name({"tactic", "ext_simplify_core"}), - "tactic_ext_simplify_core", 10, tactic_ext_simplify_core); -} - -void finalize_simplify() { -} -} diff --git a/src/library/tactic/simplify.h b/src/library/tactic/simplify.h deleted file mode 100644 index 51f9bfd52c..0000000000 --- a/src/library/tactic/simplify.h +++ /dev/null @@ -1,197 +0,0 @@ -/* -Copyright (c) 2015 Daniel Selsam. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Author: Daniel Selsam, Leonardo de Moura -*/ -#pragma once -#include "kernel/expr_pair.h" -#include "library/type_context.h" -#include "library/defeq_canonizer.h" -#include "library/vm/vm.h" -#include "library/tactic/simp_lemmas.h" -#include "library/tactic/simp_result.h" - -namespace lean { - -/* -structure simp_config := -(max_steps : nat) -(contextual : bool) -(lift_eq : bool) -(canonize_instances : bool) -(canonize_proofs : bool) -(use_axioms : bool) -(zeta : bool) -(beta : bool) -(eta : bool) -(proj : bool) -(iota : bool) -(iota_eqn : bool) -(constructor_eq : bool) -(single_pass : bool) -(fail_if_unchaged : bool) -(memoize : bool) -*/ -struct simp_config { - unsigned m_max_steps; - bool m_contextual; - bool m_lift_eq; - bool m_canonize_instances; - bool m_canonize_proofs; - bool m_use_axioms; - bool m_zeta; - bool m_beta; - bool m_eta; - bool m_proj; - bool m_iota; - bool m_iota_eqn; - bool m_constructor_eq; - bool m_single_pass; - bool m_fail_if_unchanged; - bool m_memoize; - simp_config(); - simp_config(vm_obj const & o); -}; - -/* Core simplification procedure. It performs the following tasks: - 1- Manages the cache; - 2- Applies congruence lemmas; - 3- Canonizes instances & proofs; - 4- Manages contextual rewriting - - This is a base class for many simplification strategies. - Its behavior can be configured by overriding its virtual methods. - This class does *not* apply any simp lemma, nor it tries to - put subterms in weak-head-normal-form. - - This class also does *not* use axioms. For example, it will - not use funext to go inside lambda terms. This feature is provided - by subclasses. - - Remark: it is debatable whether the options m_lift_eq, m_canonize_instances and - m_canonize_proofs really need to be here. They may be moved to subclasses in the - future. -*/ -class simplify_core_fn { -protected: - typedef expr_map simplify_cache; - - type_context_old & m_ctx; - defeq_canonizer m_defeq_canonizer; - name m_rel; - simp_lemmas m_slss; - simplify_cache m_cache; - - /* Logging */ - unsigned m_num_steps{0}; - bool m_need_restart{false}; - - /* Options */ - simp_config m_cfg; - - simp_result join(simp_result const & r1, simp_result const & r2); - void inc_num_steps(); - bool is_dependent_fn(expr const & f); - bool should_defeq_canonize() const { - return m_cfg.m_canonize_instances || m_cfg.m_canonize_proofs; - } - bool instantiate_emetas(tmp_type_context & tmp_tctx, list const & emetas, - list const & instances); - simp_result lift_from_eq(simp_result const & r_eq); - simp_lemmas add_to_slss(simp_lemmas const & slss, buffer const & ls); - expr remove_unnecessary_casts(expr const & e); - expr defeq_canonize_args_step(expr const & e); - - /* Congruence */ - simp_result try_user_congrs(expr const & e); - simp_result try_user_congr(expr const & e, simp_lemma const & cr); - - optional try_auto_eq_congr(expr const & e); - - simp_result congr_fun_arg(simp_result const & r_f, simp_result const & r_arg); - simp_result congr(simp_result const & r_f, simp_result const & r_arg); - simp_result congr_fun(simp_result const & r_f, expr const & arg); - simp_result congr_arg(expr const & f, simp_result const & r_arg); - simp_result congr_funs(simp_result const & r_f, buffer const & args); - - /* Rewriting - Remark: the rewriting methods are implemented on this base class once and for all, - but used in subclasses.*/ - simp_result rewrite(expr const & e); - simp_result rewrite(expr const & e, simp_lemma const & sl); - simp_result rewrite_core(expr const & e, simp_lemma const & sl); - simp_result propext_rewrite(expr const & e); - - /* Simplify equalities of the form (c ... = c' ...) where `c` and `c'` are - constructors. - - Return true if `r` was simplified. */ - bool simplify_constructor_eq_constructor(simp_result & r); - - /* Visitors */ - virtual optional> pre(expr const & e, optional const & parent); - virtual optional> post(expr const & e, optional const & parent); - - virtual optional prove(expr const & goal); - friend class simp_prover; - - simp_result visit_fn(expr const & e); - virtual simp_result visit_lambda(expr const & e); - virtual simp_result visit_pi(expr const & e); - virtual simp_result visit_let(expr const & e); - virtual simp_result visit_app(expr const & e); - virtual simp_result visit_macro(expr const & e); - - virtual simp_result visit(expr const & e, optional const & parent); - - simp_result simplify(expr const & e); - - /* Apply conversion rules: beta, projection */ - expr reduce(expr e); - simp_result reduce(simp_result r); - - bool match(tmp_type_context & ctx, simp_lemma const & sl, expr const & t); - -public: - simplify_core_fn(type_context_old & ctx, defeq_canonizer::state & dcs, simp_lemmas const & slss, - simp_config const & cfg); - - environment const & env() const; - simp_result operator()(name const & rel, expr const & e); - - optional prove_by_simp(name const & rel, expr const & e); -}; - -/* Extend simplify_core_fn functionality by assuming function - extensionality and propositional extensionality. */ -class simplify_ext_core_fn : public simplify_core_fn { -protected: - simp_result forall_congr(expr const & e); - simp_result imp_congr(expr const & e); - virtual simp_result visit_lambda(expr const & e) override; - virtual simp_result visit_pi(expr const & e) override; - virtual simp_result visit_let(expr const & e) override; - virtual simp_result visit_macro(expr const & e) override; -public: - simplify_ext_core_fn(type_context_old & ctx, defeq_canonizer::state & dcs, simp_lemmas const & slss, - simp_config const & cfg); -}; - -/* Default (bottom-up) simplifier: reduce projections, apply simplification lemmas, - and use itself to discharge hypotheses. */ -class simplify_fn : public simplify_ext_core_fn { -protected: - name_set m_to_unfold; - virtual optional> pre(expr const & e, optional const & parent) override; - virtual optional> post(expr const & e, optional const & parent) override; - virtual optional prove(expr const & e) override; -public: - simplify_fn(type_context_old & ctx, defeq_canonizer::state & dcs, simp_lemmas const & slss, names const & to_unfold, - simp_config const & cfg): - simplify_ext_core_fn(ctx, dcs, slss, cfg), - m_to_unfold(to_name_set(to_unfold)) {} -}; - -void initialize_simplify(); -void finalize_simplify(); -}