From 88975927e65aa19a988d81f9a0df24e6b5793343 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 24 May 2015 18:54:28 -0700
Subject: [PATCH] fix(library/tactic/relation_tactics): beta-reduce goal before
 trying to extract head symbol

---
 library/data/stream.lean                | 23 +++++++++++------------
 src/library/tactic/relation_tactics.cpp |  3 ++-
 tests/lean/run/refl_beta.lean           | 13 +++++++++++++
 tests/lean/run/rewrite_with_beta.lean   |  2 +-
 4 files changed, 27 insertions(+), 14 deletions(-)
 create mode 100644 tests/lean/run/refl_beta.lean

diff --git a/library/data/stream.lean b/library/data/stream.lean
index 0c083f955..f7c3ef4a5 100644
--- a/library/data/stream.lean
+++ b/library/data/stream.lean
@@ -84,7 +84,7 @@ exists.intro 0 rfl
 
 theorem mem_cons_of_mem {a : A} {s : stream A} (b : A) : a ∈ s → a ∈ b :: s :=
 assume ains, obtain n (h : a = nth n s), from ains,
-exists.intro (succ n) (by rewrite [nth_succ, tail_cons, h]; esimp)
+exists.intro (succ n) (by rewrite [nth_succ, tail_cons, h])
 
 theorem eq_or_mem_of_mem_cons {a b : A} {s : stream A} : a ∈ b::s → a = b ∨ a ∈ s :=
 assume ainbs, obtain n (h : a = nth n (b::s)), from ainbs,
@@ -129,7 +129,7 @@ rfl
 
 theorem mem_map {a : A} {s : stream A} : a ∈ s → f a ∈ map f s :=
 assume ains, obtain n (h : a = nth n s), from ains,
-exists.intro n (by rewrite [nth_map, h]; esimp)
+exists.intro n (by rewrite [nth_map, h])
 end map
 
 section zip
@@ -330,12 +330,12 @@ theorem nth_interleave_right : ∀ (n : nat) (s₁ s₂ : stream A), nth (2*n+1)
   end
 
 theorem mem_interleave_left {a : A} {s₁ : stream A} (s₂ : stream A) : a ∈ s₁ → a ∈ s₁ ⋈ s₂ :=
-assume ains₁, obtain n (h : a = nth n s₁), from ains₁,
-exists.intro (2*n) (by rewrite [h, nth_interleave_left]; esimp)
+assume ains₁, obtain n h, from ains₁,
+exists.intro (2*n) (by rewrite [h, nth_interleave_left])
 
 theorem mem_interleave_right {a : A} {s₁ : stream A} (s₂ : stream A) : a ∈ s₂ → a ∈ s₁ ⋈ s₂ :=
-assume ains₂, obtain n (h : a = nth n s₂), from ains₂,
-exists.intro (2*n+1) (by rewrite [h, nth_interleave_right]; esimp)
+assume ains₂, obtain n h, from ains₂,
+exists.intro (2*n+1) (by rewrite [h, nth_interleave_right])
 
 definition even (s : stream A) : stream A :=
 corec
@@ -371,8 +371,7 @@ eq_of_bisim
       constructor,
        {reflexivity},
        {existsi (tail s₂),
-        rewrite [interleave_eq, even_cons_cons, tail_cons],
-        apply rfl}
+        rewrite [interleave_eq, even_cons_cons, tail_cons]}
     end)
   (exists.intro s₂ rfl)
 
@@ -399,12 +398,12 @@ theorem nth_odd : ∀ (n : nat) (s : stream A), nth n (odd s) = nth (2*n + 1) s
 λ n s, by rewrite [odd_eq, nth_even]
 
 theorem mem_of_mem_even (a : A) (s : stream A) : a ∈ even s → a ∈ s :=
-assume aines, obtain n (h : a = nth n (even s)), from aines,
-exists.intro (2*n) (by rewrite [h, nth_even]; esimp)
+assume aines, obtain n h, from aines,
+exists.intro (2*n) (by rewrite [h, nth_even])
 
 theorem mem_of_mem_odd (a : A) (s : stream A) : a ∈ odd s → a ∈ s :=
-assume ainos, obtain n (h : a = nth n (odd s)), from ainos,
-exists.intro (2*n+1) (by rewrite [h, nth_odd]; esimp)
+assume ainos, obtain n h, from ainos,
+exists.intro (2*n+1) (by rewrite [h, nth_odd])
 
 open list
 definition append : list A → stream A → stream A
diff --git a/src/library/tactic/relation_tactics.cpp b/src/library/tactic/relation_tactics.cpp
index 39d7476e4..2e2cca801 100644
--- a/src/library/tactic/relation_tactics.cpp
+++ b/src/library/tactic/relation_tactics.cpp
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
+#include "kernel/instantiate.h"
 #include "library/relation_manager.h"
 #include "library/explicit.h"
 #include "library/placeholder.h"
@@ -21,7 +22,7 @@ static optional<name> get_goal_op(proof_state const & s, bool no_meta = false) {
     goal const & g   = head(gs);
     if (no_meta && has_metavar(g.get_type()))
         return optional<name>();
-    expr const & op  = get_app_fn(g.get_type());
+    expr op  = get_app_fn(head_beta_reduce(g.get_type()));
     if (is_constant(op))
         return optional<name>(const_name(op));
     else
diff --git a/tests/lean/run/refl_beta.lean b/tests/lean/run/refl_beta.lean
new file mode 100644
index 000000000..aafb895b8
--- /dev/null
+++ b/tests/lean/run/refl_beta.lean
@@ -0,0 +1,13 @@
+import data.stream
+open nat
+
+namespace stream
+variable A : Type
+
+set_option pp.beta false
+
+theorem mem_of_mem_odd₂ (a : A) (s : stream A) : a ∈ odd s → a ∈ s :=
+assume ainos, obtain n (h : a = nth n (odd s)), from ainos,
+exists.intro (2*n+1) (by rewrite [h, nth_odd])
+
+end stream
diff --git a/tests/lean/run/rewrite_with_beta.lean b/tests/lean/run/rewrite_with_beta.lean
index 4a04ce679..b64f34981 100644
--- a/tests/lean/run/rewrite_with_beta.lean
+++ b/tests/lean/run/rewrite_with_beta.lean
@@ -6,6 +6,6 @@ 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
+exists.intro (succ n) begin rewrite [nth_succ, tail_cons, h] end
 
 end stream