From 4d52de6f33fb7331471a0b2cea4e94651dd7f829 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 18 Oct 2016 16:18:25 -0700 Subject: [PATCH] refactor(library/tactic/simplify): add simplify subclasses, and use new simplifier at nested --- library/init/classical.lean | 6 +- library/init/congr.lean | 16 ++ library/init/logic.lean | 4 +- library/init/simplifier.lean | 6 +- src/library/constants.cpp | 16 ++ src/library/constants.h | 4 + src/library/constants.txt | 4 + src/library/inductive_compiler/nested.cpp | 30 +- src/library/tactic/simplify.cpp | 318 +++++++++++++++++++++- src/library/tactic/simplify.h | 53 ++-- src/library/vm/vm_expr.cpp | 4 + src/library/vm/vm_expr.h | 1 + 12 files changed, 412 insertions(+), 50 deletions(-) create mode 100644 library/init/congr.lean diff --git a/library/init/classical.lean b/library/init/classical.lean index 20fa565c58..c86d23f3ed 100644 --- a/library/init/classical.lean +++ b/library/init/classical.lean @@ -143,13 +143,13 @@ cases_true_false (λ x, x = false ∨ x = true) (or.inl rfl) a -theorem eq.of_iff {a b : Prop} (h : a ↔ b) : a = b := +theorem iff.to_eq {a b : Prop} (h : a ↔ b) : a = b := iff.elim (assume h1 h2, propext (iff.intro h1 h2)) h theorem iff_eq_eq {a b : Prop} : (a ↔ b) = (a = b) := propext (iff.intro - (assume h, eq.of_iff h) - (assume h, iff.of_eq h)) + (assume h, iff.to_eq h) + (assume h, h^.to_iff)) lemma eq_false {a : Prop} : (a = false) = (¬ a) := have (a ↔ false) = (¬ a), from propext (iff_false a), diff --git a/library/init/congr.lean b/library/init/congr.lean new file mode 100644 index 0000000000..4c67ea1ae2 --- /dev/null +++ b/library/init/congr.lean @@ -0,0 +1,16 @@ +/- +Copyright (c) 2016 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: Leonardo de Moura + +Additional congruence lemmas. +-/ +prelude +import init.quot +universe variables u v + +lemma forall_congr_eq {A : Type u} {p q : A → Prop} (h : ∀ a, p a = q a) : (∀ a, p a) = ∀ a, q a := +propext (forall_congr (λ a, (h a)^.to_iff)) + +lemma imp_congr_eq {a b c d : Prop} (h₁ : a = c) (h₂ : b = d) : (a → b) = (c → d) := +propext (imp_congr h₁^.to_iff h₂^.to_iff) diff --git a/library/init/logic.lean b/library/init/logic.lean index cc216ad72b..17c665870f 100644 --- a/library/init/logic.lean +++ b/library/init/logic.lean @@ -281,7 +281,7 @@ iff.intro (iff.elim_right h) (iff.elim_left h) lemma iff.comm : (a ↔ b) ↔ (b ↔ a) := iff.intro iff.symm iff.symm -lemma iff.of_eq {a b : Prop} (h : a = b) : a ↔ b := +lemma eq.to_iff {a b : Prop} (h : a = b) : a ↔ b := eq.rec_on h iff.rfl lemma not_iff_not_of_iff (h₁ : a ↔ b) : ¬a ↔ ¬b := @@ -646,7 +646,7 @@ section else is_false (iff.mp (not_iff_not_of_iff h) hp) def decidable_of_decidable_of_eq (hp : decidable p) (h : p = q) : decidable q := - decidable_of_decidable_of_iff hp (iff.of_eq h) + decidable_of_decidable_of_iff hp h^.to_iff protected def or.by_cases [decidable p] [decidable q] {A : Type u} (h : p ∨ q) (h₁ : p → A) (h₂ : q → A) : A := diff --git a/library/init/simplifier.lean b/library/init/simplifier.lean index d7b8a4ad55..e7e43b9936 100644 --- a/library/init/simplifier.lean +++ b/library/init/simplifier.lean @@ -16,11 +16,7 @@ is_associative.mk (λ x y z, propext (@or.assoc x y z)) -- Basic congruence theorems over equality (using propext) attribute [congr] theorem imp_congr_ctx_eq {P₁ P₂ Q₁ Q₂ : Prop} (H₁ : P₁ = P₂) (H₂ : P₂ → (Q₁ = Q₂)) : (P₁ → Q₁) = (P₂ → Q₂) := -propext (imp_congr_ctx (iff.of_eq H₁) (assume p₂, iff.of_eq (H₂ p₂))) - -attribute [congr] -theorem forall_congr_eq {A : Type u} (P Q : A → Prop) (H : ∀ a, P a = Q a) : ((∀ a, P a) = (∀ a, Q a)) := -propext (forall_congr (assume a, iff.of_eq (H a))) +propext (imp_congr_ctx H₁^.to_iff (assume p₂, (H₂ p₂)^.to_iff)) -- Congruence theorems for flattening namespace simplifier diff --git a/src/library/constants.cpp b/src/library/constants.cpp index 8043d32038..b8d405a72a 100644 --- a/src/library/constants.cpp +++ b/src/library/constants.cpp @@ -78,6 +78,8 @@ name const * g_false_rec = nullptr; name const * g_field = nullptr; name const * g_fin = nullptr; name const * g_fin_mk = nullptr; +name const * g_forall_congr = nullptr; +name const * g_forall_congr_eq = nullptr; name const * g_funext = nullptr; name const * g_ge = nullptr; name const * g_get_line = nullptr; @@ -116,6 +118,8 @@ name const * g_iff_refl = nullptr; name const * g_iff_symm = nullptr; name const * g_iff_trans = nullptr; name const * g_iff_true_intro = nullptr; +name const * g_imp_congr = nullptr; +name const * g_imp_congr_eq = nullptr; name const * g_implies = nullptr; name const * g_implies_of_if_neg = nullptr; name const * g_implies_of_if_pos = nullptr; @@ -460,6 +464,8 @@ void initialize_constants() { g_field = new name{"field"}; g_fin = new name{"fin"}; g_fin_mk = new name{"fin", "mk"}; + g_forall_congr = new name{"forall_congr"}; + g_forall_congr_eq = new name{"forall_congr_eq"}; g_funext = new name{"funext"}; g_ge = new name{"ge"}; g_get_line = new name{"get_line"}; @@ -498,6 +504,8 @@ void initialize_constants() { g_iff_symm = new name{"iff", "symm"}; g_iff_trans = new name{"iff", "trans"}; g_iff_true_intro = new name{"iff_true_intro"}; + g_imp_congr = new name{"imp_congr"}; + g_imp_congr_eq = new name{"imp_congr_eq"}; g_implies = new name{"implies"}; g_implies_of_if_neg = new name{"implies_of_if_neg"}; g_implies_of_if_pos = new name{"implies_of_if_pos"}; @@ -843,6 +851,8 @@ void finalize_constants() { delete g_field; delete g_fin; delete g_fin_mk; + delete g_forall_congr; + delete g_forall_congr_eq; delete g_funext; delete g_ge; delete g_get_line; @@ -881,6 +891,8 @@ void finalize_constants() { delete g_iff_symm; delete g_iff_trans; delete g_iff_true_intro; + delete g_imp_congr; + delete g_imp_congr_eq; delete g_implies; delete g_implies_of_if_neg; delete g_implies_of_if_pos; @@ -1225,6 +1237,8 @@ name const & get_false_rec_name() { return *g_false_rec; } name const & get_field_name() { return *g_field; } name const & get_fin_name() { return *g_fin; } name const & get_fin_mk_name() { return *g_fin_mk; } +name const & get_forall_congr_name() { return *g_forall_congr; } +name const & get_forall_congr_eq_name() { return *g_forall_congr_eq; } name const & get_funext_name() { return *g_funext; } name const & get_ge_name() { return *g_ge; } name const & get_get_line_name() { return *g_get_line; } @@ -1263,6 +1277,8 @@ name const & get_iff_refl_name() { return *g_iff_refl; } name const & get_iff_symm_name() { return *g_iff_symm; } name const & get_iff_trans_name() { return *g_iff_trans; } name const & get_iff_true_intro_name() { return *g_iff_true_intro; } +name const & get_imp_congr_name() { return *g_imp_congr; } +name const & get_imp_congr_eq_name() { return *g_imp_congr_eq; } name const & get_implies_name() { return *g_implies; } name const & get_implies_of_if_neg_name() { return *g_implies_of_if_neg; } name const & get_implies_of_if_pos_name() { return *g_implies_of_if_pos; } diff --git a/src/library/constants.h b/src/library/constants.h index 3bd8a4ee3a..082d79933b 100644 --- a/src/library/constants.h +++ b/src/library/constants.h @@ -80,6 +80,8 @@ name const & get_false_rec_name(); name const & get_field_name(); name const & get_fin_name(); name const & get_fin_mk_name(); +name const & get_forall_congr_name(); +name const & get_forall_congr_eq_name(); name const & get_funext_name(); name const & get_ge_name(); name const & get_get_line_name(); @@ -118,6 +120,8 @@ name const & get_iff_refl_name(); name const & get_iff_symm_name(); name const & get_iff_trans_name(); name const & get_iff_true_intro_name(); +name const & get_imp_congr_name(); +name const & get_imp_congr_eq_name(); name const & get_implies_name(); name const & get_implies_of_if_neg_name(); name const & get_implies_of_if_pos_name(); diff --git a/src/library/constants.txt b/src/library/constants.txt index 26ed31e486..c84fbddd42 100644 --- a/src/library/constants.txt +++ b/src/library/constants.txt @@ -73,6 +73,8 @@ false.rec field fin fin.mk +forall_congr +forall_congr_eq funext ge get_line @@ -111,6 +113,8 @@ iff.refl iff.symm iff.trans iff_true_intro +imp_congr +imp_congr_eq implies implies_of_if_neg implies_of_if_pos diff --git a/src/library/inductive_compiler/nested.cpp b/src/library/inductive_compiler/nested.cpp index ca33d4ddcf..4079a5c0e8 100644 --- a/src/library/inductive_compiler/nested.cpp +++ b/src/library/inductive_compiler/nested.cpp @@ -1251,35 +1251,31 @@ class add_nested_inductive_decl_fn { return simp_result(h_a, pr); } - options get_simp_options(options opts) { - opts = remove_all_with_prefix(get_simplify_prefix_name(), m_tctx.get_options()); - opts = opts.update(get_simplify_max_steps_name(), 100000); - opts = opts.update(get_simplify_contextual_name(), false); - opts = opts.update(get_simplify_rewrite_name(), true); - opts = opts.update(get_simplify_lift_eq_name(), false); - opts = opts.update(get_simplify_canonize_instances_fixed_point_name(), false); - opts = opts.update(get_simplify_canonize_proofs_fixed_point_name(), false); - return opts; - } - expr prove_by_simp(local_context const & lctx, expr const & thm, list Hs, bool use_sizeof) { - type_context tctx(m_env, get_simp_options(m_tctx.get_options()), lctx, transparency_mode::Semireducible); - type_context tctx_whnf(m_env, get_simp_options(m_tctx.get_options()), lctx, transparency_mode::None); - + type_context tctx(m_env, m_tctx.get_options(), lctx, transparency_mode::Semireducible); + type_context tctx_whnf(m_env, m_tctx.get_options(), lctx, transparency_mode::None); simp_lemmas all_lemmas = use_sizeof ? join(m_sizeof_lemmas, m_lemmas) : m_lemmas; for (expr const & H : Hs) { expr H_type = tctx_whnf.infer(H); all_lemmas = add(tctx_whnf, all_lemmas, mlocal_name(H), H_type, H, LEAN_DEFAULT_PRIORITY); } - lean_trace(name({"inductive_compiler", "nested", "simp", "start"}), tout() << thm << "\n";); - auto thm_pr = prove_eq_by_simp(tctx, tctx_whnf, all_lemmas, thm); + unsigned max_steps = 1000000; + bool contextual = false; + bool lift_eq = false; + bool canonize_instances = false; + bool canonize_proofs = false; + bool use_axioms = false; + simplify_fn simplifier(tctx, all_lemmas, max_steps, contextual, lift_eq, + canonize_instances, canonize_proofs, use_axioms); + auto thm_pr = simplifier.prove_by_simp(get_eq_name(), thm); if (!thm_pr) { formatter_factory const & fmtf = get_global_ios().get_formatter_factory(); lean_trace(name({"inductive_compiler", "nested", "simp", "failure"}), tout() << "\n-------------------\n" << lctx.pp(fmtf(m_env, m_tctx.get_options(), m_tctx)) << "\n";); - throw exception("simplifier failed to prove goal; trace 'inductive_compiler.nested.simp.failure' for more information"); + throw exception("simplifier failed to prove goal; trace 'inductive_compiler.nested.simp.failure' " + "for more information"); } return *thm_pr; } diff --git a/src/library/tactic/simplify.cpp b/src/library/tactic/simplify.cpp index 5ebae2772f..d4d7b428da 100644 --- a/src/library/tactic/simplify.cpp +++ b/src/library/tactic/simplify.cpp @@ -30,6 +30,7 @@ Author: Daniel Selsam, Leonardo de Moura #include "library/congr_lemma.h" #include "library/fun_info.h" #include "library/vm/vm_expr.h" +#include "library/vm/vm_option.h" #include "library/vm/vm_list.h" #include "library/vm/vm_name.h" #include "library/tactic/tactic_state.h" @@ -39,7 +40,7 @@ Author: Daniel Selsam, Leonardo de Moura #include "library/tactic/simplify.h" #ifndef LEAN_DEFAULT_SIMPLIFY_MAX_STEPS -#define LEAN_DEFAULT_SIMPLIFY_MAX_STEPS 10000 +#define LEAN_DEFAULT_SIMPLIFY_MAX_STEPS 1000000 #endif #ifndef LEAN_DEFAULT_SIMPLIFY_CONTEXTUAL #define LEAN_DEFAULT_SIMPLIFY_CONTEXTUAL true @@ -60,6 +61,10 @@ Author: Daniel Selsam, Leonardo de Moura namespace lean { #define lean_simp_trace(CTX, N, CODE) lean_trace(N, scope_trace_env _scope1(CTX.env(), CTX); CODE) +/* ----------------------------------- + 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); } @@ -239,7 +244,8 @@ simp_result simplify_core_fn::try_user_congr(expr const & e, simp_lemma const & 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 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_metavar(l)); m_type = binding_body(m_type); @@ -463,6 +469,64 @@ simp_result simplify_core_fn::congr_funs(simp_result const & r_f, buffer c 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) { + lean_trace_d(name({"debug", "simplify", "try_rewrite"}), tout() << "no simp lemmas for: " << e << "\n";); + return simp_result(e); + } + + for (simp_lemma const & lemma : *srs) { + simp_result r = rewrite(e, lemma); + if (!is_eqp(r.get_new(), e)) { + lean_trace_d(name({"simplify", "rewrite"}), tout() << "[" << lemma.get_id() << "]: " << e + << " ==> " << r.get_new() << "\n";); + return r; + } + } + + return simp_result(e); +} + +simp_result simplify_core_fn::rewrite(expr const & e, simp_lemma const & sl) { + tmp_type_context tmp_ctx(m_ctx, sl.get_num_umeta(), sl.get_num_emeta()); + if (!tmp_ctx.is_def_eq(e, sl.get_lhs())) { + lean_trace_d(name({"debug", "simplify", "rewrite"}), tout() << "fail to unify: " << sl.get_id() << "\n";); + return simp_result(e); + } + + if (!instantiate_emetas(tmp_ctx, sl.get_num_emeta(), sl.get_emetas(), sl.get_instances())) { + lean_trace_d(name({"debug", "simplify", "rewrite"}), tout() << "fail to instantiate emetas: " << + sl.get_id() << "\n";); + return simp_result(e); + } + + for (unsigned i = 0; i < sl.get_num_umeta(); i++) { + if (!tmp_ctx.is_uassigned(i)) + 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 (sl.is_permutation()) { + if (!is_lt(new_rhs, new_lhs, false)) { + lean_simp_trace(tmp_ctx, name({"simplify", "perm"}), + tout() << "perm rejected: " << new_rhs << " !< " << new_lhs << "\n";); + return simp_result(e); + } + } + + if (sl.is_refl()) { + return simp_result(new_rhs); + } else { + expr pf = tmp_ctx.instantiate_mvars(sl.get_proof()); + return simp_result(new_rhs, pf); + } +} + simp_result simplify_core_fn::visit(expr const & e, optional const & parent) { check_system("simplify"); inc_num_steps(); @@ -635,6 +699,238 @@ simp_result simplify_core_fn::operator()(name const & rel, expr const & e) { } } +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 const & mpr = rel == get_eq_name() ? get_eq_mpr_name() : get_iff_mpr_name(); + + 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_app(m_ctx, mpr, 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_app(m_ctx, mpr, r.get_proof(), mk_true_intro())); + } else { + return some_expr(mk_true_intro()); + } + } + return none_expr(); +} + +/* ----------------------------------- + simplify_ext_core_fn + ------------------------------------ */ + +simplify_ext_core_fn::simplify_ext_core_fn(type_context & ctx, simp_lemmas const & slss, + unsigned max_steps, bool contextual, bool lift_eq, + bool canonize_instances, bool canonize_proofs, + bool use_axioms): + simplify_core_fn(ctx, slss, max_steps, contextual, lift_eq, canonize_instances, canonize_proofs), + m_use_axioms (use_axioms) { +} + +simp_result simplify_ext_core_fn::visit_lambda(expr const & e) { + if (m_rel != get_eq_name() || !m_use_axioms) return simp_result(e); + type_context::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(e); + + if (!r.has_proof()) + return simp_result(locals.mk_lambda(new_body)); + + // TODO(Leo): create funext proof + return simp_result(e); +} + +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::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_locals(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_locals(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(closed(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) { + // TODO(Leo) + return simp_result(e); +} + +simp_result simplify_ext_core_fn::visit_pi(expr const & e) { + if ((m_rel == get_eq_name() && 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_let(expr const & e) { + /* TODO(Leo): we need to implement efficient code for checking whether the abstraction of + a let-body is type correct or not */ + return simp_result(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 & e, optional const &) { + if (auto r = m_ctx.reduce_projection(e)) + return to_ext_result(simp_result(*r)); + else + return no_ext_result(); +} + +optional> simplify_fn::post(expr const & e, optional const &) { + simp_result r = rewrite(e); + if (r.get_new() != e) + return to_ext_result(r); + else + return no_ext_result(); +} + +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(m_s, m_ctx.mctx(), m_ctx.lctx()); + vm_obj r = invoke(fn, m_a, to_obj(m_rel), to_obj(m_slss), to_obj(parent), to_obj(e), to_obj(m_s)); + /* r : tactic_state (A × expr × option expr × bool) */ + if (optional new_s = is_tactic_success(r)) { + m_s = *new_s; + m_ctx.set_mctx(m_s.mctx()); + vm_obj t = cfield(r, 0); + /* 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 { + tactic_state s = mk_tactic_state_for(m_ctx.env(), m_ctx.get_options(), m_ctx.lctx(), e); + vm_obj r_obj = invoke(m_prove, m_a, to_obj(s)); + optional s_new = is_tactic_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 & ctx, simp_lemmas const & slss, + unsigned max_steps, bool contextual, bool lift_eq, + bool canonize_instances, bool canonize_proofs, bool use_axioms, + vm_obj const & prove, vm_obj const & pre, vm_obj const & post): + simplify_ext_core_fn(ctx, slss, max_steps, contextual, lift_eq, + canonize_instances, canonize_proofs, use_axioms), + m_prove(prove), m_pre(pre), m_post(post), + m_s(mk_tactic_state_for(ctx.env(), ctx.get_options(), ctx.mctx(), ctx.lctx(), mk_true())) {} +}; + +void initialize_new_simplify() { +} + +void finalize_new_simplify() { +} + +/* LEGACY */ + + static name * g_simplify_prefix = nullptr; name get_simplify_prefix_name() { return *g_simplify_prefix; } @@ -672,7 +968,8 @@ static bool get_simplify_lift_eq(options const & o) { } static bool get_simplify_canonize_instances_fixed_point(options const & o) { - return o.get_bool(*g_simplify_canonize_instances_fixed_point, LEAN_DEFAULT_SIMPLIFY_DEFEQ_CANONIZE_INSTANCES_FIXED_POINT); + return o.get_bool(*g_simplify_canonize_instances_fixed_point, + LEAN_DEFAULT_SIMPLIFY_DEFEQ_CANONIZE_INSTANCES_FIXED_POINT); } static bool get_simplify_canonize_proofs_fixed_point(options const & o) { @@ -739,7 +1036,8 @@ class simplifier { return m_canonize_instances_fixed_point || m_canonize_proofs_fixed_point; } - bool instantiate_emetas(tmp_type_context & tmp_tctx, unsigned num_emeta, list const & emetas, list const & instances); + bool instantiate_emetas(tmp_type_context & tmp_tctx, unsigned num_emeta, + list const & emetas, list const & instances); /* Simp_Results */ simp_result lift_from_eq(expr const & old_e, simp_result const & r_eq); @@ -796,7 +1094,8 @@ class simplifier { for (simp_lemma const & lemma : *srs) { simp_result r = rewrite_binary(e, lemma); if (!is_eqp(r.get_new(), e)) { - lean_trace_d(name({"simplifier", "rewrite"}), tout() << "[" << lemma.get_id() << "]: " << e << " ==> " << r.get_new() << "\n";); + lean_trace_d(name({"simplifier", "rewrite"}), tout() << "[" << lemma.get_id() << "]: " << e << + " ==> " << r.get_new() << "\n";); return r; } } @@ -810,7 +1109,8 @@ class simplifier { return simp_result(e); } if (!instantiate_emetas(tmp_tctx, sl.get_num_emeta(), sl.get_emetas(), sl.get_instances())) { - lean_trace_d(name({"debug", "simplifier", "try_rewrite"}), tout() << "fail to instantiate emetas: " << sl.get_id() << "\n";); + lean_trace_d(name({"debug", "simplifier", "try_rewrite"}), tout() << "fail to instantiate emetas: " << + sl.get_id() << "\n";); return simp_result(e); } @@ -913,7 +1213,8 @@ class simplifier { if (m_rewrite) { simp_result r_rewrite = simplify_rewrite_binary(r.get_new()); if (r_rewrite.get_new() != r.get_new()) { - lean_trace_d(name({"simplifier", "rewrite"}), tout() << r.get_new() << " ==> " << r_rewrite.get_new() << "\n";); + lean_trace_d(name({"simplifier", "rewrite"}), tout() << r.get_new() << " ==> " << + r_rewrite.get_new() << "\n";); return join(r, r_rewrite); } } @@ -1486,6 +1787,9 @@ expr simplifier::remove_unnecessary_casts(expr const & e) { return mk_app(f, args); } +simp_result simplify(type_context & tctx, name const & rel, simp_lemmas const & simp_lemmas, + vm_obj const & prove_fn, expr const & e); + vm_obj simp_lemmas_simplify_core(vm_obj const & lemmas, vm_obj const & prove_fn, vm_obj const & rel_name, vm_obj const & e, vm_obj const & s0) { tactic_state const & s = to_tactic_state(s0); try { diff --git a/src/library/tactic/simplify.h b/src/library/tactic/simplify.h index ef9e2151d0..5121453811 100644 --- a/src/library/tactic/simplify.h +++ b/src/library/tactic/simplify.h @@ -54,7 +54,8 @@ protected: void inc_num_steps(); bool is_dependent_fn(expr const & f); bool should_defeq_canonize() const { return m_canonize_instances || m_canonize_proofs; } - bool instantiate_emetas(tmp_type_context & tmp_tctx, unsigned num_emeta, list const & emetas, list const & instances); + bool instantiate_emetas(tmp_type_context & tmp_tctx, unsigned num_emeta, + 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); @@ -72,6 +73,12 @@ protected: 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); + /* Visitors */ virtual optional> pre(expr const & e, optional const & parent); virtual optional> post(expr const & e, optional const & parent); @@ -94,24 +101,38 @@ public: environment const & env() const; simp_result operator()(name const & rel, expr const & e); + + optional prove_by_simp(name const & rel, expr const & e); }; -simp_result simplify(type_context & tctx, name const & rel, simp_lemmas const & simp_lemmas, vm_obj const & prove_fn, expr const & e); -simp_result simplify(type_context & tctx, name const & rel, simp_lemmas const & simp_lemmas, 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: + bool m_use_axioms; + 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; +public: + simplify_ext_core_fn(type_context & ctx, simp_lemmas const & slss, + unsigned max_steps, bool contextual, bool lift_eq, + bool canonize_instances, bool canonize_proofs, bool use_axioms); +}; -simp_result simplify(type_context & tctx, type_context & tctx_whnf, name const & rel, simp_lemmas const & simp_lemmas, vm_obj const & prove_fn, expr const & e); -simp_result simplify(type_context & tctx, type_context & tctx_whnf, name const & rel, simp_lemmas const & simp_lemmas, expr const & e); - -optional prove_eq_by_simp(type_context & tctx, type_context & tctx_whnf, simp_lemmas const & simp_lemmas, expr const & e); - -name get_simplify_prefix_name(); -name get_simplify_max_steps_name(); -name get_simplify_contextual_name(); -name get_simplify_rewrite_name(); -name get_simplify_lift_eq_name(); -name get_simplify_canonize_instances_fixed_point_name(); -name get_simplify_canonize_proofs_fixed_point_name(); -name get_simplify_canonize_subsingletons_name(); +/* Default (bottom-up) simplifier: reduce projections, and apply simplification lemmas */ +class simplify_fn : public simplify_ext_core_fn { +protected: + virtual optional> pre(expr const & e, optional const & parent) override; + virtual optional> post(expr const & e, optional const & parent) override; +public: + simplify_fn(type_context & ctx, simp_lemmas const & slss, + unsigned max_steps, bool contextual, bool lift_eq, + bool canonize_instances, bool canonize_proofs, bool use_axioms): + simplify_ext_core_fn(ctx, slss, max_steps, contextual, lift_eq, + canonize_instances, canonize_proofs, use_axioms) {} +}; void initialize_simplify(); void finalize_simplify(); diff --git a/src/library/vm/vm_expr.cpp b/src/library/vm/vm_expr.cpp index 2008ed5ec6..4fc92c1b91 100644 --- a/src/library/vm/vm_expr.cpp +++ b/src/library/vm/vm_expr.cpp @@ -60,6 +60,10 @@ vm_obj to_obj(expr const & e) { return mk_vm_external(new (get_vm_allocator().allocate(sizeof(vm_expr))) vm_expr(e)); } +vm_obj to_obj(optional const & e) { + return e ? mk_vm_some(to_obj(*e)) : mk_vm_none(); +} + binder_info to_binder_info(vm_obj const & o) { lean_assert(is_simple(o)); /* diff --git a/src/library/vm/vm_expr.h b/src/library/vm/vm_expr.h index aa1e1fa5b3..aa69f744d0 100644 --- a/src/library/vm/vm_expr.h +++ b/src/library/vm/vm_expr.h @@ -15,6 +15,7 @@ macro_definition const & to_macro_definition(vm_obj const & o); vm_obj to_obj(macro_definition const & d); expr const & to_expr(vm_obj const & o); vm_obj to_obj(expr const & e); +vm_obj to_obj(optional const & e); void initialize_vm_expr(); void finalize_vm_expr(); void initialize_vm_expr_builtin_idxs();