fix(library/tactic/rewrite_tactic): apply beta reduction when selecting patterns

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

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

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