From ac24f19210851a3121d2b3304a243861cfa832e8 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 7 May 2015 09:57:23 -0700 Subject: [PATCH] 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 | 30 ++++++++++++------------ tests/lean/583.lean | 33 +++++++++++++++++++++++++++ tests/lean/583.lean.expected.out | 15 ++++++++++++ 3 files changed, 63 insertions(+), 15 deletions(-) create mode 100644 tests/lean/583.lean create mode 100644 tests/lean/583.lean.expected.out diff --git a/src/library/tactic/rewrite_tactic.cpp b/src/library/tactic/rewrite_tactic.cpp index e736dfefa..f016bf57d 100644 --- a/src/library/tactic/rewrite_tactic.cpp +++ b/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 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 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; - level l1 = sort_level(m_unifier_tc->ensure_type(Pa).first); - level l2 = sort_level(m_unifier_tc->ensure_type(A).first); + expr A = m_relaxed_tc->infer(a).first; + level l1 = sort_level(m_relaxed_tc->ensure_type(Pa).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; - level l1 = sort_level(m_unifier_tc->ensure_type(Pa).first); - level l2 = sort_level(m_unifier_tc->ensure_type(A).first); + expr A = m_relaxed_tc->infer(a).first; + level l1 = sort_level(m_relaxed_tc->ensure_type(Pa).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(); diff --git a/tests/lean/583.lean b/tests/lean/583.lean new file mode 100644 index 000000000..db9e740e6 --- /dev/null +++ b/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 diff --git a/tests/lean/583.lean.expected.out b/tests/lean/583.lean.expected.out new file mode 100644 index 000000000..2edc63294 --- /dev/null +++ b/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