From 004ea80e65a2ce877319b00fccf3c4b83bcd3182 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 24 May 2015 18:44:30 -0700
Subject: [PATCH] fix(library/tactic/rewrite_tactic): apply beta reduction when
 selecting patterns

---
 src/kernel/instantiate.cpp            |  2 +-
 src/library/tactic/rewrite_tactic.cpp |  2 ++
 tests/lean/run/rewrite_with_beta.lean | 11 +++++++++++
 3 files changed, 14 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/run/rewrite_with_beta.lean

diff --git a/src/kernel/instantiate.cpp b/src/kernel/instantiate.cpp
index 9a4f80db1..3991aefec 100644
--- a/src/kernel/instantiate.cpp
+++ b/src/kernel/instantiate.cpp
@@ -117,7 +117,7 @@ expr head_beta_reduce(expr const & t) {
         buffer<expr> args;
         expr const & f = get_app_rev_args(t, args);
         lean_assert(is_lambda(f));
-        return apply_beta(f, args.size(), args.data());
+        return head_beta_reduce(apply_beta(f, args.size(), args.data()));
     }
 }
 
diff --git a/src/library/tactic/rewrite_tactic.cpp b/src/library/tactic/rewrite_tactic.cpp
index 2ab9f5c10..f5e8a3559 100644
--- a/src/library/tactic/rewrite_tactic.cpp
+++ b/src/library/tactic/rewrite_tactic.cpp
@@ -918,6 +918,7 @@ class rewrite_fn {
                 rule_type     = instantiate(binding_body(rule_type), meta);
                 new_rule_type = m_relaxed_tc->whnf(rule_type).first;
             }
+            rule_type = head_beta_reduce(rule_type);
             if (is_standard(m_env)) {
                 if (!is_eq(rule_type) && !is_iff(rule_type))
                     throw_rewrite_exception("invalid rewrite tactic, given lemma is not an equality or iff");
@@ -1122,6 +1123,7 @@ class rewrite_fn {
                 new_rule_type = m_relaxed_tc->whnf(rule_type , cs_seq);
                 rule       = mk_app(rule, meta);
             }
+            rule_type = head_beta_reduce(rule_type);
             lean_assert(is_eq(rule_type) || (is_standard(m_env) && is_iff(rule_type)));
             if (is_standard(m_env) && is_iff(rule_type)) {
                 rule      = apply_propext(rule, rule_type);
diff --git a/tests/lean/run/rewrite_with_beta.lean b/tests/lean/run/rewrite_with_beta.lean
new file mode 100644
index 000000000..4a04ce679
--- /dev/null
+++ b/tests/lean/run/rewrite_with_beta.lean
@@ -0,0 +1,11 @@
+import data.stream
+open nat
+
+namespace stream
+variable A : Type
+
+theorem mem_cons_of_mem₂ {a : A} {s : stream A} (b : A) : a ∈ s → a ∈ b :: s :=
+assume ains, obtain n h, from ains,
+exists.intro (succ n) begin rewrite [nth_succ, tail_cons, h], esimp end
+
+end stream