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

@@ -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.

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"

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"

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)

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 {

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

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"
 

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"

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();

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)

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 {

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 {

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);

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();

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);

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<simp_lemma> 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() {

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);

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"

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 {

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"