From b3707ab54af4db9c010de47f65fc6431705e5970 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 29 Jul 2015 17:11:46 -0700
Subject: [PATCH] feat(library/tactic/unfold_rec): fixes #753

---
 src/library/tactic/unfold_rec.cpp        | 9 +++++++--
 tests/lean/unfold_rec4.lean              | 8 ++++++++
 tests/lean/unfold_rec4.lean.expected.out | 6 ++++++
 3 files changed, 21 insertions(+), 2 deletions(-)
 create mode 100644 tests/lean/unfold_rec4.lean
 create mode 100644 tests/lean/unfold_rec4.lean.expected.out

diff --git a/src/library/tactic/unfold_rec.cpp b/src/library/tactic/unfold_rec.cpp
index b9410372f..a39ee964a 100644
--- a/src/library/tactic/unfold_rec.cpp
+++ b/src/library/tactic/unfold_rec.cpp
@@ -275,8 +275,13 @@ class unfold_rec_fn : public replace_visitor_aux {
         virtual expr visit_app(expr const & e) {
             buffer<expr> args;
             expr fn = get_app_args(e, args);
-            if (m_kind == REC && is_constant(fn) && const_name(fn) == m_rec_name)
-                return fold_rec(e, args);
+            if (m_kind == REC && is_constant(fn) && const_name(fn) == m_rec_name) {
+                expr new_e = m_tc->whnf(e).first;
+                if (new_e != e)
+                    return visit_app(new_e);
+                else
+                    return fold_rec(e, args);
+            }
             if (m_kind == BREC && is_constant(fn) && const_name(fn) == get_prod_pr1_name() && args.size() >= 3) {
                 expr rec_fn = get_app_fn(args[1]);
                 if (is_constant(rec_fn) && const_name(rec_fn) == m_rec_name)
diff --git a/tests/lean/unfold_rec4.lean b/tests/lean/unfold_rec4.lean
new file mode 100644
index 000000000..509c56cab
--- /dev/null
+++ b/tests/lean/unfold_rec4.lean
@@ -0,0 +1,8 @@
+open nat
+definition f [unfold 1] (n : ℕ) : ℕ :=
+by induction n with n fn; exact zero; exact succ (succ fn)
+
+example (n : ℕ) : f (succ (succ n)) = sorry :=
+begin
+  unfold f,
+end
diff --git a/tests/lean/unfold_rec4.lean.expected.out b/tests/lean/unfold_rec4.lean.expected.out
new file mode 100644
index 000000000..85cb3ad5b
--- /dev/null
+++ b/tests/lean/unfold_rec4.lean.expected.out
@@ -0,0 +1,6 @@
+unfold_rec4.lean:8:0: error: 1 unsolved subgoal
+n : ℕ
+⊢ succ (succ (succ (succ (f n)))) = sorry
+unfold_rec4.lean:8:0: error: failed to add declaration 'example' to environment, value has metavariables
+remark: set 'formatter.hide_full_terms' to false to see the complete term
+  ?M_1