fix(library/tactic/rewrite_tactic): bug when rewriting hypotheses

src/library/locals.cpp

@@ -49,14 +49,18 @@ level_param_names to_level_param_names(name_set const & ls) {
     return r;
 }
 
-void collect_locals(expr const & e, expr_struct_set & ls) {
+void collect_locals(expr const & e, expr_struct_set & ls, bool restricted) {
     if (!has_local(e))
         return;
     for_each(e, [&](expr const & e, unsigned) {
             if (!has_local(e))
                 return false;
-            if (is_local(e))
+            if (is_local(e)) {
                 ls.insert(e);
+                return !restricted; // search type if not restricted
+            }
+            if (is_meta(e))
+                return !restricted; // search type if not restricted
             return true;
         });
 }

src/library/locals.h

@@ -11,7 +11,11 @@ Author: Leonardo de Moura
 namespace lean {
 void collect_univ_params_core(level const & l, name_set & r);
 name_set collect_univ_params(expr const & e, name_set const & ls = name_set());
-void collect_locals(expr const & e, expr_struct_set & ls);
+/**
+  \remark If restricted is true, then locals in meta-variable applications and local constants
+  are ignored.
+*/
+void collect_locals(expr const & e, expr_struct_set & ls, bool restricted = false);
 level_param_names to_level_param_names(name_set const & ls);
 
 /** \brief Return true iff \c [begin_locals, end_locals) contains \c local */

src/library/tactic/rewrite_tactic.cpp

@@ -1288,7 +1288,7 @@ class rewrite_fn {
         if (loc.is_goal_only())
             return process_rewrite_goal(orig_elem, pattern, *loc.includes_goal());
         expr_struct_set used_hyps;
-        collect_locals(elem, used_hyps);
+        collect_locals(elem, used_hyps, true);
         // We collect hypotheses used in the rewrite step. They are not rewritten.
         // That is, we don't use them to rewrite themselves.
         // We need to do that to avoid the problem described on issue #548.

tests/lean/run/rw_bug2.lean

@@ -0,0 +1,13 @@
+import logic.eq
+open prod
+
+definition swap {A : Type} : A × A → A × A
+| (a, b) := (b, a)
+
+theorem swap_swap {A : Type} : ∀ p : A × A, swap (swap p) = p
+| (a, b) := rfl
+
+theorem eq_of_swap_eq {A : Type} : ∀ p₁ p₂ : A × A, swap p₁ = swap p₂ → p₁ = p₂ :=
+take p₁ p₂, assume seqs,
+assert h₁ : swap (swap p₁) = swap (swap p₂), from congr_arg swap seqs,
+by rewrite *swap_swap at h₁; exact h₁