fix(library/tactic/unfold_rec): support indexed families + brec_on at unfold_rec

see issue #692

src/library/tactic/unfold_rec.cpp

@@ -250,6 +250,10 @@ class unfold_rec_fn : public replace_visitor_aux {
             }
             buffer<expr> new_args;
             new_args.append(m_args);
+            unsigned nindices = m_indices_pos.size();
+            for (unsigned i = 0; i < m_indices_pos.size(); i++) {
+                new_args[m_indices_pos[i]] = nested_args[m_major_idx - nindices + i];
+            }
             new_args[m_main_pos] = nested_args[m_major_idx];
             for (unsigned i = 0; i < m_rec_arg_pos.size(); i++) {
                 new_args[m_rec_arg_pos[i]] = args[prefix_size + i];

tests/lean/run/unfold_rec.lean

@@ -0,0 +1,50 @@
+import data.vector
+open nat vector
+
+variables {A B : Type}
+variable {n : nat}
+
+theorem tst1 : ∀ n m, succ n + succ m = succ (succ (n + m)) :=
+begin
+  intro n m,
+  esimp [add],
+  state,
+  rewrite [succ_add]
+end
+
+definition add2 (x y : nat) : nat :=
+nat.rec_on x (λ y, y) (λ x r y, succ (r y)) y
+
+local infix + := add2
+
+theorem tst2 : ∀ n m, succ n + succ m = succ (succ (n + m)) :=
+begin
+  intro n m,
+  esimp [add2],
+  state,
+  apply sorry
+end
+
+definition fib (A : Type) : nat → nat → nat → nat
+| b 0      c         := b
+| b 1      c         := c
+| b (succ (succ a)) c := fib b a c + fib b (succ a) c
+
+theorem fibgt0 : ∀ b n c, fib nat b n c > 0
+| b 0 c := sorry
+| b 1 c := sorry
+| b (succ (succ m)) c :=
+begin
+  unfold fib,
+  state,
+  apply sorry
+end
+
+theorem unzip_zip : ∀ {n : nat} (v₁ : vector A n) (v₂ : vector B n), unzip (zip v₁ v₂) = (v₁, v₂)
+| 0        []      []      := rfl
+| (succ m) (a::va) (b::vb) :=
+begin
+  unfold [zip, unzip],
+  state,
+  rewrite [unzip_zip]
+end

tests/lean/run/unfold_rec2.lean

@@ -0,0 +1,22 @@
+import data.vector
+open nat vector
+
+variable {A : Type}
+
+definition rev : Π {n : nat}, vector A n → vector A n
+| ⌞0⌟     []      := []
+| ⌞n+1⌟ (x :: xs) := concat (rev xs) x
+
+theorem rev_concat : Π {n : nat} (xs : vector A n) (a : A), rev (concat xs a) = a :: rev xs
+| 0     []         a := rfl
+| (n+1) (x :: xs)  a :=
+  begin
+    unfold [concat, rev], rewrite rev_concat
+  end
+
+theorem rev_rev : Π {n : nat} (xs : vector A n), rev (rev xs) = xs
+| 0     []        := rfl
+| (n+1) (x :: xs) :=
+  begin
+    unfold rev at {1}, krewrite rev_concat, rewrite rev_rev
+  end