From 442cbff57848f175e7295336730958a254952e85 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 2 Oct 2015 15:21:28 -0700 Subject: [PATCH] feat(library/blast): add blast tactic is_def_eq procedure (aka unification) We still have to implement subst_mref, assign_mref, and occurs check. --- src/library/blast/infer_type.cpp | 171 ++++++++++++++++++++++++++++++- src/library/blast/infer_type.h | 16 +-- src/library/blast/state.h | 5 + 3 files changed, 181 insertions(+), 11 deletions(-) diff --git a/src/library/blast/infer_type.cpp b/src/library/blast/infer_type.cpp index 4bc85bc14..1682935df 100644 --- a/src/library/blast/infer_type.cpp +++ b/src/library/blast/infer_type.cpp @@ -7,6 +7,7 @@ Author: Leonardo de Moura #include "util/interrupt.h" #include "kernel/instantiate.h" #include "kernel/abstract.h" +#include "library/normalize.h" #include "library/blast/infer_type.h" #include "library/blast/blast_context.h" #include "library/blast/blast_exception.h" @@ -105,11 +106,6 @@ expr whnf(expr const & e) { } } -bool is_def_eq(expr const & e1, expr const & e2) { - // TODO(Leo) - return e1 == e2; -} - static expr infer_constant(expr const & e) { declaration d = env().get(const_name(e)); auto const & ps = d.get_univ_params(); @@ -184,6 +180,8 @@ static void ensure_pi(expr const & e, expr const & ref) { // Remark: for simplicity reasons, we just fail if \c e is not a Pi. if (!is_pi(e)) throw blast_exception("infer type failed, Pi expected", ref); + // Potential problem: e is of the form (f ...) where f is a constant that is not marked as reducible. + // So, whnf does not reduce it, and we fail to detect that e is can be reduced to a Pi-expression. } static expr infer_app(expr const & e) { @@ -250,4 +248,167 @@ expr infer_type(expr const & e) { // TODO(Leo): cache results if we have performance problems return r; } + +bool is_prop(expr const & e) { + if (env().impredicative()) { + expr t = whnf(infer_type(e)); + return t == mk_Prop(); + } else { + return false; + } +} + +bool is_def_eq(level const & l1, level const & l2) { + if (is_equivalent(l1, l2)) { + return true; + } else { + // TODO(Leo): check/update universe level assignment + lean_unreachable(); + return false; + } +} + +bool is_def_eq(levels const & ls1, levels const & ls2) { + if (is_nil(ls1) && is_nil(ls2)) { + return true; + } else if (!is_nil(ls1) && !is_nil(ls2)) { + return + is_def_eq(head(ls1), head(ls2)) && + is_def_eq(tail(ls1), tail(ls2)); + } else { + return false; + } +} + +/** \brief Given \c e of the form ?m t_1 ... t_n, where + ?m is an assigned mref, substitute \c ?m with its assignment. */ +static expr subst_mref(expr const & e) { + // TODO(Leo): + lean_unreachable(); +} + +/** \brief Given \c m of the form ?m t_1 ... t_n, (try to) assign + ?m to (an abstraction of) v. Return true if success and false otherwise. */ +static bool assign_mref(expr const & m, expr const & v) { + // TODO(Leo): + lean_unreachable(); +} + +static bool is_def_eq_binding(expr e1, expr e2) { + lean_assert(e1.kind() == e2.kind()); + lean_assert(is_binding(e1)); + expr_kind k = e1.kind(); + buffer subst; + do { + optional var_e1_type; + if (binding_domain(e1) != binding_domain(e2)) { + var_e1_type = instantiate_rev(binding_domain(e1), subst.size(), subst.data()); + expr var_e2_type = instantiate_rev(binding_domain(e2), subst.size(), subst.data()); + if (!is_def_eq(var_e2_type, *var_e1_type)) + return false; + } + if (!closed(binding_body(e1)) || !closed(binding_body(e2))) { + // local is used inside t or s + if (!var_e1_type) + var_e1_type = instantiate_rev(binding_domain(e1), subst.size(), subst.data()); + subst.push_back(blast::mk_local(mk_fresh_local_name(), binding_name(e1), + *var_e1_type, binding_info(e1))); + } else { + expr const & dont_care = mk_Prop(); + subst.push_back(dont_care); + } + e1 = binding_body(e1); + e2 = binding_body(e2); + } while (e1.kind() == k && e2.kind() == k); + return is_def_eq(instantiate_rev(e1, subst.size(), subst.data()), + instantiate_rev(e2, subst.size(), subst.data())); +} + +static bool is_def_eq_app(expr const & e1, expr const & e2) { + lean_assert(is_app(e1) && is_app(e2)); + buffer args1, args2; + expr const & f1 = get_app_args(e1, args1); + expr const & f2 = get_app_args(e2, args2); + if (args1.size() != args2.size() || !is_def_eq(f1, f2)) + return false; + for (unsigned i = 0; i < args1.size(); i++) { + if (!is_def_eq(args1[i], args2[i])) + return false; + } + return true; +} + +static bool is_def_eq_eta(expr const & e1, expr const & e2) { + expr new_e1 = try_eta(e1); + expr new_e2 = try_eta(e2); + if (e1 != new_e1 || e2 != new_e2) + return is_def_eq(new_e1, new_e2); + return false; +} + +static bool is_def_eq_proof_irrel(expr const & e1, expr const & e2) { + if (!env().prop_proof_irrel()) + return false; + expr e1_type = infer_type(e1); + expr e2_type = infer_type(e2); + return is_prop(e1_type) && is_def_eq(e1_type, e2_type); +} + +bool is_def_eq(expr const & e1, expr const & e2) { + check_system("is_def_eq"); + if (e1 == e2) + return true; + state & s = curr_state(); + expr const & f1 = get_app_fn(e1); + if (is_mref(f1)) { + if (s.is_mref_assigned(f1)) { + return is_def_eq(subst_mref(e1), e2); + } else { + return assign_mref(e1, e2); + } + } + expr const & f2 = get_app_fn(e2); + if (is_mref(f2)) { + if (s.is_mref_assigned(f2)) { + return is_def_eq(e1, subst_mref(e2)); + } else { + return assign_mref(e2, e1); + } + } + expr e1_n = whnf(e1); + expr e2_n = whnf(e2); + if (e1 != e1_n || e2 != e2_n) + return is_def_eq(e1_n, e2_n); + if (e1.kind() == e2.kind()) { + switch (e1.kind()) { + case expr_kind::Lambda: + case expr_kind::Pi: + if (is_def_eq_binding(e1, e2)) + return true; + break; + case expr_kind::Sort: + if (is_def_eq(sort_level(e1), sort_level(e2))) + return true; + break; + case expr_kind::Meta: + case expr_kind::Var: + lean_unreachable(); // LCOV_EXCL_LINE + case expr_kind::Local: + case expr_kind::Macro: + break; + case expr_kind::Constant: + if (const_name(e1) == const_name(e2) && + is_def_eq(const_levels(e1), const_levels(e2))) + return true; + break; + case expr_kind::App: + if (is_def_eq_app(e1, e2)) + return true; + break; + } + } + if (is_def_eq_eta(e1, e2)) + return true; + return is_def_eq_proof_irrel(e1, e2); +} }} diff --git a/src/library/blast/infer_type.h b/src/library/blast/infer_type.h index 77f51c86c..ea9b3f859 100644 --- a/src/library/blast/infer_type.h +++ b/src/library/blast/infer_type.h @@ -12,16 +12,20 @@ namespace blast { /** \brief Put the given expression in weak-head-normal-form with respect to the current state being processed by the blast tactic. */ expr whnf(expr const & e); -/** \brief Return true iff the two expressions are definitionally equal in the - current state being processed by the blast tactic. - - \remark: (potential side-effect) this procedure may update the meta-variable assignment - associated with the current state. */ -bool is_def_eq(expr const & e1, expr const & e2); /** \brief Return the type of the given expression with respect to the current state being processed by the blast tactic. \remark: (potential side-effect) this procedure may update the meta-variable assignment associated with the current state. */ expr infer_type(expr const & e); +/** \brief Return true if \c e is a Proposition */ +bool is_prop(expr const & e); +/** \brief Return true iff the two expressions are definitionally equal in the + current state being processed by the blast tactic. + + \remark: (potential side-effect) this procedure may update the meta-variable assignment + associated with the current state. */ +bool is_def_eq(expr const & e1, expr const & e2); +bool is_def_eq(level const & l1, level const & l2); +bool is_def_eq(levels const & l1, levels const & l2); }} diff --git a/src/library/blast/state.h b/src/library/blast/state.h index 0f852b5cf..390f28d33 100644 --- a/src/library/blast/state.h +++ b/src/library/blast/state.h @@ -66,6 +66,11 @@ public: The context of this metavariable will be all hypotheses occurring in the main branch. */ expr mk_metavar(expr const & type); + bool is_mref_assigned(expr const & e) const { + lean_assert(is_mref(e)); + return m_eassignment.contains(mref_index(e)); + } + /** \brief Add a new hypothesis to the main branch */ expr add_hypothesis(name const & n, expr const & type, optional const & value, optional const & jst) { return m_main.add_hypothesis(n, type, value, jst);