feat(library/tactic): use occurrence object in unfold tactic family

library/data/nat/examples/fib.lean

@@ -25,15 +25,12 @@ definition fib_fast (n : nat) := (fib_fast_aux n).2
 
 -- We now prove that fib_fast and fib are equal
 
-lemma fib_fast_aux_succ_succ : ∀ n, fib_fast_aux (succ (succ n)) = match fib_fast_aux (succ n) with | (fn, fn1) := (fn1, fn1 + fn) end :=
-λ n, rfl
-
 lemma fib_fast_aux_lemma : ∀ n, (fib_fast_aux (succ n)).1 = (fib_fast_aux n).2
 | 0               := rfl
 | 1               := rfl
 | (succ (succ n)) :=
   begin
-    rewrite [fib_fast_aux_succ_succ],
+    unfold fib_fast_aux at {1},
     rewrite [-prod.eta (fib_fast_aux _)],
   end
 

library/data/nat/examples/fib2.lean

@@ -17,16 +17,13 @@ private definition fib_fast_aux : nat → nat → nat → nat
 | 0     i j := j
 | (n+1) i j := fib_fast_aux n j (j+i)
 
-lemma fib_fast_aux_succ : ∀ n i j, fib_fast_aux (succ n) i j = fib_fast_aux n j (j+i) :=
-λ n i j, rfl
-
 lemma fib_fast_aux_lemma : ∀ n m, fib_fast_aux n (fib m) (fib (succ m)) = fib (succ (n + m))
 | 0        m := by rewrite zero_add
 | (succ n) m :=
   begin
     have ih : fib_fast_aux n (fib (succ m)) (fib (succ (succ m))) = fib (succ (n + succ m)), from fib_fast_aux_lemma n (succ m),
     have h₁ : fib (succ m) + fib m = fib (succ (succ m)), from rfl,
-    rewrite [fib_fast_aux_succ, h₁, ih, succ_add, add_succ],
+    unfold fib_fast_aux, rewrite [h₁, ih, succ_add, add_succ]
   end
 
 definition fib_fast (n: nat) :=
@@ -37,5 +34,5 @@ lemma fib_fast_eq_fib : ∀ n, fib_fast n = fib n
 | (succ n) :=
   begin
     have h₁ : fib_fast_aux n (fib 0) (fib 1) = fib (succ n), from !fib_fast_aux_lemma,
-    unfold fib_fast, krewrite [fib_fast_aux_succ, h₁]
+    unfold fib_fast, unfold fib_fast_aux, krewrite h₁
   end

src/library/tactic/rewrite_tactic.cpp

@@ -628,13 +628,15 @@ class rewrite_fn {
         }
     };
 
-    optional<expr> reduce(expr const & e, list<name> const & to_unfold, bool force_unfold) {
+    optional<expr> reduce(expr const & e, list<name> const & to_unfold, optional<occurrence> const & occs, bool force_unfold) {
+        lean_assert(is_nil(to_unfold) == !occs);
         constraint_seq cs;
         bool unfolded = !to_unfold;
         bool use_eta  = true;
         // TODO(Leo): should we add add an option that will not try to fold recursive applications
         if (to_unfold) {
-            auto new_e = unfold_rec(m_env, m_ngen.mk_child(), force_unfold, e, to_unfold);
+            lean_assert(occs);
+            auto new_e = unfold_rec(m_env, m_ngen.mk_child(), force_unfold, e, to_unfold, *occs);
             if (!new_e)
                 return none_expr();
             type_checker_ptr tc(new type_checker(m_env, m_ngen.mk_child(),
@@ -662,8 +664,8 @@ class rewrite_fn {
         update_goal(new_g);
     }
 
-    bool process_reduce_goal(list<name> const & to_unfold, bool force_unfold) {
-        if (auto new_type = reduce(m_g.get_type(), to_unfold, force_unfold)) {
+    bool process_reduce_goal(list<name> const & to_unfold, optional<occurrence> const & occ, bool force_unfold) {
+        if (auto new_type = reduce(m_g.get_type(), to_unfold, occ, force_unfold)) {
             replace_goal(*new_type);
             return true;
         } else {
@@ -699,9 +701,9 @@ class rewrite_fn {
         update_goal(new_g);
     }
 
-    bool process_reduce_hypothesis(name const & hyp_internal_name, list<name> const & to_unfold, bool force_unfold) {
+    bool process_reduce_hypothesis(name const & hyp_internal_name, list<name> const & to_unfold, optional<occurrence> const & occs, bool force_unfold) {
         expr hyp = m_g.find_hyp_from_internal_name(hyp_internal_name)->first;
-        if (auto new_hyp_type = reduce(mlocal_type(hyp), to_unfold, force_unfold)) {
+        if (auto new_hyp_type = reduce(mlocal_type(hyp), to_unfold, occs, force_unfold)) {
             replace_hypothesis(hyp, *new_hyp_type);
             return true;
         } else {
@@ -711,18 +713,19 @@ class rewrite_fn {
 
     bool process_reduce_step(list<name> const & to_unfold, bool force_unfold, location const & loc) {
         if (loc.is_goal_only())
-            return process_reduce_goal(to_unfold, force_unfold);
+            return process_reduce_goal(to_unfold, loc.includes_goal(), force_unfold);
         bool progress = false;
         buffer<expr> hyps;
         m_g.get_hyps(hyps);
         for (expr const & h : hyps) {
-            if (!loc.includes_hypothesis(local_pp_name(h)))
+            auto occs = loc.includes_hypothesis(local_pp_name(h));
+            if (!occs)
                 continue;
-            if (process_reduce_hypothesis(mlocal_name(h), to_unfold, force_unfold))
+            if (process_reduce_hypothesis(mlocal_name(h), to_unfold, occs, force_unfold))
                 progress = true;
         }
-        if (loc.includes_goal()) {
-            if (process_reduce_goal(to_unfold, force_unfold))
+        if (auto occs = loc.includes_goal()) {
+            if (process_reduce_goal(to_unfold, occs, force_unfold))
                 progress = true;
         }
         return progress;
@@ -962,7 +965,7 @@ class rewrite_fn {
 
     expr reduce_rule_type(expr const & e) {
         if (m_apply_reduce) {
-            if (auto it = reduce(e, list<name>(), false))
+            if (auto it = reduce(e, list<name>(), optional<occurrence>(), false))
                 return *it;
             else // TODO(Leo): we should fail instead of doing trying again
                 return head_beta_reduce(e);

src/library/tactic/unfold_rec.cpp

@@ -11,6 +11,7 @@ Author: Leonardo de Moura
 #include "library/util.h"
 #include "library/replace_visitor.h"
 #include "library/constants.h"
+#include "library/tactic/location.h"
 
 extern void pp_detail(lean::environment const & env, lean::expr const & e);
 extern void pp(lean::environment const & env, lean::expr const & e);
@@ -50,6 +51,8 @@ class unfold_rec_fn : public replace_visitor_aux {
     type_checker_ptr    m_tc;
     type_checker_ptr    m_norm_decl_tc;
     list<name>          m_to_unfold;
+    occurrence          m_occs;
+    unsigned            m_occ_idx;
 
     virtual name mk_fresh_name() { return m_ngen.next(); }
 
@@ -292,7 +295,12 @@ class unfold_rec_fn : public replace_visitor_aux {
     }
 
     bool unfold_cnst(expr const & e) {
-        return is_constant(e) && std::find(m_to_unfold.begin(), m_to_unfold.end(), const_name(e)) != m_to_unfold.end();
+        if (!is_constant(e))
+            return false;
+        if (std::find(m_to_unfold.begin(), m_to_unfold.end(), const_name(e)) == m_to_unfold.end())
+            return false;
+        m_occ_idx++;
+        return m_occs.contains(m_occ_idx);
     }
 
     virtual expr visit_app(expr const & e) {
@@ -329,23 +337,28 @@ class unfold_rec_fn : public replace_visitor_aux {
     }
 
 public:
-    unfold_rec_fn(environment const & env, name_generator && ngen, bool force_unfold, list<name> const & to_unfold):
+    unfold_rec_fn(environment const & env, name_generator && ngen, bool force_unfold, list<name> const & to_unfold,
+                  occurrence const & occs):
         m_env(env),
         m_ngen(ngen),
         m_force_unfold(force_unfold),
         m_tc(mk_type_checker(m_env, m_ngen.mk_child(), [](name const &) { return false; })),
         m_norm_decl_tc(mk_type_checker(m_env, m_ngen.mk_child(), [](name const & n) { return !is_rec_building_part(n); })),
-        m_to_unfold(to_unfold)
+        m_to_unfold(to_unfold),
+        m_occs(occs),
+        m_occ_idx(0)
         {}
 
     expr operator()(expr const & e) {
+        m_occ_idx = 0;
         return replace_visitor_aux::operator()(e);
     }
 };
 
-optional<expr> unfold_rec(environment const & env, name_generator && ngen, bool force_unfold, expr const & e, list<name> const & to_unfold) {
+optional<expr> unfold_rec(environment const & env, name_generator && ngen, bool force_unfold, expr const & e, list<name> const & to_unfold,
+                          occurrence const & occs) {
     try {
-        expr r = unfold_rec_fn(env, std::move(ngen), force_unfold, to_unfold)(e);
+        expr r = unfold_rec_fn(env, std::move(ngen), force_unfold, to_unfold, occs)(e);
         if (r == e)
             return none_expr();
         return some_expr(r);

src/library/tactic/unfold_rec.h

@@ -6,6 +6,9 @@ Author: Leonardo de Moura
 */
 #pragma once
 #include "kernel/environment.h"
+#include "library/tactic/location.h"
+
 namespace lean {
-optional<expr> unfold_rec(environment const & env, name_generator && ngen, bool force_unfold, expr const & e, list<name> const & to_unfold);
+optional<expr> unfold_rec(environment const & env, name_generator && ngen, bool force_unfold, expr const & e,
+                          list<name> const & to_unfold, occurrence const & occs);
 }

tests/lean/run/unfold_test.lean

@@ -0,0 +1,39 @@
+import data.list data.vector
+
+variables {A B : Type}
+
+section
+open list
+theorem last_concat {x : A} : ∀ {l : list A} (h : concat x l ≠ []), last (concat x l) h = x
+| []          h := rfl
+| [a]         h := rfl
+| (a₁::a₂::l) h :=
+  by xrewrite [↑concat, ↑concat, last_cons_cons, ↓concat x (a₂::l), last_concat]
+
+theorem reverse_append : ∀ (s t : list A), reverse (s ++ t) = (reverse t) ++ (reverse s)
+| []         t2 :=
+  by rewrite [↑append, ↑reverse, append_nil_right]
+| (a2 :: s2) t2 :=
+  by rewrite [↑append, ↑reverse, reverse_append, concat_eq_append, append.assoc, -concat_eq_append]
+end
+
+section
+open vector nat prod
+
+theorem unzip_zip : ∀ {n : nat} (v₁ : vector A n) (v₂ : vector B n), unzip (zip v₁ v₂) = (v₁, v₂)
+| 0     []      []      := rfl
+| (n+1) (a::va) (b::vb) := by rewrite [↑zip, ↑unzip, unzip_zip]
+
+theorem zip_unzip : ∀ {n : nat} (v : vector (A × B) n), zip (pr₁ (unzip v)) (pr₂ (unzip v)) = v
+| 0     []             := rfl
+| (n+1) ((a, b) :: v)  := by rewrite [↑unzip,↑zip,zip_unzip]
+
+theorem reverse_concat : Π {n : nat} (xs : vector A n) (a : A), reverse (concat xs a) = a :: reverse xs
+| 0     []         a := rfl
+| (n+1) (x :: xs)  a := by xrewrite [↑concat,↑reverse,reverse_concat]
+
+theorem reverse_reverse : Π {n : nat} (xs : vector A n), reverse (reverse xs) = xs
+| 0        []        := rfl
+| (succ n) (x :: xs) := by rewrite [↑reverse at {1}, reverse_concat, reverse_reverse]
+
+end