fix(library/tactic/inversion_tactic): bug in injectivity transition

src/library/tactic/inversion_tactic.cpp

@@ -328,8 +328,9 @@ class inversion_tac {
                 goal new_g(new_meta, new_type);
                 expr val      = g.abstract(mk_app(no_confusion, new_meta));
                 m_subst.assign(g.get_name(), val);
-                lean_assert(lhs_args.size() >= m_nparams);
-                return unify_eqs(new_g, neqs - 1 + lhs_args.size() - m_nparams);
+                unsigned A_nparams = *inductive::get_num_params(m_env, const_name(A_fn));
+                lean_assert(lhs_args.size() >= A_nparams);
+                return unify_eqs(new_g, neqs - 1 + lhs_args.size() - A_nparams);
             } else {
                 // conflict transition, eq is of the form c_1 ... = c_2 ..., where c_1 and c_2 are different constructors/intro rules.
                 expr val      = g.abstract(no_confusion);

tests/lean/run/vec_inv.lean

@@ -0,0 +1,29 @@
+import data.nat.basic data.empty data.prod
+open nat eq.ops prod
+
+inductive vector (T : Type) : ℕ → Type :=
+  nil {} : vector T 0,
+  cons : T → ∀{n}, vector T n → vector T (succ n)
+
+set_option pp.metavar_args true
+set_option pp.implicit true
+set_option pp.notation false
+
+namespace vector
+  variables {A B C : Type}
+  variables {n m : nat}
+
+  theorem z_cases_on {C : vector A 0 → Type} (v : vector A 0) (Hnil : C nil) : C v :=
+  begin
+    cases v,
+    apply Hnil
+  end
+
+  protected definition destruct (v : vector A (succ n)) {P : Π {n : nat}, vector A (succ n) → Type}
+                      (H : Π {n : nat} (h : A) (t : vector A n), P (cons h t)) : P v :=
+  begin
+    cases v,
+    apply (H a a_1)
+  end
+
+end vector