diff --git a/library/init/congr.lean b/library/init/congr.lean index 4c67ea1ae2..116b24ac5b 100644 --- a/library/init/congr.lean +++ b/library/init/congr.lean @@ -14,3 +14,6 @@ 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) + +lemma imp_congr_ctx_eq {a b c d : Prop} (h₁ : a = c) (h₂ : c → (b = d)) : (a → b) = (c → d) := +propext (imp_congr_ctx h₁^.to_iff (λ hc, (h₂ hc)^.to_iff)) diff --git a/library/init/default.lean b/library/init/default.lean index f25ed51935..470c0b0889 100644 --- a/library/init/default.lean +++ b/library/init/default.lean @@ -7,9 +7,9 @@ prelude import init.core init.logic import init.relation init.nat init.prod init.sum init.combinator import init.bool init.unit init.num init.sigma init.setoid init.quot -import init.funext init.function init.subtype init.classical +import init.funext init.function init.subtype init.classical init.congr import init.monad init.option init.state init.fin init.list init.char init.string init.to_string import init.monad_combinators init.set import init.timeit init.trace init.unsigned init.ordering init.list_classes init.coe import init.wf init.nat_div init.meta init.instances -import init.sigma_lex init.simplifier init.id_locked init.order init.algebra +import init.sigma_lex init.id_locked init.order init.algebra diff --git a/library/init/meta/interactive.lean b/library/init/meta/interactive.lean index d1c569ce87..2f18c79e52 100644 --- a/library/init/meta/interactive.lean +++ b/library/init/meta/interactive.lean @@ -268,33 +268,39 @@ do es ← to_expr_list hs, s₁ ← s₀^.append es, return $ simp_lemmas.erase s₁ ex -private meta def simp_goal : simp_lemmas → tactic unit +private meta def simp_goal (cfg : simplify_config) : simp_lemmas → tactic unit | s := do - (new_target, Heq) ← target >>= s^.simplify_core (simp_goal s) `eq, + (new_target, Heq) ← target >>= simplify_core cfg s `eq, tactic.assert `Htarget new_target, swap, Ht ← get_local `Htarget, mk_app `eq.mpr [Heq, Ht] >>= tactic.exact -private meta def simp_hyp (s : simp_lemmas) (h_name : name) : tactic unit := +private meta def simp_hyp (cfg : simplify_config) (s : simp_lemmas) (h_name : name) : tactic unit := do h ← get_local h_name, htype ← infer_type h, - (new_htype, eqpr) ← s^.simplify_core (simp_goal s) `eq htype, + (new_htype, eqpr) ← simplify_core cfg s `eq htype, tactic.assert (expr.local_pp_name h) new_htype, mk_app `eq.mp [eqpr, h] >>= tactic.exact, try $ tactic.clear h -private meta def simp_hyps : simp_lemmas → location → tactic unit +private meta def simp_hyps (cfg : simplify_config) : simp_lemmas → location → tactic unit | s [] := skip -| s (h::hs) := simp_hyp s h >> simp_hyps s hs +| s (h::hs) := simp_hyp cfg s h >> simp_hyps s hs -meta def simp (hs : opt_qexpr_list) (attr_names : with_ident_list) (ids : without_ident_list) (loc : location) : tactic unit := +private meta def simp_core (cfg : simplify_config) (hs : opt_qexpr_list) (attr_names : with_ident_list) (ids : without_ident_list) (loc : location) : tactic unit := do s ← mk_simp_set attr_names hs ids, match loc : _ → tactic unit with - | [] := simp_goal s - | _ := simp_hyps s loc + | [] := simp_goal cfg s + | _ := simp_hyps cfg s loc end, try tactic.triv, try tactic.reflexivity +meta def simp (hs : opt_qexpr_list) (attr_names : with_ident_list) (ids : without_ident_list) (loc : location) : tactic unit := +simp_core default_simplify_config hs attr_names ids loc + +meta def ctx_simp (hs : opt_qexpr_list) (attr_names : with_ident_list) (ids : without_ident_list) (loc : location) : tactic unit := +simp_core {default_simplify_config with contextual := tt} hs attr_names ids loc + private meta def dsimp_hyps : location → tactic unit | [] := skip | (h::hs) := get_local h >>= dsimp_at diff --git a/library/init/meta/simp_tactic.lean b/library/init/meta/simp_tactic.lean index 0f7c287b0b..f29b1eb99d 100644 --- a/library/init/meta/simp_tactic.lean +++ b/library/init/meta/simp_tactic.lean @@ -54,16 +54,6 @@ meta constant simp_lemmas.drewrite_core : transparency → simp_lemmas → expr meta def simp_lemmas.drewrite : simp_lemmas → expr → tactic expr := simp_lemmas.drewrite_core reducible -/- Simplify the given expression using [simp] and [congr] lemmas. - The first argument is a tactic to be used to discharge proof obligations. - The second argument is the name of the relation to simplify over. - The third argument is a list of additional expressions to be considered as simp rules. - The fourth argument is the expression to be simplified. - The result is the simplified expression along with a proof that the new - expression is equivalent to the old one. - Fails if no simplifications can be performed. -/ -meta constant simp_lemmas.simplify_core : simp_lemmas → tactic unit → name → expr → tactic (expr × expr) - /- (Definitional) Simplify the given expression using *only* reflexivity equality lemmas from the given set of lemmas. The resulting expression is definitionally equal to the input. -/ meta constant simp_lemmas.dsimplify_core (max_steps : nat) (visit_instances : bool) : simp_lemmas → expr → tactic expr @@ -204,23 +194,26 @@ meta constant ext_simplify_core (r : name) : expr → tactic (A × expr × expr) -meta def simplify (prove_fn : tactic unit) (extra_lemmas : list expr) (e : expr) : tactic (expr × expr) := +meta def simplify (cfg : simplify_config) (extra_lemmas : list expr) (e : expr) : tactic (expr × expr) := do lemmas ← simp_lemmas.mk_default, new_lemmas ← lemmas^.append extra_lemmas, e_type ← infer_type e >>= whnf, - new_lemmas^.simplify_core prove_fn `eq e + simplify_core cfg new_lemmas `eq e -meta def simplify_goal (prove_fn : tactic unit) (extra_lemmas : list expr) : tactic unit := -do (new_target, Heq) ← target >>= simplify prove_fn extra_lemmas, +meta def simplify_goal (cfg : simplify_config) (extra_lemmas : list expr) : tactic unit := +do (new_target, Heq) ← target >>= simplify cfg extra_lemmas, assert `Htarget new_target, swap, Ht ← get_local `Htarget, mk_app `eq.mpr [Heq, Ht] >>= exact meta def simp : tactic unit := -simplify_goal failed [] >> try triv >> try reflexivity +simplify_goal default_simplify_config [] >> try triv >> try reflexivity meta def simp_using (Hs : list expr) : tactic unit := -simplify_goal failed Hs >> try triv +simplify_goal default_simplify_config Hs >> try triv + +meta def ctx_simp : tactic unit := +simplify_goal {default_simplify_config with contextual := tt} [] >> try triv >> try reflexivity meta def dsimp : tactic unit := do S ← simp_lemmas.mk_default, @@ -249,23 +242,23 @@ private meta def collect_eqs : list expr → tactic (list expr) meta def simp_using_hs : tactic unit := local_context >>= collect_eqs >>= simp_using -meta def simp_core_at (prove_fn : tactic unit) (extra_lemmas : list expr) (H : expr) : tactic unit := +meta def simp_core_at (extra_lemmas : list expr) (H : expr) : tactic unit := do when (expr.is_local_constant H = ff) (fail "tactic simp_at failed, the given expression is not a hypothesis"), Htype ← infer_type H, - (new_Htype, Heq) ← simplify prove_fn extra_lemmas Htype, + (new_Htype, Heq) ← simplify default_simplify_config extra_lemmas Htype, assert (expr.local_pp_name H) new_Htype, mk_app `eq.mp [Heq, H] >>= exact, try $ clear H meta def simp_at : expr → tactic unit := -simp_core_at failed [] +simp_core_at [] meta def simp_at_using (Hs : list expr) : expr → tactic unit := -simp_core_at failed Hs +simp_core_at Hs meta def simp_at_using_hs (H : expr) : tactic unit := do Hs ← local_context >>= collect_eqs, - simp_core_at failed (list.filter (ne H) Hs) H + simp_core_at (list.filter (ne H) Hs) H meta def mk_eq_simp_ext (simp_ext : expr → tactic (expr × expr)) : tactic unit := do (lhs, rhs) ← target >>= match_eq, diff --git a/library/init/simplifier.lean b/library/init/simplifier.lean deleted file mode 100644 index e7e43b9936..0000000000 --- a/library/init/simplifier.lean +++ /dev/null @@ -1,41 +0,0 @@ -prelude -import init.logic init.classical - -universe variables u - --- For n-ary support -class is_associative {A : Type u} (op : A → A → A) := -(op_assoc : ∀ x y z : A, op (op x y) z = op x (op y z)) - -instance : is_associative and := -is_associative.mk (λ x y z, propext (@and.assoc x y z)) - -instance : is_associative or := -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 H₁^.to_iff (assume p₂, (H₂ p₂)^.to_iff)) - --- Congruence theorems for flattening -namespace simplifier -variables {A : Type u} - -theorem congr_bin_op {op op' : A → A → A} (H : op = op') (x y : A) : op x y = op' x y := -congr_fun (congr_fun H x) y - -theorem congr_bin_arg1 {op : A → A → A} {x x' y : A} (Hx : x = x') : op x y = op x' y := -congr_fun (congr_arg op Hx) y - -theorem congr_bin_arg2 {op : A → A → A} {x y y' : A} (Hy : y = y') : op x y = op x y' := -congr_arg (op x) Hy - -theorem congr_bin_args {op : A → A → A} {x x' y y' : A} (Hx : x = x') (Hy : y = y') : op x y = op x' y' := -congr (congr_arg op Hx) Hy - -theorem assoc_subst {op op' : A → A → A} (H : op = op') (H_assoc : ∀ x y z, op (op x y) z = op x (op y z)) - : (∀ x y z, op' (op' x y) z = op' x (op' y z)) := -H ▸ H_assoc - -end simplifier diff --git a/src/library/constants.cpp b/src/library/constants.cpp index b8d405a72a..af26b72ccb 100644 --- a/src/library/constants.cpp +++ b/src/library/constants.cpp @@ -120,6 +120,8 @@ 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_imp_congr_ctx = nullptr; +name const * g_imp_congr_ctx_eq = nullptr; name const * g_implies = nullptr; name const * g_implies_of_if_neg = nullptr; name const * g_implies_of_if_pos = nullptr; @@ -506,6 +508,8 @@ void initialize_constants() { 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_imp_congr_ctx = new name{"imp_congr_ctx"}; + g_imp_congr_ctx_eq = new name{"imp_congr_ctx_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"}; @@ -893,6 +897,8 @@ void finalize_constants() { delete g_iff_true_intro; delete g_imp_congr; delete g_imp_congr_eq; + delete g_imp_congr_ctx; + delete g_imp_congr_ctx_eq; delete g_implies; delete g_implies_of_if_neg; delete g_implies_of_if_pos; @@ -1279,6 +1285,8 @@ 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_imp_congr_ctx_name() { return *g_imp_congr_ctx; } +name const & get_imp_congr_ctx_eq_name() { return *g_imp_congr_ctx_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 082d79933b..36450f43c5 100644 --- a/src/library/constants.h +++ b/src/library/constants.h @@ -122,6 +122,8 @@ 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_imp_congr_ctx_name(); +name const & get_imp_congr_ctx_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 c84fbddd42..6fc1b43c61 100644 --- a/src/library/constants.txt +++ b/src/library/constants.txt @@ -115,6 +115,8 @@ iff.trans iff_true_intro imp_congr imp_congr_eq +imp_congr_ctx +imp_congr_ctx_eq implies implies_of_if_neg implies_of_if_pos diff --git a/src/library/tactic/simplify.cpp b/src/library/tactic/simplify.cpp index 3139b714b1..d26606d5ac 100644 --- a/src/library/tactic/simplify.cpp +++ b/src/library/tactic/simplify.cpp @@ -32,6 +32,7 @@ Author: Daniel Selsam, Leonardo de Moura #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/tactic_state.h" #include "library/tactic/ac_tactics.h" @@ -814,8 +815,40 @@ simp_result simplify_ext_core_fn::forall_congr(expr const & e) { } simp_result simplify_ext_core_fn::imp_congr(expr const & e) { - // TODO(Leo) - return simp_result(e); + expr const & a = binding_domain(e); + expr const & b = binding_body(e); + simp_result r_a = visit(a, some_expr(e)); + if (m_contextual) { + type_context::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(mk_arrow(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(mk_arrow(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(mk_arrow(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(mk_arrow(r_a.get_new(), r_b.get_new()), pr); + } + } } simp_result simplify_ext_core_fn::visit_pi(expr const & e) { @@ -920,981 +953,115 @@ public: 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; } - -/* Options */ - -static name * g_simplify_max_steps = nullptr; -static name * g_simplify_contextual = nullptr; -static name * g_simplify_rewrite = nullptr; -static name * g_simplify_lift_eq = nullptr; -static name * g_simplify_canonize_instances_fixed_point = nullptr; -static name * g_simplify_canonize_proofs_fixed_point = nullptr; - -name get_simplify_max_steps_name() { return *g_simplify_max_steps; } -name get_simplify_contextual_name() { return *g_simplify_contextual; } -name get_simplify_rewrite_name() { return *g_simplify_rewrite; } -name get_simplify_lift_eq_name() { return *g_simplify_lift_eq; } -name get_simplify_canonize_instances_fixed_point_name() { return *g_simplify_canonize_instances_fixed_point; } -name get_simplify_canonize_proofs_fixed_point_name() { return *g_simplify_canonize_proofs_fixed_point; } - -static unsigned get_simplify_max_steps(options const & o) { - return o.get_unsigned(*g_simplify_max_steps, LEAN_DEFAULT_SIMPLIFY_MAX_STEPS); -} - -static bool get_simplify_contextual(options const & o) { - return o.get_bool(*g_simplify_contextual, LEAN_DEFAULT_SIMPLIFY_CONTEXTUAL); -} - -static bool get_simplify_rewrite(options const & o) { - return o.get_bool(*g_simplify_rewrite, LEAN_DEFAULT_SIMPLIFY_REWRITE); -} - -static bool get_simplify_lift_eq(options const & o) { - return o.get_bool(*g_simplify_lift_eq, LEAN_DEFAULT_SIMPLIFY_LIFT_EQ); -} - -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); -} - -static bool get_simplify_canonize_proofs_fixed_point(options const & o) { - return o.get_bool(*g_simplify_canonize_proofs_fixed_point, LEAN_DEFAULT_SIMPLIFY_DEFEQ_CANONIZE_PROOFS_FIXED_POINT); -} - -/* Main simplifier class */ - -class simplifier { - type_context m_tctx, m_tctx_whnf; - - name m_rel; - - simp_lemmas m_slss; - - optional m_prove_fn; - - /* Logging */ - unsigned m_num_steps{0}; - - bool m_need_restart{false}; - - /* Options */ - unsigned m_max_steps; - bool m_contextual; - bool m_rewrite; - bool m_lift_eq; - bool m_canonize_instances_fixed_point; - bool m_canonize_proofs_fixed_point; - - typedef expr_struct_map simplify_cache; - simplify_cache m_cache; - optional cache_lookup(expr const & e); - void cache_save(expr const & e, simp_result const & r); - - /* Basic helpers */ - environment const & env() const { return m_tctx.env(); } - - simp_result join(simp_result const & r1, simp_result const & r2) { return ::lean::join(m_tctx, m_rel, r1, r2); } - - bool using_eq() { return m_rel == get_eq_name(); } - - bool is_dependent_fn(expr const & f) { - expr f_type = m_tctx.whnf(m_tctx.infer(f)); - lean_assert(is_pi(f_type)); - return has_free_vars(binding_body(f_type)); - } - - simp_lemmas 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 { - // TODO(Leo,Daniel): should we allow the user to set the priority of local lemmas? - slss = add(m_tctx, slss, mlocal_name(l), m_tctx.infer(l), l, LEAN_DEFAULT_PRIORITY); - lean_trace_d(name({"simplifier", "context"}), tout() << mlocal_name(l) << " : " << m_tctx.infer(l) << "\n";); - } catch (exception e) { - } - } - return slss; - } - - bool should_defeq_canonize() { - 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); - - /* Simp_Results */ - simp_result lift_from_eq(expr const & old_e, simp_result const & r_eq); - - /* Main simplify method */ - simp_result simplify(expr const & old_e) { - m_num_steps++; - lean_trace_inc_depth("simplifier"); - lean_trace_d("simplifier", tout() << m_rel << ": " << old_e << "\n";); - - if (m_num_steps > m_max_steps) { - lean_trace(name({"simplifier", "failed"}), tout() << m_rel << ": " << old_e << "\n";); - throw exception("simplifier failed, maximum number of steps exceeded"); - } - - if (auto it = cache_lookup(old_e)) - return *it; - - expr e = whnf_eta(old_e); - simp_result r; - - r = simplify_binary(e); - - if (!r.is_done()) - r = join(r, simplify(r.get_new())); - - if (m_lift_eq && !using_eq()) { - simp_result r_eq; - { - flet use_eq(m_rel, get_eq_name()); - r_eq = simplify(r.get_new()); - } - if (r_eq.get_new() != r.get_new()) { - r = join(r, lift_from_eq(r.get_new(), r_eq)); - r = join(r, simplify(r.get_new())); - } - } - - cache_save(old_e, r); - - return r; - } - - simp_result simplify_rewrite_binary(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", "simplifier", "try_rewrite"}), tout() << "no simp lemmas for: " << e << "\n";); - return simp_result(e); - } - - 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";); - return r; - } - } - return simp_result(e); - } - - simp_result rewrite_binary(expr const & e, simp_lemma const & sl) { - tmp_type_context tmp_tctx(m_tctx, sl.get_num_umeta(), sl.get_num_emeta()); - if (!tmp_tctx.is_def_eq(e, sl.get_lhs())) { - lean_trace_d(name({"debug", "simplifier", "try_rewrite"}), tout() << "fail to unify: " << sl.get_id() << "\n";); - 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";); - return simp_result(e); - } - - for (unsigned i = 0; i < sl.get_num_umeta(); i++) { - if (!tmp_tctx.is_uassigned(i)) - return simp_result(e); - } - - expr new_lhs = tmp_tctx.instantiate_mvars(sl.get_lhs()); - expr new_rhs = tmp_tctx.instantiate_mvars(sl.get_rhs()); - if (sl.is_permutation()) { - if (!is_lt(new_rhs, new_lhs, false)) { - lean_simp_trace(tmp_tctx, name({"simplifier", "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_tctx.instantiate_mvars(sl.get_proof()); - return simp_result(new_rhs, pf); - } - } - - simp_result simplify_subterms_app_binary(expr const & _e) { - lean_assert(is_app(_e)); - expr e = should_defeq_canonize() ? defeq_canonize_args_step(_e) : _e; - - // (1) Try user-defined congruences - simp_result r_user = try_congrs(e); - if (r_user.has_proof()) { - if (using_eq()) { - return join(r_user, simplify_operator_of_app(r_user.get_new())); - } else { - return r_user; - } - } - - // (2) Synthesize congruence lemma - if (using_eq()) { - optional r_args = synth_congr(e); - if (r_args) return join(*r_args, simplify_operator_of_app(r_args->get_new())); - } - // (3) Fall back on generic binary congruence - if (using_eq()) { - expr const & f = app_fn(e); - expr const & arg = app_arg(e); - - simp_result r_f = simplify(f); - - if (is_dependent_fn(f)) { - if (r_f.has_proof()) return congr_fun(r_f, arg); - else return mk_app(r_f.get_new(), arg); - } else { - simp_result r_arg = simplify(arg); - return congr_fun_arg(r_f, r_arg); - } - } - return simp_result(e); - } - - - // Main binary simplify method - simp_result simplify_binary(expr const & e) { - // [1] Simplify subterms using congruence - simp_result r(e); - - switch (r.get_new().kind()) { - case expr_kind::Local: - case expr_kind::Meta: - case expr_kind::Sort: - case expr_kind::Constant: - case expr_kind::Macro: - // no-op - break; - case expr_kind::Lambda: - if (using_eq()) - r = simplify_subterms_lambda(r.get_new()); - break; - case expr_kind::Pi: - r = simplify_subterms_pi(r.get_new()); - break; - case expr_kind::App: - r = simplify_subterms_app_binary(r.get_new()); - break; - case expr_kind::Let: - // whnf unfolds let-expressions - // TODO(dhs, leo): add flag for type_context not to unfold let-expressions - lean_unreachable(); - case expr_kind::Var: - lean_unreachable(); - } - - if (r.get_new() != e) { - lean_trace_d(name({"simplifier", "congruence"}), tout() << e << " ==> " << r.get_new() << "\n";); - } - - 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";); - return join(r, r_rewrite); - } - } - - r.set_done(); - return r; - } - - /* Simplifying the necessary subterms */ - simp_result simplify_subterms_lambda(expr const & e); - simp_result simplify_subterms_pi(expr const & e); - simp_result simplify_subterms_app(expr const & e); - - /* Called from simplify_subterms_app */ - simp_result simplify_operator_of_app(expr const & e); - - /* Proving */ - optional prove(expr const & thm); - - /* Canonize */ - expr defeq_canonize_args_step(expr const & e); - - /* Congruence */ - 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); - simp_result funext(simp_result const & r, expr const & l); - - simp_result try_congrs(expr const & e); - simp_result try_congr(expr const & e, simp_lemma const & cr); - - optional synth_congr(expr const & e); - - expr remove_unnecessary_casts(expr const & e); - - /* Apply whnf and eta-reduction - \remark We want (Sum n (fun x, f x)) and (Sum n f) to be the same. - \remark We may want to switch to eta-expansion later (see paper: "The Virtues of Eta-expansion"). - TODO(Daniel, Leo): should we add an option for disabling/enabling eta? */ - expr whnf_eta(expr const & e); - -public: - simplifier(type_context & tctx, type_context & tctx_whnf, name const & rel, simp_lemmas const & slss, optional const & prove_fn): - m_tctx(tctx), m_tctx_whnf(tctx_whnf), m_rel(rel), m_slss(slss), m_prove_fn(prove_fn), - /* Options */ - m_max_steps(get_simplify_max_steps(tctx.get_options())), - m_contextual(get_simplify_contextual(tctx.get_options())), - m_rewrite(get_simplify_rewrite(tctx.get_options())), - m_lift_eq(get_simplify_lift_eq(tctx.get_options())), - m_canonize_instances_fixed_point(get_simplify_canonize_instances_fixed_point(tctx.get_options())), - m_canonize_proofs_fixed_point(get_simplify_canonize_proofs_fixed_point(tctx.get_options())) - {} - - simp_result operator()(expr const & e) { - scope_trace_env scope(env(), m_tctx.get_options(), m_tctx); - simp_result r(e); - while (true) { - m_need_restart = false; - r = join(r, simplify(r.get_new())); - if (!m_need_restart || !should_defeq_canonize()) - return r; - m_cache.clear(); - } - return simplify(e); + 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); } }; -/* Cache */ - -optional simplifier::cache_lookup(expr const & e) { - auto it = m_cache.find(e); - if (it == m_cache.end()) return optional(); - return optional(it->second); +/* +structure simplify_config := +(max_steps : nat) +(contextual : bool) +(lift_eq : bool) +(canonize_instances : bool) +(canonize_proofs : bool) +(use_axioms : bool) +*/ +void get_simplify_config(vm_obj const & obj, unsigned & max_steps, bool & contextual, bool & lift_eq, + bool & canonize_instances, bool & canonize_proofs, bool & use_axioms) { + max_steps = force_to_unsigned(cfield(obj, 0), std::numeric_limits::max()); + contextual = to_bool(cfield(obj, 1)); + lift_eq = to_bool(cfield(obj, 2)); + canonize_instances = to_bool(cfield(obj, 3)); + canonize_proofs = to_bool(cfield(obj, 4)); + use_axioms = to_bool(cfield(obj, 5)); } -void simplifier::cache_save(expr const & e, simp_result const & r) { - m_cache.insert(mk_pair(e, r)); -} - -/* Simp_Results */ - -simp_result simplifier::lift_from_eq(expr const & old_e, simp_result const & r_eq) { - if (!r_eq.has_proof()) return r_eq; - lean_assert(r_eq.has_proof()); - /* r_eq.get_proof() : old_e = r_eq.get_new() */ - /* goal : old_e r_eq.get_new() */ - type_context::tmp_locals local_factory(m_tctx); - expr local = local_factory.push_local(name(), m_tctx.infer(old_e)); - expr motive_local = mk_app(m_tctx, m_rel, old_e, local); - /* motive = fun y, old_e y */ - expr motive = local_factory.mk_lambda(motive_local); - /* Rxx = x x */ - expr Rxx = mk_refl(m_tctx, m_rel, old_e); - expr pf = mk_eq_rec(m_tctx, motive, Rxx, r_eq.get_proof()); - return simp_result(r_eq.get_new(), pf); -} - -/* Whnf + Eta */ -expr simplifier::whnf_eta(expr const & e) { - return try_eta(m_tctx_whnf.whnf(e)); -} - -simp_result simplifier::simplify_subterms_lambda(expr const & old_e) { - lean_assert(is_lambda(old_e)); - expr e = old_e; - - buffer ls; - while (is_lambda(e)) { - expr d = instantiate_rev(binding_domain(e), ls.size(), ls.data()); - expr l = m_tctx.push_local(binding_name(e), d, binding_info(e)); - ls.push_back(l); - e = instantiate(binding_body(e), l); - } - - simp_result r = simplify(e); - expr new_e = r.get_new(); - - if (r.get_new() == e) - return old_e; - - if (!r.has_proof()) - return m_tctx.mk_lambda(ls, r.get_new()); - - for (int i = ls.size() - 1; i >= 0; --i) - r = funext(r, ls[i]); - - return r; -} - -simp_result simplifier::simplify_subterms_pi(expr const & e) { - lean_assert(is_pi(e)); - return try_congrs(e); -} - -expr simplifier::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_tctx, 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_canonize_instances_fixed_point && pinfo.is_inst_implicit()) || (m_canonize_proofs_fixed_point && pinfo.is_prop())) { - new_a = ::lean::defeq_canonize(m_tctx, args[i], m_need_restart); - lean_trace(name({"simplifier", "canonize"}), - tout() << "\n" << args[i] << "\n==>\n" << new_a << "\n";); - if (new_a != args[i]) { - modified = true; - args[i] = new_a; - } - } - i++; - } - - if (!modified) - return e; - else - return mk_app(f, args); -} - -simp_result simplifier::simplify_operator_of_app(expr const & e) { - lean_assert(is_app(e)); - buffer args; - expr const & f = get_app_args(e, args); - simp_result r_f = simplify(f); - return congr_funs(r_f, args); -} - -/* Proving */ -optional simplifier::prove(expr const & goal) { - if (!m_prove_fn) - return none_expr(); - - metavar_context mctx = m_tctx.mctx(); - expr goal_mvar = mctx.mk_metavar_decl(m_tctx.lctx(), goal); - lean_trace(name({"simplifier", "prove"}), tout() << "goal: " << goal_mvar << " : " << goal << "\n";); - vm_obj s = to_obj(tactic_state(m_tctx.env(), m_tctx.get_options(), mctx, list(goal_mvar), goal_mvar)); - vm_obj prove_fn_result = invoke(*m_prove_fn, s); - optional s_new = is_tactic_success(prove_fn_result); - if (s_new) { - if (!s_new->mctx().is_assigned(goal_mvar)) { - lean_trace(name({"simplifier", "prove"}), tout() << "prove_fn succeeded but did not return a proof\n";); - return none_expr(); - } - metavar_context smctx = s_new->mctx(); - expr proof = smctx.instantiate_mvars(goal_mvar); - optional new_metavar = find(proof, [&](expr const & e, unsigned) { - return is_metavar(e) && !static_cast(m_tctx.mctx().get_metavar_decl(e)); - }); - if (new_metavar) { - lean_trace(name({"simplifier", "prove"}), - tout() << "prove_fn succeeded but left an unrecognized metavariable of type " - << smctx.get_metavar_decl(*new_metavar)->get_type() << " in proof\n";); - return none_expr(); - } - m_tctx.set_mctx(s_new->mctx()); - lean_trace(name({"simplifier", "prove"}), tout() << "success: " << proof << " : " << m_tctx.infer(proof) << "\n";); - return some_expr(proof); - } else { - lean_trace(name({"simplifier", "prove"}), tout() << "prove_fn failed to prove " << goal << "\n";); - return none_expr(); - } -} - -/* Congruence */ - -simp_result simplifier::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 simplifier::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_tctx, r_f.get_proof(), r_arg.get_proof()); - return simp_result(e, pf); -} - -simp_result simplifier::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_tctx, r_f.get_proof(), arg); - return simp_result(e, pf); -} - -simp_result simplifier::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_tctx, f, r_arg.get_proof()); - return simp_result(e, pf); -} - -/* Note: handles reflexivity */ -simp_result simplifier::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_tctx, pf, args[i]); - } - return simp_result(e, pf); -} - -simp_result simplifier::funext(simp_result const & r, expr const & l) { - expr e = m_tctx.mk_lambda(l, r.get_new()); - if (!r.has_proof()) - return simp_result(e); - expr lam_pf = m_tctx.mk_lambda(l, r.get_proof()); - expr pf = mk_funext(m_tctx, lam_pf); - return simp_result(e, pf); -} - -simp_result simplifier::try_congrs(expr const & e) { - simp_lemmas_for const * sls = m_slss.find(m_rel); - if (!sls) return simp_result(e); - - list const * cls = sls->find_congr(e); - if (!cls) return simp_result(e); - - for (simp_lemma const & cl : *cls) { - simp_result r = try_congr(e, cl); - if (r.get_new() != e) - return r; - } - return simp_result(e); -} - -simp_result simplifier::try_congr(expr const & e, simp_lemma const & cl) { - tmp_type_context tmp_tctx(m_tctx, cl.get_num_umeta(), cl.get_num_emeta()); - if (!tmp_tctx.is_def_eq(e, cl.get_lhs())) - return simp_result(e); - - lean_simp_trace(tmp_tctx, name({"debug", "simplifier", "try_congruence"}), - tout() << "(" << cl.get_id() << ") " << e << "\n";); - - bool simplified = false; - - buffer congr_hyps; - to_buffer(cl.get_congr_hyps(), congr_hyps); - - buffer congr_hyp_results; - buffer factories; - buffer relations; - for (expr const & m : congr_hyps) { - factories.emplace_back(m_tctx); - type_context::tmp_locals & local_factory = factories.back(); - expr m_type = tmp_tctx.instantiate_mvars(tmp_tctx.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_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_tctx.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_contextual ? add_to_slss(m_slss, local_factory.as_buffer()) : m_slss); - - h_lhs = tmp_tctx.instantiate_mvars(h_lhs); - /* TODO(Leo, Daniel): the original assertion was !has_metavar(h_lhs). - It is incorrect. I got an assertion violation when processing - a term containing universe meta-variables. So, I relaxed it to !has_expr_metavar(h_lhs). - We should investigate this. Example: what happens if the input expression has - regular meta-variables? Perhaps, the right assertion is: h_lhs does *not* have temporary - universe and regular meta-variables. */ - lean_assert(!has_expr_metavar(h_lhs)); - - if (m_contextual || m_rel != const_name(h_rel)) { - flet set_name(m_rel, const_name(h_rel)); - freset reset_cache(m_cache); - congr_hyp_results.emplace_back(simplify(h_lhs)); - } else { - congr_hyp_results.emplace_back(simplify(h_lhs)); - } - simp_result const & r_congr_hyp = congr_hyp_results.back(); - - if (r_congr_hyp.has_proof()) - simplified = true; - - lean_assert(is_meta(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_tctx.mk_lambda(new_val_meta_args, r_congr_hyp.get_new()); - tmp_tctx.assign(new_val_meta, new_val); - } - } - - if (!simplified) - return simp_result(e); - - lean_assert(congr_hyps.size() == congr_hyp_results.size()); - for (unsigned i = 0; i < congr_hyps.size(); ++i) { - expr const & pf_meta = congr_hyps[i]; - simp_result const & r_congr_hyp = congr_hyp_results[i]; - name const & rel = relations[i]; - type_context::tmp_locals & local_factory = factories[i]; - expr hyp = finalize(m_tctx, rel, r_congr_hyp).get_proof(); - // This is the current bottleneck - // Can address somewhat by keeping the proofs as small as possible using macros - expr pf = local_factory.mk_lambda(hyp); - tmp_tctx.assign(pf_meta, pf); - } - - if (!instantiate_emetas(tmp_tctx, cl.get_num_emeta(), cl.get_emetas(), cl.get_instances())) - return simp_result(e); - - for (unsigned i = 0; i < cl.get_num_umeta(); i++) { - if (!tmp_tctx.is_uassigned(i)) - return simp_result(e); - } - - expr e_s = tmp_tctx.instantiate_mvars(cl.get_rhs()); - expr pf = tmp_tctx.instantiate_mvars(cl.get_proof()); - - simp_result r(e_s, pf); - - lean_simp_trace(tmp_tctx, name({"simplifier", "congruence"}), - tout() << "(" << cl.get_id() << ") " - << "[" << e << " ==> " << e_s << "]\n";); - - return r; -} - -bool simplifier::instantiate_emetas(tmp_type_context & tmp_tctx, unsigned num_emeta, list const & emetas, list const & instances) { - bool failed = false; - unsigned i = num_emeta; - for_each2(emetas, instances, [&](expr const & m, bool const & is_instance) { - i--; - if (failed) return; - expr m_type = tmp_tctx.instantiate_mvars(tmp_tctx.infer(m)); - if (has_metavar(m_type)) { - failed = true; - return; - } - - if (tmp_tctx.is_eassigned(i)) return; - - if (is_instance) { - if (auto v = m_tctx.mk_class_instance(m_type)) { - if (!tmp_tctx.is_def_eq(m, *v)) { - lean_simp_trace(tmp_tctx, name({"simplifier", "failure"}), - tout() << "unable to assign instance for: " << m_type << "\n";); - failed = true; - return; - } - } else { - lean_simp_trace(tmp_tctx, name({"simplifier", "failure"}), - tout() << "unable to synthesize instance for: " << m_type << "\n";); - failed = true; - return; - } - } - - if (tmp_tctx.is_eassigned(i)) return; - - // Note: m_type has no metavars - if (m_tctx.is_prop(m_type)) { - if (auto pf = prove(m_type)) { - lean_verify(tmp_tctx.is_def_eq(m, *pf)); - return; - } - } - - lean_simp_trace(tmp_tctx, name({"simplifier", "failure"}), - tout() << "failed to assign: " << m << " : " << m_type << "\n";); - - failed = true; - return; - }); - - return !failed; -} - -optional simplifier::synth_congr(expr const & e) { - lean_assert(is_app(e)); - buffer args; - expr f = get_app_args(e, args); - auto congr_lemma = mk_specialized_congr_simp(m_tctx, e); - if (!congr_lemma) 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(simplify(args[i])); - 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_tctx, 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); -} - -expr simplifier::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_tctx, e); - int i = -1; - bool updated = 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_rec_name() || n_f == get_eq_drec_name() || n_f == get_eq_nrec_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]; - updated = true; - } else { - break; - } - } else { - break; - } - } - } - } - if (!updated) - return e; - - expr new_e = mk_app(f, args); - lean_trace(name({"debug", "simplifier", "remove_casts"}), tout() << e << " ==> " << new_e << "\n";); - - 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); +/* +meta constant simplify_core + (c : simplify_config) + (s : simp_lemmas) + (r : name) : + expr → tactic (expr × expr) +*/ +vm_obj tactic_simplify_core(vm_obj const & c, vm_obj const & slss, vm_obj const & rel, vm_obj const & e, vm_obj const & _s) { + tactic_state const & s = to_tactic_state(_s); try { - type_context tctx = mk_type_context_for(s, transparency_mode::Reducible); - name rel = to_name(rel_name); - expr old_e = to_expr(e); - simp_result result = simplify(tctx, rel, to_simp_lemmas(lemmas), prove_fn, old_e); - - if (result.get_new() != old_e) { - result = finalize(tctx, rel, result); + unsigned max_steps; bool contextual, lift_eq, canonize_instances, canonize_proofs, use_axioms; + get_simplify_config(c, max_steps, contextual, lift_eq, canonize_instances, canonize_proofs, use_axioms); + type_context ctx = mk_type_context_for(s, transparency_mode::Reducible); + simp_result result = simplify_fn(ctx, to_simp_lemmas(slss), max_steps, contextual, lift_eq, + canonize_instances, canonize_proofs, use_axioms)(to_name(rel), to_expr(e)); + if (result.get_new() != to_expr(e)) { + result = finalize(ctx, to_name(rel), result); return mk_tactic_success(mk_vm_pair(to_obj(result.get_new()), to_obj(result.get_proof())), s); } else { - return mk_tactic_exception("simp tactic failed to simplify", s); + return mk_tactic_exception("simplify tactic failed to simplify", s); } } catch (exception & e) { return mk_tactic_exception(e, s); } } -/* Setup and teardown */ +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 const & s) { + try { + unsigned max_steps; bool contextual, lift_eq, canonize_instances, canonize_proofs, use_axioms; + get_simplify_config(c, max_steps, contextual, lift_eq, canonize_instances, canonize_proofs, use_axioms); + type_context ctx = mk_type_context_for(s, transparency_mode::Reducible); + vm_simplify_fn simplifier(ctx, slss, max_steps, contextual, lift_eq, canonize_instances, canonize_proofs, + use_axioms, prove, pre, post); + pair p = simplifier(a, r, e); + if (p.second.get_new() != e) { + vm_obj const & a = p.first; + simp_result result = finalize(ctx, r, p.second); + return mk_tactic_success(mk_vm_pair(a, mk_vm_pair(to_obj(result.get_new()), to_obj(result.get_proof()))), s); + } else { + return mk_tactic_exception("simplify tactic failed to simplify", s); + } + } catch (exception & e) { + return mk_tactic_exception(e, s); + } +} + +/* +meta constant ext_simplify_core + {A : Type} + (a : A) + (c : simplify_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 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]), to_tactic_state(args[9])); +} + void initialize_simplify() { - register_trace_class("simplifier"); - register_trace_class(name({"simplifier", "congruence"})); - register_trace_class(name({"simplifier", "failure"})); - register_trace_class(name({"simplifier", "failed"})); - register_trace_class(name({"simplifier", "perm"})); - register_trace_class(name({"simplifier", "canonize"})); - register_trace_class(name({"simplifier", "context"})); - register_trace_class(name({"simplifier", "prove"})); - register_trace_class(name({"simplifier", "rewrite"})); - register_trace_class(name({"debug", "simplifier", "try_rewrite"})); - register_trace_class(name({"debug", "simplifier", "try_congruence"})); - register_trace_class(name({"debug", "simplifier", "remove_casts"})); + register_trace_class("simplify"); + register_trace_class(name({"simplify", "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_rewrite"})); + register_trace_class(name({"debug", "simplify", "try_congruence"})); - g_simplify_prefix = new name{"simplify"}; - - g_simplify_max_steps = new name{*g_simplify_prefix, "max_steps"}; - g_simplify_contextual = new name{*g_simplify_prefix, "contextual"}; - g_simplify_rewrite = new name{*g_simplify_prefix, "rewrite"}; - g_simplify_lift_eq = new name{*g_simplify_prefix, "lift_eq"}; - g_simplify_canonize_instances_fixed_point = new name{*g_simplify_prefix, "canonize_instances_fixed_point"}; - g_simplify_canonize_proofs_fixed_point = new name{*g_simplify_prefix, "canonize_proofs_fixed_point"}; - - register_unsigned_option(*g_simplify_max_steps, LEAN_DEFAULT_SIMPLIFY_MAX_STEPS, - "(simplify) max number of (large) steps in simplification"); - register_bool_option(*g_simplify_contextual, LEAN_DEFAULT_SIMPLIFY_CONTEXTUAL, - "(simplify) use contextual simplification"); - register_bool_option(*g_simplify_rewrite, LEAN_DEFAULT_SIMPLIFY_REWRITE, - "(simplify) rewrite with simp_lemmas"); - register_bool_option(*g_simplify_lift_eq, LEAN_DEFAULT_SIMPLIFY_LIFT_EQ, - "(simplify) try simplifying with equality when no progress over other relation"); - register_bool_option(*g_simplify_canonize_instances_fixed_point, LEAN_DEFAULT_SIMPLIFY_CANONIZE_INSTANCES_FIXED_POINT, - "(simplify) canonize instances, replacing with the smallest seen so far until reaching a fixed point"); - register_bool_option(*g_simplify_canonize_proofs_fixed_point, LEAN_DEFAULT_SIMPLIFY_CANONIZE_PROOFS_FIXED_POINT, - "(simplify) canonize proofs, replacing with the smallest seen so far until reaching a fixed point. "); - - DECLARE_VM_BUILTIN(name({"simp_lemmas", "simplify_core"}), simp_lemmas_simplify_core); + DECLARE_VM_BUILTIN(name({"tactic", "simplify_core"}), tactic_simplify_core); + declare_vm_builtin(name({"tactic", "ext_simplify_core"}), + "tactic_ext_simplify_core", 10, tactic_ext_simplify_core); } void finalize_simplify() { - delete g_simplify_canonize_instances_fixed_point; - delete g_simplify_canonize_proofs_fixed_point; - delete g_simplify_lift_eq; - delete g_simplify_rewrite; - delete g_simplify_contextual; - delete g_simplify_max_steps; -} - -/* Entry point */ -simp_result simplify(type_context & tctx, name const & rel, simp_lemmas const & simp_lemmas, vm_obj const & prove_fn, expr const & e) { - return simplifier(tctx, tctx, rel, simp_lemmas, optional(prove_fn))(e); -} - -simp_result simplify(type_context & tctx, name const & rel, simp_lemmas const & simp_lemmas, expr const & e) { - return simplifier(tctx, tctx, rel, simp_lemmas, optional())(e); -} - -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) { - return simplifier(tctx, tctx_whnf, rel, simp_lemmas, optional(prove_fn))(e); -} - -simp_result simplify(type_context & tctx, type_context & tctx_whnf, name const & rel, simp_lemmas const & simp_lemmas, expr const & e) { - scope_trace_env scope(tctx.env(), tctx); - tout() << e << "\n"; - return simplifier(tctx, tctx_whnf, rel, simp_lemmas, optional())(e); -} - -optional prove_eq_by_simp(type_context & tctx, type_context & tctx_whnf, simp_lemmas const & simp_lemmas, expr const & e) { - scope_trace_env scope(tctx.env(), tctx); - simp_result r = simplify(tctx, tctx_whnf, get_eq_name(), simp_lemmas, e); - expr lhs, rhs; - tout() << r.get_new() << "\n-------------\n"; - if (is_eq(r.get_new(), lhs, rhs) && tctx.is_def_eq(lhs, rhs)) { - if (r.has_proof()) { - return some_expr(mk_app(tctx, get_eq_mpr_name(), r.get_proof(), mk_eq_refl(tctx, lhs))); - } else { - return some_expr(mk_eq_refl(tctx, lhs)); - } - } else if (is_true(r.get_new())) { - if (r.has_proof()) { - return some_expr(mk_app(tctx, get_eq_mpr_name(), r.get_proof(), mk_true_intro())); - } else { - return some_expr(mk_true_intro()); - } - } - return none_expr(); } } diff --git a/tests/lean/attribute_bug1.lean.expected.out b/tests/lean/attribute_bug1.lean.expected.out index 28f5ecd1fe..f04d7f7c8c 100644 --- a/tests/lean/attribute_bug1.lean.expected.out +++ b/tests/lean/attribute_bug1.lean.expected.out @@ -1,9 +1,9 @@ -attribute_bug1.lean:7:0: error: simp tactic failed to simplify +attribute_bug1.lean:7:0: error: simplify tactic failed to simplify state: n : ℕ ⊢ f n = n + 1 constant fdef : ∀ (n : ℕ), f n = n + 1 -attribute_bug1.lean:19:0: error: simp tactic failed to simplify +attribute_bug1.lean:19:0: error: simplify tactic failed to simplify state: n : ℕ ⊢ f n = n + 1 diff --git a/tests/lean/run/1093.lean b/tests/lean/run/1093.lean index 2f2d61ea98..089e91a896 100644 --- a/tests/lean/run/1093.lean +++ b/tests/lean/run/1093.lean @@ -6,6 +6,3 @@ attribute [simp] zadd example (a : nat) : 0 + a ≤ a := by do simp - -example (a : nat) : 0 + a ≥ a := -by do simp diff --git a/tests/lean/run/interactive1.lean b/tests/lean/run/interactive1.lean index 734f9ebc60..7ba78af854 100644 --- a/tests/lean/run/interactive1.lean +++ b/tests/lean/run/interactive1.lean @@ -45,4 +45,4 @@ begin end open tactic example (a b : nat) : a = b → h 0 a = b := -begin simp without bla, intros, try reflexivity end -- should fail if bla is used +begin ctx_simp without bla, intros, try reflexivity end -- should fail if bla is used diff --git a/tests/lean/run/rw_set4.lean b/tests/lean/run/rw_set4.lean index b562b0c296..aec7716b45 100644 --- a/tests/lean/run/rw_set4.lean +++ b/tests/lean/run/rw_set4.lean @@ -7,5 +7,5 @@ sorry print [congr] default -example (A : Type) (a b c : A) : (a = b) → (a = c) → a = b := by (simp >> intros >> reflexivity) -example (A : Type) (a b c : A) : (a = c) → (a = b) → a = b := by (simp >> intros >> reflexivity) +example (A : Type) (a b c : A) : (a = b) → (a = c) → a = b := by (ctx_simp >> intros >> reflexivity) +example (A : Type) (a b c : A) : (a = c) → (a = b) → a = b := by (ctx_simp >> intros >> reflexivity) diff --git a/tests/lean/run/simp1.lean b/tests/lean/run/simp1.lean index 41933a52dc..29372b2590 100644 --- a/tests/lean/run/simp1.lean +++ b/tests/lean/run/simp1.lean @@ -6,6 +6,5 @@ lemma bar : g y = z := sorry open tactic -set_option trace.simplifier.failure true example : g (f x y) = z := by simp example : g (f x (f x y)) = z := by simp diff --git a/tests/lean/run/simp_prove_fn.lean b/tests/lean/run/simp_prove_fn.lean deleted file mode 100644 index 683805bc31..0000000000 --- a/tests/lean/run/simp_prove_fn.lean +++ /dev/null @@ -1,16 +0,0 @@ -open tactic - -constants (A : Type.{1}) (x y z w v : A) (f : A → A) (H₁ : f (f x) = f y) (H₂ : f (f y) = f z) (H₃ : f (f z) = w) (g : A → A → A) - (H : ∀ a b : A, f (f (f (f a))) = b → f (g a b) = b) - -meta definition my_prove_fn : tactic unit := -do h₁ ← mk_const `H₁, - h₂ ← mk_const `H₂, - h₃ ← mk_const `H₃, - simp_using [h₁, h₂, h₃], reflexivity - -set_option trace.simplifier.prove true -example : f (g x w) = w := -by do h ← mk_const `H, - simplify_goal my_prove_fn [h], - reflexivity diff --git a/tests/lean/run/simplifier_canonize_instances.lean b/tests/lean/run/simplifier_canonize_instances.lean deleted file mode 100644 index fe1fca75f1..0000000000 --- a/tests/lean/run/simplifier_canonize_instances.lean +++ /dev/null @@ -1,24 +0,0 @@ -open tactic - -set_option pp.implicit true - -meta definition simplify_goal_force : tactic unit := -do (new_target, Heq) ← target >>= simplify failed [], - assert `Htarget new_target, swap, - Ht ← get_local `Htarget, - mk_app `eq.mpr [Heq, Ht] >>= apply_core transparency.all ff tt, - try reflexivity - -universe l - -constants (f₁ : Π (X : Type*) (X_grp : group X), X) -constants (f₂ : Π (X : Type*) [X_grp : group X], X) -constants (A : Type l) (A_grp₁ : group A) - -attribute [irreducible] noncomputable definition A_grp₂ : group A := A_grp₁ -attribute [irreducible] noncomputable definition A_grp₃ (t : true) : group A := A_grp₁ - -set_option simplify.canonize_instances_fixed_point true -example : @f₂ A A_grp₁ = @f₂ A A_grp₂ := by simplify_goal_force -example : @f₂ A (A_grp₃ trivial) = @f₂ A A_grp₂ := by simplify_goal_force -example : @f₂ A (A_grp₃ trivial) = @f₂ A A_grp₂ := by simplify_goal_force diff --git a/tests/lean/run/simplifier_custom_relations.lean b/tests/lean/run/simplifier_custom_relations.lean index b7413e6408..6eac102dfd 100644 --- a/tests/lean/run/simplifier_custom_relations.lean +++ b/tests/lean/run/simplifier_custom_relations.lean @@ -26,7 +26,7 @@ print [congr] default meta definition relsimp_core (e : expr) : tactic (expr × expr) := do S ← simp_lemmas.mk_default, e_type ← infer_type e >>= whnf, - S^.simplify_core failed `rel e + simplify_core default_simplify_config S `rel e example : rel (h (f x)) z := by do e₁ ← to_expr `(h (f x)), diff --git a/tests/lean/simplifier_prove_failures.lean b/tests/lean/simplifier_prove_failures.lean deleted file mode 100644 index 893f7651aa..0000000000 --- a/tests/lean/simplifier_prove_failures.lean +++ /dev/null @@ -1,16 +0,0 @@ -open tactic - -constants (P Q R : Prop) (HP : P) (HPQ : P → Q) (HQR : Q → R = true) -attribute [simp] HQR - -meta definition prove_skip : tactic unit := skip -meta definition prove_fail : tactic unit := failed -meta definition prove_partial_assign : tactic unit := mk_const `HPQ >>= apply -meta definition prove_full_assign : tactic unit := (mk_const `HPQ >>= apply) >> (mk_const `HP) >>= exact - -set_option trace.simplifier.prove true - -example : R := by simplify_goal prove_skip [] >> try triv -example : R := by simplify_goal prove_fail [] >> try triv -example : R := by simplify_goal prove_partial_assign [] >> try triv -example : R := by simplify_goal prove_full_assign [] >> try triv diff --git a/tests/lean/simplifier_prove_failures.lean.expected.out b/tests/lean/simplifier_prove_failures.lean.expected.out deleted file mode 100644 index 1391d69af0..0000000000 --- a/tests/lean/simplifier_prove_failures.lean.expected.out +++ /dev/null @@ -1,17 +0,0 @@ -[simplifier.prove] goal: ?m_1 : Q -[simplifier.prove] prove_fn succeeded but did not return a proof -simplifier_prove_failures.lean:13:15: error: simp tactic failed to simplify -state: -⊢ R -[simplifier.prove] goal: ?m_1 : Q -[simplifier.prove] prove_fn failed to prove Q -simplifier_prove_failures.lean:14:15: error: simp tactic failed to simplify -state: -⊢ R -[simplifier.prove] goal: ?m_1 : Q -[simplifier.prove] prove_fn succeeded but left an unrecognized metavariable of type P in proof -simplifier_prove_failures.lean:15:15: error: simp tactic failed to simplify -state: -⊢ R -[simplifier.prove] goal: ?m_1 : Q -[simplifier.prove] success: HPQ HP : Q