From 9dc0388022c012e61fb2f0cbe555630330efc02c Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 1 May 2015 19:45:23 -0700
Subject: [PATCH] fix(library/tactic/rewrite_tactic): bug when rewriting
 hypotheses

---
 src/library/locals.cpp                |  8 ++++++--
 src/library/locals.h                  |  6 +++++-
 src/library/tactic/rewrite_tactic.cpp |  2 +-
 tests/lean/run/rw_bug2.lean           | 13 +++++++++++++
 4 files changed, 25 insertions(+), 4 deletions(-)
 create mode 100644 tests/lean/run/rw_bug2.lean

diff --git a/src/library/locals.cpp b/src/library/locals.cpp
index 6821abcc3..d5e155c1a 100644
--- a/src/library/locals.cpp
+++ b/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;
         });
 }
diff --git a/src/library/locals.h b/src/library/locals.h
index e985778c0..b0d1f8910 100644
--- a/src/library/locals.h
+++ b/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 */
diff --git a/src/library/tactic/rewrite_tactic.cpp b/src/library/tactic/rewrite_tactic.cpp
index 152d30290..b2a0cc8fc 100644
--- a/src/library/tactic/rewrite_tactic.cpp
+++ b/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.
diff --git a/tests/lean/run/rw_bug2.lean b/tests/lean/run/rw_bug2.lean
new file mode 100644
index 000000000..077694fc8
--- /dev/null
+++ b/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₁