fix(library/tactic/rewrite_tactic): use relaxed type checker when processing rewrite "proof step"

That is, the restricted type checker should only be used in the
matching/unification step.

fixes #583

src/library/tactic/rewrite_tactic.cpp

@@ -540,7 +540,7 @@ class rewrite_fn {
     name_generator       m_ngen;
     type_checker_ptr     m_tc;
     type_checker_ptr     m_matcher_tc;
-    type_checker_ptr     m_unifier_tc; // reduce_to and check_trivial
+    type_checker_ptr     m_relaxed_tc; // reduce_to and check_trivial
     rewrite_match_plugin m_mplugin;
     goal                 m_g;
     local_context        m_ctx;
@@ -755,7 +755,7 @@ class rewrite_fn {
         buffer<constraint> cs;
         to_buffer(ecs.second, cs);
         constraint_seq cs_seq;
-        if (!m_unifier_tc->is_def_eq(t, new_e, justification(), cs_seq))
+        if (!m_relaxed_tc->is_def_eq(t, new_e, justification(), cs_seq))
             return none_expr();
         cs_seq.linearize(cs);
         unifier_config cfg;
@@ -892,10 +892,10 @@ class rewrite_fn {
             // Remark: we discard constraints generated producing the pattern.
             // Patterns are only used to locate positions where the rule should be applied.
             expr rule      = get_rewrite_rule(e);
-            expr rule_type = m_tc->whnf(m_tc->infer(rule).first).first;
+            expr rule_type = m_relaxed_tc->whnf(m_relaxed_tc->infer(rule).first).first;
             while (is_pi(rule_type)) {
                 expr meta  = mk_meta(binding_domain(rule_type));
-                rule_type  = m_tc->whnf(instantiate(binding_body(rule_type), meta)).first;
+                rule_type  = m_relaxed_tc->whnf(instantiate(binding_body(rule_type), meta)).first;
             }
             if (!is_eq(rule_type))
                 throw_rewrite_exception("invalid rewrite tactic, given lemma is not an equality");
@@ -1079,7 +1079,7 @@ class rewrite_fn {
             buffer<constraint> cs;
             to_buffer(rcs.second, cs);
             constraint_seq cs_seq;
-            expr rule_type = m_tc->whnf(m_tc->infer(rule, cs_seq), cs_seq);
+            expr rule_type = m_relaxed_tc->whnf(m_relaxed_tc->infer(rule, cs_seq), cs_seq);
             while (is_pi(rule_type)) {
                 expr meta;
                 if (binding_info(rule_type).is_inst_implicit()) {
@@ -1089,7 +1089,7 @@ class rewrite_fn {
                 } else {
                     meta = mk_meta(binding_domain(rule_type));
                 }
-                rule_type  = m_tc->whnf(instantiate(binding_body(rule_type), meta), cs_seq);
+                rule_type  = m_relaxed_tc->whnf(instantiate(binding_body(rule_type), meta), cs_seq);
                 rule       = mk_app(rule, meta);
             }
             lean_assert(is_eq(rule_type));
@@ -1124,12 +1124,12 @@ class rewrite_fn {
                     if (symm) {
                         return unify_result(rule, lhs);
                     } else {
-                        rule = mk_symm(*m_tc, rule);
+                        rule = mk_symm(*m_relaxed_tc, rule);
                         return unify_result(rule, rhs);
                     }
                 } else {
                     if (symm) {
-                        rule = mk_symm(*m_tc, rule);
+                        rule = mk_symm(*m_relaxed_tc, rule);
                         return unify_result(rule, lhs);
                     } else {
                         return unify_result(rule, rhs);
@@ -1209,9 +1209,9 @@ class rewrite_fn {
             expr Px  = replace_occurrences(Pa, a, occ, vidx);
             expr Pb  = instantiate(Px, vidx, b);
 
-            expr A   = m_tc->infer(a).first;
+            expr A   = m_relaxed_tc->infer(a).first;
-            level l1 = sort_level(m_unifier_tc->ensure_type(Pa).first);
+            level l1 = sort_level(m_relaxed_tc->ensure_type(Pa).first);
-            level l2 = sort_level(m_unifier_tc->ensure_type(A).first);
+            level l2 = sort_level(m_relaxed_tc->ensure_type(A).first);
             expr H;
             if (has_dep_elim) {
                 expr Haeqx = mk_app(mk_constant(get_eq_name(), {l2}), A, a, mk_var(0));
@@ -1260,9 +1260,9 @@ class rewrite_fn {
             unsigned vidx = has_dep_elim ? 1 : 0;
             expr Px  = replace_occurrences(Pa, a, occ, vidx);
             expr Pb  = instantiate(Px, vidx, b);
-            expr A   = m_tc->infer(a).first;
+            expr A   = m_relaxed_tc->infer(a).first;
-            level l1 = sort_level(m_unifier_tc->ensure_type(Pa).first);
+            level l1 = sort_level(m_relaxed_tc->ensure_type(Pa).first);
-            level l2 = sort_level(m_unifier_tc->ensure_type(A).first);
+            level l2 = sort_level(m_relaxed_tc->ensure_type(A).first);
             expr M   = m_g.mk_meta(m_ngen.next(), Pb);
             expr H;
             if (has_dep_elim) {
@@ -1458,7 +1458,7 @@ public:
         m_env(env), m_ios(ios), m_elab(elab), m_ps(ps), m_ngen(ps.get_ngen()),
         m_tc(mk_type_checker(m_env, m_ngen.mk_child(), ps.relax_main_opaque(), UnfoldQuasireducible)),
         m_matcher_tc(mk_matcher_tc()),
-        m_unifier_tc(mk_type_checker(m_env, m_ngen.mk_child(), ps.relax_main_opaque())),
+        m_relaxed_tc(mk_type_checker(m_env, m_ngen.mk_child(), ps.relax_main_opaque())),
         m_mplugin(m_ios, *m_matcher_tc) {
         m_ps = apply_substitution(m_ps);
         goals const & gs = m_ps.get_goals();

tests/lean/583.lean

@@ -0,0 +1,33 @@
+import algebra.group data.set
+namespace group_hom
+open algebra
+-- ⁻¹ in eq.ops conflicts with group ⁻¹
+-- open eq.ops
+notation H1 ▸ H2 := eq.subst H1 H2
+open set
+open function
+local attribute set [reducible]
+
+section
+variables {A B : Type}
+variable [s1 : group A]
+variable [s2 : group B]
+include s1
+include s2
+variable f : A → B
+definition is_hom := ∀ a b, f (a*b) = (f a)*(f b)
+definition ker (Hom : is_hom f) : (set A) := {a : A | f a = 1}
+theorem hom_map_id (f : A → B) (Hom : is_hom f) : f 1 = 1 :=
+        have P : f 1 = (f 1) * (f 1), from
+        calc f 1 = f (1*1) : mul_one
+        ... = (f 1) * (f 1) : Hom,
+        eq.symm (mul.right_inv (f 1) ▸ (mul_inv_eq_of_eq_mul P))
+
+theorem hom_map_inv (Hom : is_hom f) (a : A) : f a⁻¹ = (f a)⁻¹ :=
+        assert P : f 1 = 1, from hom_map_id f Hom,
+        begin
+          rewrite (eq.symm (mul.left_inv a)) at P,
+          rewrite (Hom a⁻¹ a) at P,
+        end
+end
+end group_hom

tests/lean/583.lean.expected.out

@@ -0,0 +1,15 @@
+583.lean:31:8: error: 1 unsolved subgoal
+A : Type,
+B : Type,
+s1 : group A,
+s2 : group B,
+f : A → B,
+Hom : is_hom f,
+a : A,
+P : f a⁻¹ * f a = 1
+⊢ f a⁻¹ = (f a)⁻¹
+583.lean:27:8: error: failed to add declaration 'group_hom.hom_map_inv' to environment, value has metavariables
+remark: set 'formatter.hide_full_terms' to false to see the complete term
+  λ (A : Type) (B : Type) (s1 : …) (s2 : …) (f : …) (Hom : …) (a : A),
+    have P [visible] : …, from …,
+    ?M_1