From 924b4d3bdcb6510dc7d7b3d33d2b9d7792153e4e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 12 Oct 2016 14:36:00 -0700 Subject: [PATCH] refactor(library, library/tactic): move simp_lemmas and eqn_lemmas to tactic folder They were at src/library because we hoped we would be able to use them in the type_context unifier. However, the plan did not work for several reasons. We saved the partial implementation in the branch: https://github.com/leodemoura/lean/tree/type_context_with_refl_lemmas Here are the problems: 1) We have to be able to rewrite even when the type context is already in tmp-mode. This is an issue because the tmp metavariables in the refl lemma clash with the ones created in the type context. Solution: implemented lift operation for idx metavariables, and custom match. This solution is not perfect since the lifting is extra overhead. 2) The term being "unfolded" may be stuck. Example: nat.add n (@one nat ?m) will not match the pattern nat.add ?x_0 (nat.succ ?x_1) because ?m is not assigned yet. We can assign it during the matching process because it is a regular metavariable and the matching is performed in tmp_mode. Possible workaround a) try to instanciate type class instances before we try the refl lemmas. This is a potential performance problem because the term can be arbitrarily big. The current heuristics we use to speed up the process do not work for the example above. Possible workaround b) allow regular metavariables be assigned by type class resolution even when we are in tmp-mode. We have not tried to implement any of these workarounds. 3) There are many more lazy-delta steps. Before this feature, when we unfold `nat.add a (succ ... (succ b) ...)`, we are done with delta-reduction. It is just iota and beta after that. However, with refl-lemmas, the term `nat.add a (succ ... (succ b) ...)` produces one lazy-delta step per succ. This produces nasty side-effects because of the The heuristic (f t =?= f s) ==> (t =?= s). Examples such as (fib 8) =?= 34 will take a very long time because of this heuristic. Possible workaround: cache failures like we did in Lean2. However, failure are only easy to cache if there are no meta-variables. 4) The type context trace gets very confusing since we use is_def_eq for matching lhs while we are computing is_def_eq. Possible workaround: disable trace when trying refl_lemmas. 5) We must be able to temporarily disable the feature. Example: when proving a refl_lemma for a definition `f`, we may have to expand the nested definitions (e.g., for match-end blocks) 6) refl/simp lemmas were designed to rewrite elaborated terms. Using them during unification may produce a series of unexpected behaviors since terms usually contain many regular and universe meta-variables. 7) We need to define a notion of "refl stuck application". Right now, a metavar is stuck, a projection is stuck if the structure is stuck, a recursor is stuck is the major premise is stuck. An application (f ...) is refl-lemma stuck if f has refl-lemmas associated with it, AND metavariables occurring in arguments are preventing a refl-lemma from being applied. --- library/init/meta/simp_tactic.lean | 5 ++++- src/frontends/lean/definition_cmds.cpp | 2 +- src/frontends/lean/print_cmd.cpp | 2 +- src/library/CMakeLists.txt | 3 +-- src/library/constructions/has_sizeof.cpp | 2 +- src/library/constructions/has_sizeof.h | 2 +- src/library/equations_compiler/util.cpp | 2 +- src/library/inductive_compiler/nested.cpp | 2 +- src/library/init_module.cpp | 6 ------ src/library/tactic/CMakeLists.txt | 3 ++- src/library/tactic/dsimplify.h | 2 +- src/library/{ => tactic}/eqn_lemmas.cpp | 2 +- src/library/{ => tactic}/eqn_lemmas.h | 2 +- src/library/tactic/init_module.cpp | 6 ++++++ src/library/{ => tactic}/simp_lemmas.cpp | 2 +- src/library/{ => tactic}/simp_lemmas.h | 0 src/library/tactic/simp_lemmas_tactics.cpp | 12 ++++++------ src/library/tactic/simp_lemmas_tactics.h | 2 +- src/library/tactic/simplifier/simplifier.cpp | 2 +- src/library/tactic/simplifier/simplifier.h | 2 +- src/library/tactic/unfold_tactic.cpp | 2 +- 21 files changed, 33 insertions(+), 30 deletions(-) rename src/library/{ => tactic}/eqn_lemmas.cpp (98%) rename src/library/{ => tactic}/eqn_lemmas.h (92%) rename src/library/{ => tactic}/simp_lemmas.cpp (99%) rename src/library/{ => tactic}/simp_lemmas.h (100%) diff --git a/library/init/meta/simp_tactic.lean b/library/init/meta/simp_tactic.lean index a90539b8ab..0f332cb58a 100644 --- a/library/init/meta/simp_tactic.lean +++ b/library/init/meta/simp_tactic.lean @@ -49,7 +49,10 @@ meta def simp_lemmas.rewrite : simp_lemmas → tactic unit → name → expr → simp_lemmas.rewrite_core reducible /- (simp_lemmas.drewrite s e) tries to rewrite 'e' using only refl lemmas in 's' -/ -meta constant simp_lemmas.drewrite : simp_lemmas → expr → tactic expr +meta constant simp_lemmas.drewrite_core : transparency → simp_lemmas → expr → tactic 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. diff --git a/src/frontends/lean/definition_cmds.cpp b/src/frontends/lean/definition_cmds.cpp index 90b021444e..f1f7448288 100644 --- a/src/frontends/lean/definition_cmds.cpp +++ b/src/frontends/lean/definition_cmds.cpp @@ -23,10 +23,10 @@ Author: Leonardo de Moura #include "library/error_handling.h" #include "library/scope_pos_info_provider.h" #include "library/replace_visitor.h" -#include "library/eqn_lemmas.h" #include "library/equations_compiler/equations.h" #include "library/compiler/vm_compiler.h" #include "library/compiler/rec_fn_macro.h" +#include "library/tactic/eqn_lemmas.h" #include "frontends/lean/parser.h" #include "frontends/lean/tokens.h" #include "frontends/lean/elaborator.h" diff --git a/src/frontends/lean/print_cmd.cpp b/src/frontends/lean/print_cmd.cpp index 9ae82e4c1b..f7c9f62e84 100644 --- a/src/frontends/lean/print_cmd.cpp +++ b/src/frontends/lean/print_cmd.cpp @@ -24,7 +24,7 @@ Author: Leonardo de Moura #include "library/type_context.h" #include "library/unification_hint.h" #include "library/reducible.h" -#include "library/simp_lemmas.h" +#include "library/tactic/simp_lemmas.h" #include "library/tactic/kabstract.h" #include "frontends/lean/parser.h" #include "frontends/lean/util.h" diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt index e2ac35bbb6..3f2257e6f5 100644 --- a/src/library/CMakeLists.txt +++ b/src/library/CMakeLists.txt @@ -15,5 +15,4 @@ add_library(library OBJECT deep_copy.cpp expr_lt.cpp io_state.cpp fun_info.cpp congr_lemma.cpp defeq_canonizer.cpp scope_pos_info_provider.cpp mpq_macro.cpp arith_instance_manager.cpp replace_visitor_with_tc.cpp aux_definition.cpp inverse.cpp library_system.cpp pattern_attribute.cpp choice.cpp - locals.cpp normalize.cpp discr_tree.cpp simp_lemmas.cpp eqn_lemmas.cpp - ) + locals.cpp normalize.cpp discr_tree.cpp) diff --git a/src/library/constructions/has_sizeof.cpp b/src/library/constructions/has_sizeof.cpp index ec570f6334..b5c8f13435 100644 --- a/src/library/constructions/has_sizeof.cpp +++ b/src/library/constructions/has_sizeof.cpp @@ -23,7 +23,7 @@ Author: Daniel Selsam #include "library/trace.h" #include "library/module.h" #include "library/constants.h" -#include "library/simp_lemmas.h" +#include "library/tactic/simp_lemmas.h" #include "library/constructions/has_sizeof.h" namespace lean { diff --git a/src/library/constructions/has_sizeof.h b/src/library/constructions/has_sizeof.h index dd50df952f..c161425e2c 100644 --- a/src/library/constructions/has_sizeof.h +++ b/src/library/constructions/has_sizeof.h @@ -6,7 +6,7 @@ Author: Daniel Selsam */ #pragma once #include "kernel/environment.h" -#include "library/simp_lemmas.h" +#include "library/tactic/simp_lemmas.h" namespace lean { /** \brief Given an inductive datatype \c n in \c env, add diff --git a/src/library/equations_compiler/util.cpp b/src/library/equations_compiler/util.cpp index 2aa677c5fe..9a9ab9cba3 100644 --- a/src/library/equations_compiler/util.cpp +++ b/src/library/equations_compiler/util.cpp @@ -18,9 +18,9 @@ Author: Leonardo de Moura #include "library/inverse.h" #include "library/replace_visitor.h" #include "library/aux_definition.h" -#include "library/eqn_lemmas.h" #include "library/scope_pos_info_provider.h" #include "library/compiler/vm_compiler.h" +#include "library/tactic/eqn_lemmas.h" #include "library/equations_compiler/equations.h" #include "library/equations_compiler/util.h" diff --git a/src/library/inductive_compiler/nested.cpp b/src/library/inductive_compiler/nested.cpp index 339d6bb15f..d50d491c5f 100644 --- a/src/library/inductive_compiler/nested.cpp +++ b/src/library/inductive_compiler/nested.cpp @@ -29,7 +29,7 @@ Author: Daniel Selsam #include "library/protected.h" #include "library/attribute_manager.h" #include "library/pattern_attribute.h" -#include "library/simp_lemmas.h" +#include "library/tactic/simp_lemmas.h" #include "library/constructions/has_sizeof.h" #include "library/inductive_compiler/ginductive.h" #include "library/inductive_compiler/compiler.h" diff --git a/src/library/init_module.cpp b/src/library/init_module.cpp index 417d48099a..32a3510e5b 100644 --- a/src/library/init_module.cpp +++ b/src/library/init_module.cpp @@ -46,8 +46,6 @@ Author: Leonardo de Moura #include "library/mpq_macro.h" #include "library/arith_instance_manager.h" #include "library/inverse.h" -#include "library/simp_lemmas.h" -#include "library/eqn_lemmas.h" #include "library/pattern_attribute.h" namespace lean { @@ -100,8 +98,6 @@ void initialize_library_module() { initialize_app_builder(); initialize_fun_info(); initialize_unification_hint(); - initialize_simp_lemmas(); - initialize_eqn_lemmas(); initialize_type_context(); initialize_delayed_abstraction(); initialize_mpq_macro(); @@ -117,8 +113,6 @@ void finalize_library_module() { finalize_mpq_macro(); finalize_delayed_abstraction(); finalize_type_context(); - finalize_eqn_lemmas(); - finalize_simp_lemmas(); finalize_unification_hint(); finalize_fun_info(); finalize_app_builder(); diff --git a/src/library/tactic/CMakeLists.txt b/src/library/tactic/CMakeLists.txt index 5f01aa4928..6621e21ef5 100644 --- a/src/library/tactic/CMakeLists.txt +++ b/src/library/tactic/CMakeLists.txt @@ -6,4 +6,5 @@ add_library(tactic OBJECT occurrences.cpp kabstract.cpp tactic_state.cpp ac_tactics.cpp induction_tactic.cpp cases_tactic.cpp generalize_tactic.cpp rewrite_tactic.cpp unfold_tactic.cpp hsubstitution.cpp gexpr.cpp elaborate.cpp init_module.cpp - simp_result.cpp user_attribute.cpp eval.cpp simp_lemmas_tactics.cpp dsimplify.cpp) + simp_result.cpp user_attribute.cpp eval.cpp + simp_lemmas.cpp eqn_lemmas.cpp simp_lemmas_tactics.cpp dsimplify.cpp) diff --git a/src/library/tactic/dsimplify.h b/src/library/tactic/dsimplify.h index 1a0ec00504..51402b4aa9 100644 --- a/src/library/tactic/dsimplify.h +++ b/src/library/tactic/dsimplify.h @@ -6,7 +6,7 @@ Author: Leonardo de Moura */ #pragma once #include "library/type_context.h" -#include "library/simp_lemmas.h" +#include "library/tactic/simp_lemmas.h" namespace lean { class dsimplify_core_fn { diff --git a/src/library/eqn_lemmas.cpp b/src/library/tactic/eqn_lemmas.cpp similarity index 98% rename from src/library/eqn_lemmas.cpp rename to src/library/tactic/eqn_lemmas.cpp index 543aba7aa7..444131b1c8 100644 --- a/src/library/eqn_lemmas.cpp +++ b/src/library/tactic/eqn_lemmas.cpp @@ -8,9 +8,9 @@ Author: Leonardo de Moura #include "library/attribute_manager.h" #include "library/kernel_serializer.h" #include "library/trace.h" -#include "library/eqn_lemmas.h" #include "library/constants.h" #include "library/module.h" +#include "library/tactic/eqn_lemmas.h" namespace lean { struct eqn_lemmas_ext : public environment_extension { diff --git a/src/library/eqn_lemmas.h b/src/library/tactic/eqn_lemmas.h similarity index 92% rename from src/library/eqn_lemmas.h rename to src/library/tactic/eqn_lemmas.h index 138e2f02fc..2cb3953a2c 100644 --- a/src/library/eqn_lemmas.h +++ b/src/library/tactic/eqn_lemmas.h @@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #pragma once -#include "library/simp_lemmas.h" +#include "library/tactic/simp_lemmas.h" namespace lean { environment add_eqn_lemma(environment const & env, name const & eqn_lemma); diff --git a/src/library/tactic/init_module.cpp b/src/library/tactic/init_module.cpp index 3fdf5569c3..a84aef2540 100644 --- a/src/library/tactic/init_module.cpp +++ b/src/library/tactic/init_module.cpp @@ -28,6 +28,8 @@ Author: Leonardo de Moura #include "library/tactic/elaborate.h" #include "library/tactic/user_attribute.h" #include "library/tactic/eval.h" +#include "library/tactic/simp_lemmas.h" +#include "library/tactic/eqn_lemmas.h" #include "library/tactic/simp_lemmas_tactics.h" #include "library/tactic/dsimplify.h" #include "library/tactic/simplifier/init_module.h" @@ -61,11 +63,15 @@ void initialize_tactic_module() { initialize_elaborate(); initialize_user_attribute(); initialize_eval(); + initialize_simp_lemmas(); + initialize_eqn_lemmas(); initialize_simp_lemmas_tactics(); initialize_dsimplify(); } void finalize_tactic_module() { finalize_dsimplify(); + finalize_eqn_lemmas(); + finalize_simp_lemmas(); finalize_simp_lemmas_tactics(); finalize_eval(); finalize_user_attribute(); diff --git a/src/library/simp_lemmas.cpp b/src/library/tactic/simp_lemmas.cpp similarity index 99% rename from src/library/simp_lemmas.cpp rename to src/library/tactic/simp_lemmas.cpp index 047e5dcda5..b955564028 100644 --- a/src/library/simp_lemmas.cpp +++ b/src/library/tactic/simp_lemmas.cpp @@ -10,13 +10,13 @@ Author: Leonardo de Moura #include "kernel/instantiate.h" #include "kernel/for_each_fn.h" #include "kernel/find_fn.h" -#include "library/simp_lemmas.h" #include "library/constants.h" #include "library/trace.h" #include "library/util.h" #include "library/reducible.h" #include "library/attribute_manager.h" #include "library/relation_manager.h" +#include "library/tactic/simp_lemmas.h" namespace lean { LEAN_THREAD_VALUE(bool, g_throw_ex, false); diff --git a/src/library/simp_lemmas.h b/src/library/tactic/simp_lemmas.h similarity index 100% rename from src/library/simp_lemmas.h rename to src/library/tactic/simp_lemmas.h diff --git a/src/library/tactic/simp_lemmas_tactics.cpp b/src/library/tactic/simp_lemmas_tactics.cpp index 3ca2a4c7c7..1e28610df8 100644 --- a/src/library/tactic/simp_lemmas_tactics.cpp +++ b/src/library/tactic/simp_lemmas_tactics.cpp @@ -6,12 +6,12 @@ Author: Leonardo de Moura */ #include "library/attribute_manager.h" #include "library/trace.h" -#include "library/simp_lemmas.h" #include "library/constants.h" #include "library/vm/vm_expr.h" #include "library/vm/vm_list.h" #include "library/vm/vm_option.h" #include "library/vm/vm_name.h" +#include "library/tactic/simp_lemmas.h" #include "library/tactic/simp_result.h" #include "library/tactic/tactic_state.h" @@ -220,7 +220,7 @@ vm_obj simp_lemmas_rewrite(vm_obj const & m, vm_obj const & sls, vm_obj const & to_name(R), to_expr(e), to_tactic_state(s)); } -vm_obj simp_lemmas_drewrite_core(simp_lemmas const & sls, expr const & e, tactic_state const & s) { +vm_obj simp_lemmas_drewrite_core(transparency_mode const & m, simp_lemmas const & sls, expr const & e, tactic_state const & s) { LEAN_TACTIC_TRY; simp_lemmas_for const * sr = sls.find(get_eq_name()); if (!sr) return mk_tactic_exception("failed to apply simp_lemmas, no lemmas for 'eq' relation", s); @@ -228,7 +228,7 @@ vm_obj simp_lemmas_drewrite_core(simp_lemmas const & sls, expr const & e, tactic list const * srs = sr->find(e); if (!srs) return mk_tactic_exception("failed to apply simp_lemmas, no simp lemma", s); - type_context ctx = mk_type_context_for(s); + type_context ctx = mk_type_context_for(s, m); for (simp_lemma const & lemma : *srs) { if (lemma.is_refl()) { @@ -241,8 +241,8 @@ vm_obj simp_lemmas_drewrite_core(simp_lemmas const & sls, expr const & e, tactic LEAN_TACTIC_CATCH(s); } -vm_obj simp_lemmas_drewrite(vm_obj const & sls, vm_obj const & e, vm_obj const & s) { - return simp_lemmas_drewrite_core(to_simp_lemmas(sls), to_expr(e), to_tactic_state(s)); +vm_obj simp_lemmas_drewrite(vm_obj const & m, vm_obj const & sls, vm_obj const & e, vm_obj const & s) { + return simp_lemmas_drewrite_core(to_transparency_mode(m), to_simp_lemmas(sls), to_expr(e), to_tactic_state(s)); } void initialize_simp_lemmas_tactics() { @@ -254,7 +254,7 @@ void initialize_simp_lemmas_tactics() { DECLARE_VM_BUILTIN(name({"simp_lemmas", "add_simp_core"}), simp_lemmas_add_simp); DECLARE_VM_BUILTIN(name({"simp_lemmas", "add_congr_core"}), simp_lemmas_add_congr); DECLARE_VM_BUILTIN(name({"simp_lemmas", "rewrite_core"}), simp_lemmas_rewrite); - DECLARE_VM_BUILTIN(name({"simp_lemmas", "drewrite"}), simp_lemmas_drewrite); + DECLARE_VM_BUILTIN(name({"simp_lemmas", "drewrite_core"}), simp_lemmas_drewrite); } void finalize_simp_lemmas_tactics() { diff --git a/src/library/tactic/simp_lemmas_tactics.h b/src/library/tactic/simp_lemmas_tactics.h index 6715c47f0e..25c056b43e 100644 --- a/src/library/tactic/simp_lemmas_tactics.h +++ b/src/library/tactic/simp_lemmas_tactics.h @@ -5,8 +5,8 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #pragma once -#include "library/simp_lemmas.h" #include "library/vm/vm.h" +#include "library/tactic/simp_lemmas.h" namespace lean { simp_lemmas const & to_simp_lemmas(vm_obj const & o); vm_obj to_obj(simp_lemmas const & s); diff --git a/src/library/tactic/simplifier/simplifier.cpp b/src/library/tactic/simplifier/simplifier.cpp index fdbf484e29..d97d55c1da 100644 --- a/src/library/tactic/simplifier/simplifier.cpp +++ b/src/library/tactic/simplifier/simplifier.cpp @@ -28,7 +28,6 @@ Author: Daniel Selsam #include "library/relation_manager.h" #include "library/app_builder.h" #include "library/congr_lemma.h" -#include "library/simp_lemmas.h" #include "library/fun_info.h" #include "library/vm/vm_expr.h" #include "library/vm/vm_list.h" @@ -36,6 +35,7 @@ Author: Daniel Selsam #include "library/tactic/tactic_state.h" #include "library/tactic/ac_tactics.h" #include "library/tactic/app_builder_tactics.h" +#include "library/tactic/simp_lemmas.h" #include "library/tactic/simp_lemmas_tactics.h" #include "library/tactic/simplifier/simplifier.h" #include "library/tactic/simplifier/theory_simplifier.h" diff --git a/src/library/tactic/simplifier/simplifier.h b/src/library/tactic/simplifier/simplifier.h index 710b3a6abc..db55b1254e 100644 --- a/src/library/tactic/simplifier/simplifier.h +++ b/src/library/tactic/simplifier/simplifier.h @@ -6,8 +6,8 @@ Author: Daniel Selsam #pragma once #include "kernel/expr_pair.h" #include "library/type_context.h" -#include "library/simp_lemmas.h" #include "library/vm/vm.h" +#include "library/tactic/simp_lemmas.h" #include "library/tactic/simp_result.h" namespace lean { diff --git a/src/library/tactic/unfold_tactic.cpp b/src/library/tactic/unfold_tactic.cpp index aa8b8729e5..8ff4bd1c0d 100644 --- a/src/library/tactic/unfold_tactic.cpp +++ b/src/library/tactic/unfold_tactic.cpp @@ -14,9 +14,9 @@ Author: Leonardo de Moura #include "library/replace_visitor.h" #include "library/constants.h" #include "library/user_recursors.h" -#include "library/eqn_lemmas.h" #include "library/vm/vm_list.h" #include "library/vm/vm_expr.h" +#include "library/tactic/eqn_lemmas.h" #include "library/tactic/tactic_state.h" #include "library/tactic/occurrences.h"