feat(library/tactic/unfold_rec): fixes #753

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)

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

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