From 2ca29202841b7d892fd9d4a99b9ab8ed2d6c6abc Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 23 Jan 2017 09:59:06 -0800
Subject: [PATCH] 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        |  5 +-
 tests/lean/run/simp_univ_metavars.lean | 76 ++++++++++++++++++++++++++
 2 files changed, 79 insertions(+), 2 deletions(-)
 create mode 100644 tests/lean/run/simp_univ_metavars.lean

diff --git a/src/library/tactic/simplify.cpp b/src/library/tactic/simplify.cpp
index afe03d48b6..845c6a4f62 100644
--- a/src/library/tactic/simplify.cpp
+++ b/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());
diff --git a/tests/lean/run/simp_univ_metavars.lean b/tests/lean/run/simp_univ_metavars.lean
new file mode 100644
index 0000000000..c6b738808c
--- /dev/null
+++ b/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
+}