From bf71d9f342f6166838eb1728b794f83c6de8282b Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 17 Jun 2015 18:37:53 -0700
Subject: [PATCH] fix(library/tactic/rewrite_tactic): fixes #682

---
 src/library/tactic/rewrite_tactic.cpp | 16 +++++++++++++---
 tests/lean/run/682.lean               | 15 +++++++++++++++
 2 files changed, 28 insertions(+), 3 deletions(-)
 create mode 100644 tests/lean/run/682.lean

diff --git a/src/library/tactic/rewrite_tactic.cpp b/src/library/tactic/rewrite_tactic.cpp
index 36ef80833..566c00644 100644
--- a/src/library/tactic/rewrite_tactic.cpp
+++ b/src/library/tactic/rewrite_tactic.cpp
@@ -659,11 +659,20 @@ class rewrite_fn {
     void replace_hypothesis(expr const & hyp, expr const & new_hyp_type) {
         expr new_hyp = update_mlocal(hyp, new_hyp_type);
         buffer<expr> new_hyps;
+        buffer<expr> old_locals;
+        buffer<expr> new_locals;
         m_g.get_hyps(new_hyps);
         for (expr & h : new_hyps) {
             if (mlocal_name(h) == mlocal_name(hyp)) {
+                old_locals.push_back(h);
+                new_locals.push_back(new_hyp);
                 h = new_hyp;
-                break;
+            } else if (depends_on_any(mlocal_type(h), old_locals.size(), old_locals.data())) {
+                expr new_h_type = replace_locals(mlocal_type(h), old_locals.size(), old_locals.data(), new_locals.data());
+                expr new_h      = update_mlocal(h, new_h_type);
+                old_locals.push_back(h);
+                new_locals.push_back(new_h);
+                h = new_h;
             }
         }
         expr new_type = m_g.get_type();
@@ -674,7 +683,8 @@ class rewrite_fn {
         update_goal(new_g);
     }
 
-    bool process_reduce_hypothesis(expr const & hyp, list<name> const & to_unfold) {
+    bool process_reduce_hypothesis(name const & hyp_internal_name, list<name> const & to_unfold) {
+        expr hyp = m_g.find_hyp_from_internal_name(hyp_internal_name)->first;
         if (auto new_hyp_type = reduce(mlocal_type(hyp), to_unfold)) {
             replace_hypothesis(hyp, *new_hyp_type);
             return true;
@@ -692,7 +702,7 @@ class rewrite_fn {
         for (expr const & h : hyps) {
             if (!loc.includes_hypothesis(local_pp_name(h)))
                 continue;
-            if (process_reduce_hypothesis(h, to_unfold))
+            if (process_reduce_hypothesis(mlocal_name(h), to_unfold))
                 progress = true;
         }
         if (loc.includes_goal()) {
diff --git a/tests/lean/run/682.lean b/tests/lean/run/682.lean
new file mode 100644
index 000000000..7ee337bfa
--- /dev/null
+++ b/tests/lean/run/682.lean
@@ -0,0 +1,15 @@
+import data.vector
+open nat prod.ops
+
+example (n : nat) (v₁ : vector nat n) (v₂ : vector nat 0) (h₁ : (v₂, n).2 = 0) (h₂ : n = 0) (h₃ : eq.rec_on h₁ v₁ = v₂) : v₂ = eq.rec_on h₂ v₁ :=
+begin
+  esimp at h₁,
+  esimp at h₃,
+  subst h₃
+end
+
+example (n : nat) (v₁ : vector nat n) (v₂ : vector nat 0) (h₁ : (v₂, n).2 = 0) (h₂ : n = 0) (h₃ : eq.rec_on h₁ v₁ = v₂) : v₂ = eq.rec_on h₂ v₁ :=
+begin
+  esimp at *,
+  subst h₃
+end