fix(library/tactic/unfold_tactic): should use type_context locals

library/init/meta/unfold_tactic.lean

@@ -14,7 +14,10 @@ meta_definition unfold_core (force : bool) (occs : occurrences) (ns : list name)
 target >>= unfold_expr_core force occs ns >>= change
 
 meta_definition unfold : list name → tactic unit :=
-unfold_core tt occurrences.all
+unfold_core ff occurrences.all
+
+meta_definition unfold_occs_of (occs : list nat) (c : name) : tactic unit :=
+unfold_core ff (occurrences.pos occs) [c]
 
 meta_definition unfold_core_at (force : bool) (occs : occurrences) (ns : list name) (H : expr) : tactic unit :=
 do num_reverted : ℕ ← revert H,
@@ -24,6 +27,6 @@ do num_reverted : ℕ ← revert H,
    intron num_reverted
 
 meta_definition unfold_at : list name → expr → tactic unit :=
-unfold_core_at tt occurrences.all
+unfold_core_at ff occurrences.all
 
 end tactic

src/library/tactic/unfold_tactic.cpp

@@ -180,24 +180,6 @@ class unfold_rec_fn : public replace_visitor_aux {
         }
     }
 
-    expr whnf_rec(expr const & e) {
-        return m_ctx.whnf_pred(e, [&](expr const & c) { return is_rec_building_part(const_name(get_app_fn(c))); });
-    }
-
-    expr get_fn_decl(expr const & fn, buffer<expr> & locals) {
-        lean_assert(is_constant(fn));
-        declaration decl = m_env.get(const_name(fn));
-        if (length(const_levels(fn)) != decl.get_num_univ_params())
-            throw_ill_formed();
-        expr fn_body     = instantiate_value_univ_params(decl, const_levels(fn));
-        while (is_lambda(fn_body)) {
-            expr local = mk_local(mk_fresh_name(), binding_domain(fn_body));
-            locals.push_back(local);
-            fn_body    = instantiate(binding_body(fn_body), local);
-        }
-        return whnf_rec(fn_body);
-    }
-
     struct fold_failed {};
 
     struct fold_rec_fn : public replace_visitor_aux {
@@ -302,8 +284,25 @@ class unfold_rec_fn : public replace_visitor_aux {
         }
     };
 
+    expr whnf_rec(expr const & e) {
+        return m_ctx.whnf_pred(e, [&](expr const & c) { return is_rec_building_part(const_name(get_app_fn(c))); });
+    }
+
+    expr get_fn_decl(expr const & fn, type_context::tmp_locals & locals) {
+        lean_assert(is_constant(fn));
+        declaration decl = m_env.get(const_name(fn));
+        if (length(const_levels(fn)) != decl.get_num_univ_params())
+            throw_ill_formed();
+        expr fn_body     = instantiate_value_univ_params(decl, const_levels(fn));
+        while (is_lambda(fn_body)) {
+            expr local = locals.push_local_from_binding(fn_body);
+            fn_body    = instantiate(binding_body(fn_body), local);
+        }
+        return whnf_rec(fn_body);
+    }
+
     expr unfold(expr const & fn, buffer<expr> args) {
-        buffer<expr> fn_locals;
+        type_context::tmp_locals fn_locals(m_ctx);
         expr fn_body = get_fn_decl(fn, fn_locals);
         if (args.size() < fn_locals.size()) {
             // insufficient args
@@ -313,7 +312,7 @@ class unfold_rec_fn : public replace_visitor_aux {
         unsigned main_pos = 0;
         buffer<unsigned> indices_pos;
         buffer<unsigned> rec_arg_pos;
-        rec_kind k = get_rec_kind(fn_body, fn_locals, rec_name, indices_pos, main_pos, rec_arg_pos);
+        rec_kind k = get_rec_kind(fn_body, fn_locals.as_buffer(), rec_name, indices_pos, main_pos, rec_arg_pos);
         if (k == NOREC || main_pos >= args.size()) {
             // norecursive definition
             return unfold_simple(fn, args);
@@ -327,9 +326,9 @@ class unfold_rec_fn : public replace_visitor_aux {
             throw fold_failed();
         }
         args[main_pos]      = new_main;
-        expr fn_body_abst   = abstract_locals(fn_body, fn_locals.size(), fn_locals.data());
-        expr new_e          = instantiate_rev(fn_body_abst, fn_locals.size(), args.data());
-        new_e               = mk_app(new_e, args.size() - fn_locals.size(), args.data() + fn_locals.size());
+        expr fn_body_abst   = m_ctx.abstract_locals(fn_body, fn_locals.as_buffer().size(), fn_locals.as_buffer().data());
+        expr new_e          = instantiate_rev(fn_body_abst, fn_locals.as_buffer().size(), args.data());
+        new_e               = mk_app(new_e, args.size() - fn_locals.as_buffer().size(), args.data() + fn_locals.as_buffer().size());
         new_e               = whnf_rec(new_e);
         expr const new_head = get_app_fn(new_e);
         // TODO(Leo): create an option for the following conditions?

tests/lean/unfold4.lean

@@ -0,0 +1,41 @@
+import data.nat
+import init.meta.tactic
+open tactic
+-- import init.meta.tactics
+
+inductive vector (A : Type) : nat → Type :=
+  | nil {} : vector A 0
+  | cons : Π {n}, A -> vector A n -> vector A (nat.succ n)
+
+definition vmap {A B : Type} (f : A -> B) : Π {n}, vector A n -> vector B n
+| vmap vector.nil := vector.nil
+| vmap (vector.cons x xs) := vector.cons (f x) (vmap xs)
+
+definition vappend {A} : Π {n m}, vector A n -> vector A m -> vector A (m + n)
+| vappend vector.nil vector.nil := vector.nil
+| vappend vector.nil (vector.cons x xs) := vector.cons x xs
+| vappend (vector.cons x xs) vector.nil := vector.cons x (vappend xs vector.nil)
+| vappend (vector.cons x xs) (vector.cons y ys) := vector.cons x (vappend xs (vector.cons y ys))
+
+check get_local
+
+axiom Sorry : ∀ A, A
+
+theorem vappend_assoc :
+  Π {A : Type} {n m k : nat} (v1 : vector A n) (v2 : vector A m) (v3 : vector A k),
+  vappend (vappend v1 v2) v3 == vappend v1 (vappend v2 v3) :=
+by do
+     intros,
+     v <- get_local "v1",
+     induction_core semireducible v ("vector" <.> "rec_on") [],
+     v2 ← get_local "v2",
+     cases_using v2 ["m", "h2", "t2"],
+     trace_state, trace "------",
+     -- unfold only the first occurrence (i.e., the one of the form (vappend nil nil)
+     unfold_occs_of [1] "vappend",
+     trace_state, trace "------",
+     mk_const "Sorry" >>= apply,
+     -- unfold only the first occurrence (i.e., the one of the form (vappend nil (cons ...))
+     unfold_occs_of [1] "vappend",
+     trace_state, trace "------",
+     repeat $ mk_const "Sorry" >>= apply

tests/lean/unfold4.lean.expected.out

@@ -0,0 +1,67 @@
+get_local : name → tactic expr
+A : Type,
+k : ℕ,
+v3 : vector A k,
+n m : ℕ
+⊢ vappend (vappend vector.nil vector.nil) v3 == vappend vector.nil (vappend vector.nil v3)
+
+A : Type,
+k : ℕ,
+v3 : vector A k,
+n m m : ℕ,
+h2 : A,
+t2 : vector A m
+⊢ vappend (vappend vector.nil (vector.cons h2 t2)) v3 == vappend vector.nil (vappend (vector.cons h2 t2) v3)
+
+A : Type,
+m k : ℕ,
+v2 : vector A m,
+v3 : vector A k,
+n n : ℕ,
+a : A,
+a : vector A n,
+v_0 : vappend (vappend a v2) v3 == vappend a (vappend v2 v3)
+⊢ vappend (vappend (vector.cons a_1 a) v2) v3 == vappend (vector.cons a_1 a) (vappend v2 v3)
+------
+A : Type,
+k : ℕ,
+v3 : vector A k,
+n m : ℕ
+⊢ vappend vector.nil v3 == vappend vector.nil (vappend vector.nil v3)
+
+A : Type,
+k : ℕ,
+v3 : vector A k,
+n m m : ℕ,
+h2 : A,
+t2 : vector A m
+⊢ vappend (vappend vector.nil (vector.cons h2 t2)) v3 == vappend vector.nil (vappend (vector.cons h2 t2) v3)
+
+A : Type,
+m k : ℕ,
+v2 : vector A m,
+v3 : vector A k,
+n n : ℕ,
+a : A,
+a : vector A n,
+v_0 : vappend (vappend a v2) v3 == vappend a (vappend v2 v3)
+⊢ vappend (vappend (vector.cons a_1 a) v2) v3 == vappend (vector.cons a_1 a) (vappend v2 v3)
+------
+A : Type,
+k : ℕ,
+v3 : vector A k,
+n m m : ℕ,
+h2 : A,
+t2 : vector A m
+⊢ vappend (vector.cons h2 t2) v3 == vappend vector.nil (vappend (vector.cons h2 t2) v3)
+
+A : Type,
+m k : ℕ,
+v2 : vector A m,
+v3 : vector A k,
+n n : ℕ,
+a : A,
+a : vector A n,
+v_0 : vappend (vappend a v2) v3 == vappend a (vappend v2 v3)
+⊢ vappend (vappend (vector.cons a_1 a) v2) v3 == vappend (vector.cons a_1 a) (vappend v2 v3)
+------

tests/lean/unfold_fact.lean

@@ -0,0 +1,24 @@
+import data.nat
+open nat
+
+definition fact1 : nat → nat
+| 0        := 1
+| (succ a) := (succ a) * fact1 a
+
+open tactic
+
+example (a : nat) : fact1 a > 0 :=
+by do
+  -- fact1 should not be unfolded since argument is not 0 or succ
+  unfold ["fact1"],
+  trace_state, trace "-------",
+  get_local "a" >>= λ H, induction_core semireducible H ("nat" <.> "rec_on") ["n", "iH"],
+  -- now it should unfold
+  unfold ["fact1"],
+  swap,
+  unfold ["fact1"],
+  trace_state,
+  mk_const "mul_pos" >>= apply,
+  mk_const ("nat" <.> "zero_lt_succ") >>= apply,
+  assumption,
+  mk_const "zero_lt_one" >>= apply

tests/lean/unfold_fact.lean.expected.out

@@ -0,0 +1,8 @@
+a : ℕ
+⊢ fact1 a > 0
+-------
+n : ℕ,
+iH : fact1 n > 0
+⊢ succ n * fact1 n > 0
+
+⊢ 1 > 0