From f57fc334427a2cdd77f82a4e0bec07791acd02d3 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 31 Jul 2014 14:36:13 -0700 Subject: [PATCH] fix(library/unifier): bug that was making unifier miss solutions, and add a new case-split that tries to solve flex_rigid constraints by putting the rhs into whnf Signed-off-by: Leonardo de Moura --- src/library/unifier.cpp | 84 ++++++++++++++++++++++++++++------ tests/lean/run/list_elab1.lean | 29 ++++++++++++ tests/lean/run/nat_bug7.lean | 15 ++++++ 3 files changed, 114 insertions(+), 14 deletions(-) create mode 100644 tests/lean/run/list_elab1.lean create mode 100644 tests/lean/run/nat_bug7.lean diff --git a/src/library/unifier.cpp b/src/library/unifier.cpp index 9b29c4b6e..1d473dea7 100644 --- a/src/library/unifier.cpp +++ b/src/library/unifier.cpp @@ -430,6 +430,45 @@ struct unifier_fn { } } + /** \brief Put \c e in weak head normal form. + + \remark If relax is true then opaque definitions from the main module are treated as transparent. + \remark Constraints generated in the process are stored in \c cs. The justification \c j is composed with them. + */ + expr whnf(expr const & e, justification const & j, bool relax, buffer & cs) { + unsigned cs_sz = cs.size(); + expr r = m_tc[relax]->whnf(e, cs); + for (unsigned i = cs_sz; i < cs.size(); i++) + cs[i] = update_justification(cs[i], mk_composite1(j, cs[i].get_justification())); + return r; + } + + /** \brief Process the given constraints. Return true iff no conflict was detected. */ + bool process_constraints(buffer & cs) { + for (auto const & c : cs) + if (!process_constraint(c)) + return false; + return true; + } + + /** \brief Infer \c e type. + + \remark Return none if an exception was throw when inferring the type. + \remark If relax is true then opaque definitions from the main module are treated as transparent. + \remark Constraints generated in the process are stored in \c cs. The justification \c j is composed with them. + */ + optional infer(expr const & e, justification const & j, bool relax, buffer & cs) { + try { + unsigned cs_sz = cs.size(); + expr r = m_tc[relax]->infer(e, cs); + for (unsigned i = cs_sz; i < cs.size(); i++) + cs[i] = update_justification(cs[i], mk_composite1(j, cs[i].get_justification())); + return some_expr(r); + } catch (exception &) { + return none_expr(); + } + } + /** \brief Assign \c v to metavariable \c m with justification \c j. The type of v and m are inferred, and is_def_eq is invoked. @@ -439,17 +478,20 @@ struct unifier_fn { */ bool assign(expr const & m, expr const & v, justification const & j, bool relax) { lean_assert(is_metavar(m)); + lean_assert(!in_conflict()); m_subst.assign(m, v, j); expr m_type = mlocal_type(m); expr v_type; - try { - v_type = m_tc[relax]->infer(v); - } catch (kernel_exception & e) { + buffer cs; + if (auto type = infer(v, j, relax, cs)) { + v_type = *type; + if (!process_constraints(cs)) + return false; + } else { set_conflict(j); return false; } - if (in_conflict()) - return false; + lean_assert(!in_conflict()); if (!is_def_eq(m_type, v_type, j, relax)) return false; auto it = m_mvar_occs.find(mlocal_name(m)); @@ -933,9 +975,13 @@ struct unifier_fn { } expr m_type; bool relax = relax_main_opaque(c); - try { - m_type = m_tc[relax]->infer(m); - } catch (kernel_exception &) { + + buffer cs; + if (auto type = infer(m, c.get_justification(), relax, cs)) { + m_type = *type; + if (!process_constraints(cs)) + return false; + } else { set_conflict(c.get_justification()); return false; } @@ -1071,8 +1117,8 @@ struct unifier_fn { \brief Make sure mtype is a Pi of size at least margs.size(). If it is not, we use ensure_pi and (potentially) add new constaints to enforce it. */ - optional ensure_sufficient_args(expr const & mtype, buffer const & margs, buffer & cs, justification const & j, - bool relax) { + optional ensure_sufficient_args(expr const & mtype, buffer const & margs, buffer & cs, + justification const & j, bool relax) { expr t = mtype; unsigned num = 0; while (is_pi(t)) { @@ -1386,7 +1432,7 @@ struct unifier_fn { \remark We need this step because of the optimization based on is_easy_flex_rigid_arg */ - expr expose_local_args(expr const & lhs, bool relax, buffer & aux) { + expr expose_local_args(expr const & lhs, justification const & j, bool relax, buffer & aux) { buffer margs; expr m = get_app_args(lhs, margs); bool modified = false; @@ -1394,7 +1440,7 @@ struct unifier_fn { // Make sure that if marg is reducible to a local constant, then it is replaced with it. // We need that because of the optimization based on is_easy_flex_rigid_arg if (!is_local(marg)) { - expr new_marg = m_tc[relax]->whnf(marg, aux); + expr new_marg = whnf(marg, j, relax, aux); if (is_local(new_marg)) { marg = new_marg; modified = true; @@ -1411,17 +1457,27 @@ struct unifier_fn { if (is_app(rhs)) { expr const & f = get_app_fn(rhs); if (!is_local(f) && !is_constant(f)) { - expr new_rhs = m_tc[relax]->whnf(rhs); + buffer cs; + expr new_rhs = whnf(rhs, j, relax, cs); lean_assert(new_rhs != rhs); + if (!process_constraints(cs)) + return false; return is_def_eq(lhs, new_rhs, j, relax); } } buffer aux; - lhs = expose_local_args(lhs, relax, aux); + lhs = expose_local_args(lhs, j, relax, aux); buffer alts; process_flex_rigid_core(lhs, rhs, j, relax, alts); append_auxiliary_constraints(alts, to_list(aux.begin(), aux.end())); + expr rhs_whnf = whnf(rhs, j, relax, aux); + if (rhs_whnf != rhs) { + buffer alts2; + process_flex_rigid_core(lhs, rhs_whnf, j, relax, alts2); + append_auxiliary_constraints(alts2, to_list(aux.begin(), aux.end())); + alts.append(alts2); + } if (alts.empty()) { set_conflict(j); diff --git a/tests/lean/run/list_elab1.lean b/tests/lean/run/list_elab1.lean new file mode 100644 index 000000000..1599ed19d --- /dev/null +++ b/tests/lean/run/list_elab1.lean @@ -0,0 +1,29 @@ +---------------------------------------------------------------------------------------------------- +--- Copyright (c) 2014 Parikshit Khanna. All rights reserved. +--- Released under Apache 2.0 license as described in the file LICENSE. +--- Authors: Parikshit Khanna, Jeremy Avigad +---------------------------------------------------------------------------------------------------- + +-- Theory list +-- =========== +-- +-- Basic properties of lists. + +import nat +using nat eq_proofs + +inductive list (T : Type) : Type := +| nil {} : list T +| cons : T → list T → list T + +theorem list_induction_on {T : Type} {P : list T → Prop} (l : list T) (Hnil : P nil) + (Hind : forall x : T, forall l : list T, forall H : P l, P (cons x l)) : P l := +list_rec Hnil Hind l + +definition concat {T : Type} (s t : list T) : list T := +list_rec t (fun x : T, fun l : list T, fun u : list T, cons x u) s + +theorem concat_nil {T : Type} (t : list T) : concat t nil = t := +list_induction_on t (refl (concat nil nil)) + (take (x : T) (l : list T) (H : concat l nil = l), + H ▸ (refl (concat (cons x l) nil))) diff --git a/tests/lean/run/nat_bug7.lean b/tests/lean/run/nat_bug7.lean new file mode 100644 index 000000000..d1a58fabe --- /dev/null +++ b/tests/lean/run/nat_bug7.lean @@ -0,0 +1,15 @@ +import logic + +inductive nat : Type := +| zero : nat +| succ : nat → nat + +definition add (x y : nat) : nat := nat_rec x (λn r, succ r) y +infixl `+`:65 := add + +axiom add_right_comm (n m k : nat) : n + m + k = n + k + m + +print "===========================" +theorem bug (a b c d : nat) : a + b + c + d = a + c + b + d +:= subst (add_right_comm _ _ _) (refl (a + b + c + d)) +