fix(library/tactic/simplify): relax test

We only need to check whether the resulting expression does not contain
temporary metavariables introduced by the simplifier.
It is ok if it contains regular metavariables that were already in the goal.

This fixes the issue reported at
https://groups.google.com/forum/#!topic/lean-user/3qzchWkut0g

src/library/tactic/simplify.cpp

@@ -22,6 +22,7 @@ Author: Daniel Selsam, Leonardo de Moura
 #include "library/expr_lt.h"
 #include "library/locals.h"
 #include "library/num.h"
+#include "library/idx_metavar.h"
 #include "library/util.h"
 #include "library/norm_num.h"
 #include "library/attribute_manager.h"
@@ -91,7 +92,7 @@ bool simplify_core_fn::instantiate_emetas(tmp_type_context & tmp_ctx, unsigned n
             i--;
             if (failed) return;
             expr mvar_type = tmp_ctx.instantiate_mvars(tmp_ctx.infer(mvar));
-            if (has_metavar(mvar_type)) {
+            if (has_idx_metavar(mvar_type)) {
                 failed = true;
                 return;
             }
@@ -252,7 +253,7 @@ simp_result simplify_core_fn::try_user_congr(expr const & e, simp_lemma const &
             expr d = instantiate_rev(binding_domain(m_type), local_factory.as_buffer().size(),
                                      local_factory.as_buffer().data());
             expr l = local_factory.push_local(binding_name(m_type), d, binding_info(m_type));
-            lean_assert(!has_metavar(l));
+            lean_assert(!has_idx_metavar(l));
             m_type = binding_body(m_type);
         }
         m_type = instantiate_rev(m_type, local_factory.as_buffer().size(), local_factory.as_buffer().data());

tests/lean/run/simp_univ_metavars.lean

@@ -0,0 +1,76 @@
+meta def blast : tactic unit := using_smt $ return ()
+
+structure { u v } Category :=
+  (Obj : Type u )
+  (Hom : Obj -> Obj -> Type v)
+  (identity : Π X : Obj, Hom X X)
+  (compose  : Π ⦃X Y Z : Obj⦄, Hom X Y → Hom Y Z → Hom X Z)
+  (left_identity  : ∀ ⦃X Y : Obj⦄ (f : Hom X Y), compose (identity _) f = f)
+
+structure Functor (C : Category) (D : Category) :=
+  (onObjects   : C^.Obj → D^.Obj)
+  (onMorphisms : Π ⦃X Y : C^.Obj⦄,
+                C^.Hom X Y → D^.Hom (onObjects X) (onObjects Y))
+
+structure NaturalTransformation { C D : Category } ( F G : Functor C D ) :=
+  (components: Π X : C^.Obj, D^.Hom (F^.onObjects X) (G^.onObjects X))
+
+definition IdentityNaturalTransformation { C D : Category } (F : Functor C D) : NaturalTransformation F F :=
+  {
+    components := λ X, D^.identity (F^.onObjects X)
+  }
+
+definition vertical_composition_of_NaturalTransformations
+  { C D : Category }
+  { F G H : Functor C D }
+  ( α : NaturalTransformation F G )
+  ( β : NaturalTransformation G H ) : NaturalTransformation F H :=
+  {
+    components := λ X, D^.compose (α^.components X) (β^.components X)
+  }
+
+-- We'll want to be able to prove that two natural transformations are equal if they are componentwise equal.
+lemma NaturalTransformations_componentwise_equal
+  { C D : Category }
+  { F G : Functor C D }
+  ( α β : NaturalTransformation F G )
+  ( w : ∀ X : C^.Obj, α^.components X = β^.components X ) : α = β :=
+  begin
+    induction α with αc,
+    induction β with βc,
+    have hc : αc = βc, from funext w,
+    by subst hc
+  end
+
+@[simp]
+lemma vertical_composition_of_NaturalTransformations_components
+  { C D : Category }
+  { F G H : Functor C D }
+  { α : NaturalTransformation F G }
+  { β : NaturalTransformation G H }
+  { X : C^.Obj } :
+  (vertical_composition_of_NaturalTransformations α β)^.components X = D^.compose (α^.components X) (β^.components X) :=
+by blast
+
+@[simp]
+lemma IdentityNaturalTransformation_components
+  { C D : Category }
+  { F : Functor C D }
+  { X : C^.Obj } :
+  (IdentityNaturalTransformation F)^.components X = D^.identity (F^.onObjects X) :=
+by blast
+
+definition FunctorCategory ( C D : Category ) : Category :=
+{
+  Obj := Functor C D,
+  Hom := λ F G, NaturalTransformation F G,
+  identity := λ F, IdentityNaturalTransformation F,
+  compose  := @vertical_composition_of_NaturalTransformations C D,
+
+  left_identity  := begin
+                     intros F G f,
+                     apply NaturalTransformations_componentwise_equal,
+                     intros,
+                     simp [ D^.left_identity ]
+                    end
+}