diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index 415cae374b..fd8545eb93 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/src/frontends/lean/builtin_cmds.cpp @@ -34,7 +34,6 @@ Author: Leonardo de Moura #include "library/compiler/vm_compiler.h" #include "library/tactic/kabstract.h" #include "library/tactic/elaborate.h" -#include "library/tactic/simplifier/simp_extensions.h" #include "library/tactic/tactic_state.h" #include "frontends/lean/util.h" #include "frontends/lean/parser.h" @@ -375,26 +374,6 @@ static environment init_quotient_cmd(parser & p) { return module::declare_quotient(p.env()); } -// register_simp_ext ([priority ]) -static environment register_simp_ext_cmd(parser & p) { - environment env = p.env(); - name head = p.check_constant_next("invalid #register_simp_ext_cmd command, constant expected"); - name simp_ext_name = p.check_constant_next("invalid #register_simp_ext_cmd command, constant expected"); - - unsigned prio = LEAN_DEFAULT_PRIORITY; - auto pos = p.pos(); - decl_attributes attrs; - attrs.parse(p); - if (auto const & entry = head_opt(attrs.get_entries())) - throw parser_error(sstream() << "invalid #register_simp_ext_cmd command, unexpected attribute [" - << entry->m_attr->get_name() << "]", pos); - if (attrs.get_priority()) - prio = *attrs.get_priority(); - bool persistent = true; - env = add_simp_extension(env, p.ios(), head, simp_ext_name, prio, persistent); - return env; -} - /* Temporary procedure that converts metavariables in \c e to metavar_context metavariables. After we convert the frontend to type_context, we will not need to use this procedure. @@ -577,7 +556,6 @@ void init_cmd_table(cmd_table & r) { add_cmd(r, cmd_info("help", "brief description of available commands and options", help_cmd)); add_cmd(r, cmd_info("init_quotient", "initialize quotient type computational rules", init_quotient_cmd)); add_cmd(r, cmd_info("declare_trace", "declare a new trace class (for debugging Lean tactics)", declare_trace_cmd)); - add_cmd(r, cmd_info("register_simp_ext", "register simplifier extension", register_simp_ext_cmd)); add_cmd(r, cmd_info("add_key_equivalence", "register that to symbols are equivalence for key-matching", add_key_equivalence_cmd)); add_cmd(r, cmd_info("run_command", "execute an user defined command at top-level", run_command_cmd)); add_cmd(r, cmd_info("#erase_cache", "erase cached definition (for debugging purposes)", erase_cache_cmd)); diff --git a/src/frontends/lean/print_cmd.cpp b/src/frontends/lean/print_cmd.cpp index 550f403864..5031ee5b3c 100644 --- a/src/frontends/lean/print_cmd.cpp +++ b/src/frontends/lean/print_cmd.cpp @@ -27,7 +27,6 @@ Author: Leonardo de Moura #include "library/rfl_lemmas.h" #include "library/tactic/kabstract.h" #include "library/tactic/simplifier/simp_lemmas.h" -#include "library/tactic/simplifier/simp_extensions.h" #include "frontends/lean/parser.h" #include "frontends/lean/util.h" #include "frontends/lean/tokens.h" diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp index 9c246a7dba..2b0675fdc6 100644 --- a/src/frontends/lean/token_table.cpp +++ b/src/frontends/lean/token_table.cpp @@ -108,8 +108,7 @@ void init_token_table(token_table & t) { "precedence", "reserve", "infixl", "infixr", "infix", "postfix", "prefix", "notation", "exit", "set_option", "open", "export", "override", "@[", "attribute", "persistent", "instance", "include", "omit", "init_quotient", - "init_hits", "declare_trace", "register_simp_ext", - "run_command", "add_key_equivalence", "#erase_cache", + "init_hits", "declare_trace", "run_command", "add_key_equivalence", "#erase_cache", "#compile", "#unify", nullptr}; pair aliases[] = diff --git a/src/library/inductive_compiler/nested.cpp b/src/library/inductive_compiler/nested.cpp index f047286d10..55c22d773f 100644 --- a/src/library/inductive_compiler/nested.cpp +++ b/src/library/inductive_compiler/nested.cpp @@ -1243,7 +1243,6 @@ class add_nested_inductive_decl_fn { opts = opts.update(get_simplify_nary_assoc_name(), false); opts = opts.update(get_simplify_memoize_name(), true); opts = opts.update(get_simplify_contextual_name(), false); - opts = opts.update(get_simplify_user_extensions_name(), false); opts = opts.update(get_simplify_rewrite_name(), true); opts = opts.update(get_simplify_unsafe_nary_name(), false); opts = opts.update(get_simplify_theory_name(), true); diff --git a/src/library/tactic/simplifier/CMakeLists.txt b/src/library/tactic/simplifier/CMakeLists.txt index 7616ebde02..afc2fc6522 100644 --- a/src/library/tactic/simplifier/CMakeLists.txt +++ b/src/library/tactic/simplifier/CMakeLists.txt @@ -1,3 +1,3 @@ add_library(simplifier OBJECT init_module.cpp ceqv.cpp simplifier.cpp simp_lemmas.cpp - simp_extensions.cpp prop_simplifier.cpp arith_simplifier.cpp theory_simplifier.cpp util.cpp + prop_simplifier.cpp arith_simplifier.cpp theory_simplifier.cpp util.cpp ) diff --git a/src/library/tactic/simplifier/init_module.cpp b/src/library/tactic/simplifier/init_module.cpp index 34053d4a21..2fb5558353 100644 --- a/src/library/tactic/simplifier/init_module.cpp +++ b/src/library/tactic/simplifier/init_module.cpp @@ -6,7 +6,6 @@ Author: Daniel Selsam #include "library/trace.h" #include "library/tactic/simplifier/util.h" #include "library/tactic/simplifier/simp_lemmas.h" -#include "library/tactic/simplifier/simp_extensions.h" #include "library/tactic/simplifier/prop_simplifier.h" #include "library/tactic/simplifier/arith_simplifier.h" #include "library/tactic/simplifier/theory_simplifier.h" @@ -19,7 +18,6 @@ void initialize_simplifier_module() { initialize_simp_util(); initialize_simp_lemmas(); - initialize_simp_extensions(); initialize_prop_simplifier(); initialize_arith_simplifier(); initialize_theory_simplifier(); @@ -31,7 +29,6 @@ void finalize_simplifier_module() { finalize_theory_simplifier(); finalize_arith_simplifier(); finalize_prop_simplifier(); - finalize_simp_extensions(); finalize_simp_lemmas(); finalize_simp_util(); } diff --git a/src/library/tactic/simplifier/simp_extensions.cpp b/src/library/tactic/simplifier/simp_extensions.cpp deleted file mode 100644 index 80c8b09e70..0000000000 --- a/src/library/tactic/simplifier/simp_extensions.cpp +++ /dev/null @@ -1,124 +0,0 @@ -/* -Copyright (c) 2016 Daniel Selsam. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Author: Daniel Selsam -*/ -#include -#include "util/priority_queue.h" -#include "library/trace.h" -#include "library/scoped_ext.h" -#include "library/attribute_manager.h" -#include "library/vm/vm.h" -#include "library/tactic/simplifier/simp_extensions.h" - -namespace lean { - -static std::string * g_key = nullptr; - -struct simp_ext_entry { - unsigned m_prio; - name m_head; - name m_ext_name; - - simp_ext_entry(unsigned prio, name head, name ext_name): - m_prio(prio), m_head(head), m_ext_name(ext_name) {} -}; - -struct simp_ext_record { - name m_ext_name; - unsigned m_ext_id; - simp_ext_record() {} - simp_ext_record(name ext_name, unsigned ext_id): m_ext_name(ext_name), m_ext_id(ext_id) {} -}; - -struct simp_ext_record_cmp { - int operator()(simp_ext_record const & r1, simp_ext_record const & r2) const { - // If the names are the same and the environments are compatible, then the ids must be the same as well - return quick_cmp(r1.m_ext_name, r2.m_ext_name); - } -}; - -typedef name_map> simp_ext_state; - -struct simp_ext_config { - typedef simp_ext_entry entry; - typedef simp_ext_state state; - - static void add_entry(environment const & env, io_state const &, state & s, entry const & e) { - if (optional fn_idx = get_vm_constant_idx(env, e.m_ext_name)) { - priority_queue m; - if (auto q = s.find(e.m_head)) { - m = *q; - } - m.insert(simp_ext_record(e.m_ext_name, *fn_idx), e.m_prio); - s.insert(e.m_head, m); - } else { - throw exception(sstream() << "error in adding simplifier extension: no vm_decl for " << e.m_ext_name << "\n"); - } - } - - static std::string const & get_serialization_key() { - return *g_key; - } - static void write_entry(serializer & s, entry const & e) { - s << e.m_prio << e.m_head << e.m_ext_name; - } - static entry read_entry(deserializer & d) { - unsigned prio; name head; name ext_name; - d >> prio >> head >> ext_name; - return entry(prio, head, ext_name); - } - static optional get_fingerprint(entry const & e) { - return some(hash(e.m_head.hash(), hash(e.m_ext_name.hash(), e.m_prio))); - } -}; - -typedef scoped_ext simp_ext_ext; - -environment add_simp_extension(environment const & env, io_state const & ios, name const & head, name const & simp_ext_name, unsigned prio, bool persistent) { - return simp_ext_ext::add_entry(env, ios, simp_ext_entry(prio, head, simp_ext_name), persistent); -} - -format pp_simp_extensions_for_head(priority_queue const & q) { - format fmt; - q.for_each([&](simp_ext_record const & r) { - fmt += format(r.m_ext_name); - unsigned prio = *q.get_prio(r); - if (prio != LEAN_DEFAULT_PRIORITY) - fmt += space() + paren(format(prio)); - fmt += line(); - }); - return fmt; -} - -format pp_simp_extensions(environment const & env) { - simp_ext_state s = simp_ext_ext::get_state(env); - format fmt; - s.for_each([&](name const & head, priority_queue const & q) { - fmt += format("simplification extensions for ") + format(head) + line(); - fmt += pp_simp_extensions_for_head(q); - }); - return fmt; -} - -void get_simp_extensions_for(environment const & env, name const & head, buffer & ext_ids) { - simp_ext_state s = simp_ext_ext::get_state(env); - if (auto q = s.find(head)) { - buffer records; - q->for_each([&](simp_ext_record const & r) { - ext_ids.push_back(r.m_ext_id); - }); - } -} - -void initialize_simp_extensions() { - g_key = new std::string("SIMP_EXT"); - simp_ext_ext::initialize(); -} - -void finalize_simp_extensions() { - simp_ext_ext::finalize(); - delete g_key; -} - -} diff --git a/src/library/tactic/simplifier/simp_extensions.h b/src/library/tactic/simplifier/simp_extensions.h deleted file mode 100644 index 9150e5786d..0000000000 --- a/src/library/tactic/simplifier/simp_extensions.h +++ /dev/null @@ -1,22 +0,0 @@ -/* -Copyright (c) 2016 Daniel Selsam. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Author: Daniel Selsam -*/ -#pragma once -#include "kernel/expr_pair.h" -#include "library/head_map.h" -#include "library/type_context.h" - -namespace lean { - -environment add_simp_extension(environment const & env, io_state const & ios, name const & head, name const & ext_name, unsigned prio, bool persistent); - -format pp_simp_extensions(environment const & env); - -void get_simp_extensions_for(environment const & env, name const & head, buffer & ext_ids); - -void initialize_simp_extensions(); -void finalize_simp_extensions(); - -} diff --git a/src/library/tactic/simplifier/simplifier.cpp b/src/library/tactic/simplifier/simplifier.cpp index 8910dc98d7..b3e2e05036 100644 --- a/src/library/tactic/simplifier/simplifier.cpp +++ b/src/library/tactic/simplifier/simplifier.cpp @@ -37,7 +37,6 @@ Author: Daniel Selsam #include "library/tactic/app_builder_tactics.h" #include "library/tactic/simplifier/simplifier.h" #include "library/tactic/simplifier/simp_lemmas.h" -#include "library/tactic/simplifier/simp_extensions.h" #include "library/tactic/simplifier/theory_simplifier.h" #include "library/tactic/simplifier/ceqv.h" #include "library/tactic/simplifier/util.h" @@ -54,9 +53,6 @@ Author: Daniel Selsam #ifndef LEAN_DEFAULT_SIMPLIFY_CONTEXTUAL #define LEAN_DEFAULT_SIMPLIFY_CONTEXTUAL true #endif -#ifndef LEAN_DEFAULT_SIMPLIFY_USER_EXTENSIONS -#define LEAN_DEFAULT_SIMPLIFY_USER_EXTENSIONS true -#endif #ifndef LEAN_DEFAULT_SIMPLIFY_REWRITE #define LEAN_DEFAULT_SIMPLIFY_REWRITE true #endif @@ -93,7 +89,6 @@ static name * g_simplify_max_steps = nullptr; static name * g_simplify_nary_assoc = nullptr; static name * g_simplify_memoize = nullptr; static name * g_simplify_contextual = nullptr; -static name * g_simplify_user_extensions = nullptr; static name * g_simplify_rewrite = nullptr; static name * g_simplify_unsafe_nary = nullptr; static name * g_simplify_theory = nullptr; @@ -107,7 +102,6 @@ name get_simplify_max_steps_name() { return *g_simplify_max_steps; } name get_simplify_nary_assoc_name() { return *g_simplify_nary_assoc; } name get_simplify_memoize_name() { return *g_simplify_memoize; } name get_simplify_contextual_name() { return *g_simplify_contextual; } -name get_simplify_user_extensions_name() { return *g_simplify_user_extensions; } name get_simplify_rewrite_name() { return *g_simplify_rewrite; } name get_simplify_unsafe_nary_name() { return *g_simplify_unsafe_nary; } name get_simplify_theory_name() { return *g_simplify_theory; } @@ -133,10 +127,6 @@ static bool get_simplify_contextual(options const & o) { return o.get_bool(*g_simplify_contextual, LEAN_DEFAULT_SIMPLIFY_CONTEXTUAL); } -static bool get_simplify_user_extensions(options const & o) { - return o.get_bool(*g_simplify_user_extensions, LEAN_DEFAULT_SIMPLIFY_USER_EXTENSIONS); -} - static bool get_simplify_rewrite(options const & o) { return o.get_bool(*g_simplify_rewrite, LEAN_DEFAULT_SIMPLIFY_REWRITE); } @@ -196,7 +186,6 @@ class simplifier { unsigned m_nary_assoc; bool m_memoize; bool m_contextual; - bool m_user_extensions; bool m_rewrite; bool m_unsafe_nary; bool m_theory; @@ -334,41 +323,6 @@ class simplifier { return r; } - // Binary simplify methods - simp_result simplify_user_extensions_binary(expr const & old_e) { - expr op = get_app_fn(old_e); - if (!is_constant(op)) return simp_result(old_e); - name head = const_name(op); - buffer ext_ids; - get_simp_extensions_for(m_tctx.env(), head, ext_ids); - for (unsigned ext_id : ext_ids) { - expr old_e_type = m_tctx.infer(old_e); - metavar_context mctx = m_tctx.mctx(); - expr result_mvar = mctx.mk_metavar_decl(m_tctx.lctx(), old_e_type); - m_tctx.set_mctx(mctx); // the app-builder needs to know about these metavars - expr goal_type = mk_app(m_tctx, m_rel, old_e, result_mvar); - expr goal_mvar = mctx.mk_metavar_decl(m_tctx.lctx(), goal_type); - vm_obj s = to_obj(tactic_state(m_tctx.env(), m_tctx.get_options(), mctx, list(goal_mvar), goal_mvar)); - vm_obj simp_ext_result = invoke(ext_id, s); - optional s_new = is_tactic_success(simp_ext_result); - // TODO(dhs): create a bool metavar for the `done` flag - if (s_new) { - m_tctx.set_mctx(s_new->mctx()); - expr result = m_tctx.instantiate_mvars(result_mvar); - expr proof = m_tctx.instantiate_mvars(goal_mvar); - if (is_app_of(proof, get_eq_refl_name(), 2) || is_app_of(proof, get_rfl_name(), 2)) { - return simp_result(result); - } else { - return simp_result(result, proof); - } - } else { - lean_trace(name({"simplifier", "extensions"}), - tout() << "extension failed on goal " << goal_type << "\n";); - } - } - return simp_result(old_e); - } - simp_result simplify_rewrite_binary(expr const & e) { simp_lemmas slss = ::lean::join(m_slss, m_ctx_slss); simp_lemmas_for const * sr = slss.find(m_rel); @@ -466,14 +420,6 @@ class simplifier { return r_rewrite; } } - - if (m_user_extensions) { - simp_result r_user = simplify_user_extensions_binary(e); - if (r_user.get_new() != e) { - lean_trace_d(name({"simplifier", "user_extensions"}), tout() << e << " ==> " << r_user.get_new() << "\n";); - return r_user; - } - } } // [1] Simplify subterms using congruence @@ -521,17 +467,6 @@ class simplifier { return join(r, r_rewrite); } } - - if (m_user_extensions) { - simp_result r_user = simplify_user_extensions_binary(r.get_new()); - if (r_user.get_new() != r.get_new()) { - lean_trace_d(name({"simplifier", "user_extensions"}), tout() << r.get_new() << " ==> " << r_user.get_new() << "\n";); - simp_result r_join_user = join(r, r_user); - if (r_user.is_done()) - r_join_user.set_done(); - return r_join_user; - } - } } // [5] Simplify with the theory simplifier @@ -640,17 +575,6 @@ class simplifier { return optional(simp_result(new_rhs, pf)); } - optional simplify_user_extensions_nary(expr const & /* assoc */, expr const & old_e, expr const & /* op */, buffer const & /* nary_args */) { - // For now, user extensions are not aware of the binary/nary distinction, except that they are guaranteed that - // if an operator is an instance of [is_associative] for the relation in question, the user extension will only be - // called on the outermost applications. - simp_result r = simplify_user_extensions_binary(old_e); - if (r.get_new() != old_e) - return optional(r); - else - return optional(); - } - simp_result simplify_subterms_app_nary_core(expr const & old_op, expr const & new_op, optional const & pf_op, expr const & e) { expr arg1, arg2; optional op = get_binary_op(e, arg1, arg2); @@ -700,12 +624,6 @@ class simplifier { return join(r_flat, *r_rewrite); } } - if (m_user_extensions) { - if (optional r_user = simplify_user_extensions_nary(assoc, r_flat.get_new(), op, nary_args)) { - lean_trace_d(name({"simplifier", "user_extensions"}), tout() << old_e << " ==> " << r_user->get_new() << "\n";); - return join(r_flat, *r_user); - } - } } simp_result r_congr = simplify_subterms_app_nary(op, old_e); @@ -726,12 +644,6 @@ class simplifier { return join(r_congr_flat, *r_rewrite); } } - if (m_user_extensions) { - if (optional r_user = simplify_user_extensions_nary(assoc, r_congr_flat.get_new(), new_op, new_nary_args)) { - lean_trace_d(name({"simplifier", "user_extensions"}), tout() << old_e << " ==> " << r_user->get_new() << "\n";); - return join(r_congr_flat, *r_user); - } - } } // [5] Simplify with the theory simplifier @@ -796,7 +708,6 @@ public: m_nary_assoc(get_simplify_nary_assoc(tctx.get_options())), m_memoize(get_simplify_memoize(tctx.get_options())), m_contextual(get_simplify_contextual(tctx.get_options())), - m_user_extensions(get_simplify_user_extensions(tctx.get_options())), m_rewrite(get_simplify_rewrite(tctx.get_options())), m_unsafe_nary(get_simplify_unsafe_nary(tctx.get_options())), m_theory(get_simplify_theory(tctx.get_options())), @@ -1434,7 +1345,6 @@ vm_obj tactic_simplify_core(vm_obj const & prove_fn, vm_obj const & rel_name, vm /* Setup and teardown */ void initialize_simplifier() { register_trace_class(name({"simplifier", "congruence"})); - register_trace_class(name({"simplifier", "user_extensions"})); register_trace_class(name({"simplifier", "failure"})); register_trace_class(name({"simplifier", "failed"})); register_trace_class(name({"simplifier", "perm"})); @@ -1456,7 +1366,6 @@ void initialize_simplifier() { g_simplify_nary_assoc = new name{*g_simplify_prefix, "nary_assoc"}; g_simplify_memoize = new name{*g_simplify_prefix, "memoize"}; g_simplify_contextual = new name{*g_simplify_prefix, "contextual"}; - g_simplify_user_extensions = new name{*g_simplify_prefix, "user_extensions"}; g_simplify_rewrite = new name{*g_simplify_prefix, "rewrite"}; g_simplify_unsafe_nary = new name{*g_simplify_prefix, "unsafe_nary"}; g_simplify_theory = new name{*g_simplify_prefix, "theory"}; @@ -1474,8 +1383,6 @@ void initialize_simplifier() { "(simplify) memoize simplifications"); register_bool_option(*g_simplify_contextual, LEAN_DEFAULT_SIMPLIFY_CONTEXTUAL, "(simplify) use contextual simplification"); - register_bool_option(*g_simplify_user_extensions, LEAN_DEFAULT_SIMPLIFY_USER_EXTENSIONS, - "(simplify) simplify with user_extensions"); register_bool_option(*g_simplify_rewrite, LEAN_DEFAULT_SIMPLIFY_REWRITE, "(simplify) rewrite with simp_lemmas"); register_bool_option(*g_simplify_unsafe_nary, LEAN_DEFAULT_SIMPLIFY_UNSAFE_NARY, @@ -1508,7 +1415,6 @@ void finalize_simplifier() { delete g_simplify_theory; delete g_simplify_unsafe_nary; delete g_simplify_rewrite; - delete g_simplify_user_extensions; delete g_simplify_contextual; delete g_simplify_memoize; delete g_simplify_nary_assoc; diff --git a/src/library/tactic/simplifier/simplifier.h b/src/library/tactic/simplifier/simplifier.h index b1f1db855c..eba2463e4a 100644 --- a/src/library/tactic/simplifier/simplifier.h +++ b/src/library/tactic/simplifier/simplifier.h @@ -20,7 +20,6 @@ name get_simplify_max_steps_name(); name get_simplify_nary_assoc_name(); name get_simplify_memoize_name(); name get_simplify_contextual_name(); -name get_simplify_user_extensions_name(); name get_simplify_rewrite_name(); name get_simplify_unsafe_nary_name(); name get_simplify_theory_name(); diff --git a/tests/lean/run/simp_ext_refl.lean b/tests/lean/run/simp_ext_refl.lean deleted file mode 100644 index 5db3b1e855..0000000000 --- a/tests/lean/run/simp_ext_refl.lean +++ /dev/null @@ -1,32 +0,0 @@ -open tactic - -constants (A : Type.{1}) (x y z : A) (g : A → A) (Hg : g y = z) -attribute [simp] Hg - -noncomputable definition f (a : A) := y -lemma f.def : ∀ (a), f a = y := λ a, rfl - -meta definition simp_f_to_y : tactic unit := mk_eq_simp_ext $ - λ e, if expr.get_app_num_args e = 1 - then do res ← mk_const `y, - pf ← mk_app `rfl [e], - return (res, pf) - else fail "expected f applied to one arg" - -meta definition simp_f_to_y₂ : tactic unit := mk_eq_simp_ext $ - λ e, if expr.get_app_num_args e = 1 - then do res ← mk_const `y, - pf ← mk_app `f.def [expr.app_arg e], - return (res, pf) - else fail "expected f applied to one arg" - -register_simp_ext f simp_f_to_y - -definition foo : g (f x) = z := by simp - -register_simp_ext f simp_f_to_y₂ - -definition foo₂ : g (f x) = z := by simp - -print foo -print foo₂ diff --git a/tests/lean/run/simp_orderings.lean b/tests/lean/run/simp_orderings.lean deleted file mode 100644 index 3649d0d05a..0000000000 --- a/tests/lean/run/simp_orderings.lean +++ /dev/null @@ -1,62 +0,0 @@ -open tactic - -------------- -namespace simp_lemmas - -constants (A : Type.{1}) (x y z : A) (Hxy : x = y) (Hxz : x = z) -attribute [simp] Hxy -attribute [simp] Hxz - - -example : x = z := by simp - -end simp_lemmas - -------------- -namespace simp_lemmas_args - -constants (A : Type.{1}) (x y z : A) (Hxy : x = y) (Hxz : x = z) -attribute [simp] Hxy - -example : x = z := -by do H ← mk_const `simp_lemmas_args.Hxz, - `[simp [%%H]] - -end simp_lemmas_args - -------------- -namespace simp_args - -constants (A : Type.{1}) (x y z : A) (Hxy : x = y) (Hxz : x = z) - -example : x = z := -by do Hy ← mk_const `simp_args.Hxy, - Hz ← mk_const `simp_args.Hxz, - -- CONFIRM(leo): latter arguments should get priority? - `[simp [%%Hy, %%Hz]] - -end simp_args - -------------- -namespace simp_extensions - -constants (A : Type.{1}) (x y z : A) (Hxy : x = y) (Hxz : x = z) - -meta definition simp_x_to_y : tactic unit := mk_eq_simp_ext $ - λ e, do res ← mk_const `simp_extensions.y, - pf ← mk_const `simp_extensions.Hxy, - return (res, pf) - -meta definition simp_x_to_z : tactic unit := mk_eq_simp_ext $ - λ e, do res ← mk_const `simp_extensions.z, - pf ← mk_const `simp_extensions.Hxz, - return (res, pf) - -register_simp_ext x simp_x_to_y -register_simp_ext x simp_x_to_z - -example : x = z := by simp - -end simp_extensions - ----------------