From 937c4656857c1024da3a8e977f58e33cfb62a46f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 21 Aug 2014 21:37:51 -0700 Subject: [PATCH] fix(library/unifier): too much reduction Signed-off-by: Leonardo de Moura --- src/kernel/type_checker.h | 3 +- src/library/unifier.cpp | 23 +++++++++--- tests/lean/run/sum_bug.lean | 70 +++++++++++++++++++++++++++++++++++++ 3 files changed, 90 insertions(+), 6 deletions(-) create mode 100644 tests/lean/run/sum_bug.lean diff --git a/src/kernel/type_checker.h b/src/kernel/type_checker.h index 5a320e8bd..82ee4098c 100644 --- a/src/kernel/type_checker.h +++ b/src/kernel/type_checker.h @@ -95,7 +95,6 @@ class type_checker { friend class converter; // allow converter to access the following methods name mk_fresh_name() { return m_gen.next(); } - optional expand_macro(expr const & m); pair open_binding_body(expr const & e); pair ensure_sort_core(expr e, expr const & s); pair ensure_pi_core(expr e, expr const & s); @@ -199,6 +198,8 @@ public: cs = r.second + cs; return r.first; } + + optional expand_macro(expr const & m); }; typedef std::shared_ptr type_checker_ref; diff --git a/src/library/unifier.cpp b/src/library/unifier.cpp index bab982c76..02138dc98 100644 --- a/src/library/unifier.cpp +++ b/src/library/unifier.cpp @@ -1697,6 +1697,19 @@ struct unifier_fn { return std::all_of(margs.begin(), margs.end(), [&](expr const & e) { return is_local(e); }); } + optional expand_rhs(expr const & rhs, bool relax) { + buffer args; + expr const & f = get_app_rev_args(rhs, args); + lean_assert(!is_local(f) && !is_constant(f) && !is_var(f) && !is_metavar(f)); + if (is_lambda(f)) { + return some_expr(apply_beta(f, args.size(), args.data())); + } else if (is_macro(f)) { + return m_tc[relax]->expand_macro(rhs); + } else { + return none_expr(); + } + } + /** \brief Process a flex rigid constraint */ bool process_flex_rigid(expr lhs, expr const & rhs, justification const & j, bool relax) { lean_assert(is_meta(lhs)); @@ -1704,12 +1717,12 @@ struct unifier_fn { if (is_app(rhs)) { expr const & f = get_app_fn(rhs); if (!is_local(f) && !is_constant(f)) { - constraint_seq cs; - expr new_rhs = whnf(rhs, relax, cs); - lean_assert(new_rhs != rhs); - if (!process_constraints(cs, j)) + if (auto new_rhs = expand_rhs(rhs, relax)) { + lean_assert(*new_rhs != rhs); + return is_def_eq(lhs, *new_rhs, j, relax); + } else { return false; - return is_def_eq(lhs, new_rhs, j, relax); + } } } diff --git a/tests/lean/run/sum_bug.lean b/tests/lean/run/sum_bug.lean new file mode 100644 index 000000000..1a89cc1c4 --- /dev/null +++ b/tests/lean/run/sum_bug.lean @@ -0,0 +1,70 @@ +-- Copyright (c) 2014 Microsoft Corporation. All rights reserved. +-- Released under Apache 2.0 license as described in the file LICENSE. +-- Author: Leonardo de Moura, Jeremy Avigad + +import logic.connectives.prop logic.classes.inhabited logic.classes.decidable + +using inhabited decidable + +namespace sum + +-- TODO: take this outside the namespace when the inductive package handles it better +inductive sum (A B : Type) : Type := +| inl : A → sum A B +| inr : B → sum A B + +infixr `+`:25 := sum + +abbreviation rec_on {A B : Type} {C : (A + B) → Type} (s : A + B) + (H1 : ∀a : A, C (inl B a)) (H2 : ∀b : B, C (inr A b)) : C s := +sum_rec H1 H2 s + + +theorem inl_inj {A B : Type} {a1 a2 : A} (H : inl B a1 = inl B a2) : a1 = a2 := +let f := λs, rec_on s (λa, a1 = a) (λb, false) in +have H1 : f (inl B a1), from rfl, +have H2 : f (inl B a2), from subst H H1, +H2 + +abbreviation cases_on {A B : Type} {P : (A + B) → Prop} (s : A + B) + (H1 : ∀a : A, P (inl B a)) (H2 : ∀b : B, P (inr A b)) : P s := +sum_rec H1 H2 s + +theorem inl_neq_inr {A B : Type} {a : A} {b : B} (H : inl B a = inr A b) : false := +let f := λs, rec_on s (λa', a = a') (λb, false) in +have H1 : f (inl B a), from rfl, +have H2 : f (inr A b), from subst H H1, +H2 + +theorem inr_inj {A B : Type} {b1 b2 : B} (H : inr A b1 = inr A b2) : b1 = b2 := +let f := λs, rec_on s (λa, false) (λb, b1 = b) in +have H1 : f (inr A b1), from rfl, +have H2 : f (inr A b2), from subst H H1, +H2 + +theorem sum_inhabited_left [instance] {A B : Type} (H : inhabited A) : inhabited (A + B) := +inhabited_mk (inl B (default A)) + +theorem sum_inhabited_right [instance] {A B : Type} (H : inhabited B) : inhabited (A + B) := +inhabited_mk (inr A (default B)) + +theorem sum_eq_decidable [instance] {A B : Type} (s1 s2 : A + B) + (H1 : ∀a1 a2, decidable (inl B a1 = inl B a2)) + (H2 : ∀b1 b2, decidable (inr A b1 = inr A b2)) : decidable (s1 = s2) := +rec_on s1 + (take a1, show decidable (inl B a1 = s2), from + rec_on s2 + (take a2, show decidable (inl B a1 = inl B a2), from H1 a1 a2) + (take b2, + have H3 : (inl B a1 = inr A b2) ↔ false, + from iff_intro inl_neq_inr (assume H4, false_elim _ H4), + show decidable (inl B a1 = inr A b2), from decidable_iff_equiv _ (iff_symm H3))) + (take b1, show decidable (inr A b1 = s2), from + rec_on s2 + (take a2, + have H3 : (inr A b1 = inl B a2) ↔ false, + from iff_intro (assume H4, inl_neq_inr (symm H4)) (assume H4, false_elim _ H4), + show decidable (inr A b1 = inl B a2), from decidable_iff_equiv _ (iff_symm H3)) + (take b2, show decidable (inr A b1 = inr A b2), from H2 b1 b2)) + +end sum \ No newline at end of file