From 59755289e46f196f22bc8e1a7d104f9470b34909 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 5 Jul 2014 15:52:40 -0700 Subject: [PATCH] =?UTF-8?q?feat(library/unifier):=20case=20split=20on=20co?= =?UTF-8?q?nstraints=20of=20the=20form=20(f=20...)=20=3D=3F=3D=20(f=20...)?= =?UTF-8?q?,=20where=20f=20can=20be=20unfolded,=20and=20there=20are=20meta?= =?UTF-8?q?variables=20in=20the=20arguments?= Signed-off-by: Leonardo de Moura --- library/standard/bit.lean | 21 +++--- src/kernel/converter.cpp | 90 +++++++++++++++-------- src/kernel/converter.h | 5 +- src/library/unifier.cpp | 131 +++++++++++++++++++++++----------- src/library/unifier.h | 10 +-- src/tests/library/unifier.cpp | 2 +- tests/lean/run/is_nil.lean | 47 ++++++++++++ tests/lean/run/tactic23.lean | 8 +-- tests/lean/run/trick.lean | 33 +++++++++ tests/lua/tc_bug1.lua | 1 - 10 files changed, 249 insertions(+), 99 deletions(-) create mode 100644 tests/lean/run/is_nil.lean create mode 100644 tests/lean/run/trick.lean diff --git a/library/standard/bit.lean b/library/standard/bit.lean index 778517d73..227b14496 100644 --- a/library/standard/bit.lean +++ b/library/standard/bit.lean @@ -24,20 +24,15 @@ theorem cond_b1 {A : Type} (t e : A) : cond b1 t e = t definition bor (a b : bit) := bit_rec (bit_rec b0 b1 b) b1 a -section - -- create section for setting temporary configuration option - set_option unifier.unfold_opaque true +theorem bor_b1_left (a : bit) : bor b1 a = b1 +:= refl (bor b1 a) - theorem bor_b1_left (a : bit) : bor b1 a = b1 - := refl (bor b1 a) +theorem bor_b1_right (a : bit) : bor a b1 = b1 +:= bit_rec (refl (bor b0 b1)) (refl (bor b1 b1)) a - theorem bor_b1_right (a : bit) : bor a b1 = b1 - := bit_rec (refl (bor b0 b1)) (refl (bor b1 b1)) a +theorem bor_b0_left (a : bit) : bor b0 a = a +:= bit_rec (refl (bor b0 b0)) (refl (bor b0 b1)) a - theorem bor_b0_left (a : bit) : bor b0 a = a - := bit_rec (refl (bor b0 b0)) (refl (bor b0 b1)) a - - theorem bor_b0_right (a : bit) : bor a b0 = a - := bit_rec (refl (bor b0 b0)) (refl (bor b1 b0)) a -end +theorem bor_b0_right (a : bit) : bor a b0 = a +:= bit_rec (refl (bor b0 b0)) (refl (bor b1 b0)) a end diff --git a/src/kernel/converter.cpp b/src/kernel/converter.cpp index fbb234f18..1c42e956e 100644 --- a/src/kernel/converter.cpp +++ b/src/kernel/converter.cpp @@ -42,6 +42,29 @@ bool is_opaque(declaration const & d, name_set const & extra_opaque, optional is_delta_core(environment const & env, expr const & e, name_set const & extra_opaque, optional const & mod_idx) { + if (is_constant(e)) { + if (auto d = env.find(const_name(e))) + if (d->is_definition() && !is_opaque(*d, extra_opaque, mod_idx)) + return d; + } + return none_declaration(); +} + +/** + \brief Return some definition \c d iff \c e is a target for delta-reduction, and the given definition is the one + to be expanded. +*/ +optional is_delta(environment const & env, expr const & e, name_set const & extra_opaque, optional const & mod_idx) { + return is_delta_core(env, get_app_fn(e), extra_opaque, mod_idx); +} + +static optional g_opt_main_module_idx(g_main_module_idx); +optional is_delta(environment const & env, expr const & e, name_set const & extra_opaque) { + return is_delta(env, e, extra_opaque, g_opt_main_module_idx); +} + static no_delayed_justification g_no_delayed_jst; bool converter::is_def_eq(expr const & t, expr const & s, type_checker & c) { return is_def_eq(t, s, c, g_no_delayed_jst); @@ -71,7 +94,8 @@ struct default_converter : public converter { expr_struct_map m_whnf_cache; default_converter(environment const & env, optional mod_idx, bool memoize, name_set const & extra_opaque): - m_env(env), m_module_idx(mod_idx), m_memoize(memoize), m_extra_opaque(extra_opaque) {} + m_env(env), m_module_idx(mod_idx), m_memoize(memoize), m_extra_opaque(extra_opaque) { + } optional expand_macro(expr const & m, type_checker & c) { lean_assert(is_macro(m)); @@ -204,21 +228,13 @@ struct default_converter : public converter { } } - /** \brief Auxiliary method for \c is_delta */ - optional is_delta_core(expr const & e) { - if (is_constant(e)) { - if (auto d = m_env.find(const_name(e))) - if (d->is_definition() && !is_opaque(*d)) - return d; - } - return none_declaration(); - } - /** \brief Return some definition \c d iff \c e is a target for delta-reduction, and the given definition is the one to be expanded. */ - optional is_delta(expr const & e) { return is_delta_core(get_app_fn(e)); } + optional is_delta(expr const & e) { + return ::lean::is_delta(m_env, get_app_fn(e), m_extra_opaque, m_module_idx); + } /** \brief Weak head normal form core procedure that perform delta reduction for non-opaque constants with @@ -386,20 +402,24 @@ struct default_converter : public converter { s_n = whnf_core(unfold_names(s_n, d_t->get_weight() + 1), c); } else { lean_assert(d_t && d_s && d_t->get_weight() == d_s->get_weight()); - // If t_n and s_n are both applications of the same (non-opaque) definition, - // then we try to check if their arguments are definitionally equal. - // If they are, then t_n and s_n must be definitionally equal, and we can - // skip the delta-reduction step. - // We only apply the optimization if t_n and s_n do not contain metavariables. - // In this way we don't have to backtrack constraints if the optimization fail. - if (is_app(t_n) && is_app(s_n) && - is_eqp(*d_t, *d_s) && // same definition - !has_metavar(t_n) && - !has_metavar(s_n) && - !is_opaque(*d_t) && // if d_t is opaque, we don't need to try this optimization - d_t->use_conv_opt() && // the flag use_conv_opt() can be used to disable this optimization - is_def_eq_args(t_n, s_n, c, jst)) { - return true; + if (is_app(t_n) && is_app(s_n) && is_eqp(*d_t, *d_s)) { + // If t_n and s_n are both applications of the same (non-opaque) definition, + if (has_expr_metavar(t_n) || has_expr_metavar(s_n)) { + // We let the unifier deal with cases such as + // (f ...) =?= (f ...) + break; + } else { + // Optimization: + // We try to check if their arguments are definitionally equal. + // If they are, then t_n and s_n must be definitionally equal, and we can + // skip the delta-reduction step. + // If the flag use_conv_opt() is not true, then we skip this optimization + if (!is_opaque(*d_t) && d_t->use_conv_opt()) { + type_checker::scope scope(c); + if (is_def_eq_args(t_n, s_n, c, jst)) + return true; + } + } } t_n = whnf_core(unfold_names(t_n, d_t->get_weight() - 1), c); s_n = whnf_core(unfold_names(s_n, d_s->get_weight() - 1), c); @@ -428,8 +448,16 @@ struct default_converter : public converter { is_def_eq(mlocal_type(t_n), mlocal_type(s_n), c, jst)) return true; + optional d_t, d_s; + bool delay_check = false; + if (has_expr_metavar(t_n) || has_expr_metavar(s_n)) { + d_t = is_delta(t_n); + d_s = is_delta(s_n); + delay_check = d_t && d_s && is_eqp(*d_t, *d_s); + } + // At this point, t_n and s_n are in weak head normal form (modulo meta-variables and proof irrelevance) - if (is_app(t_n) && is_app(s_n)) { + if (!delay_check && is_app(t_n) && is_app(s_n)) { type_checker::scope scope(c); buffer t_args; buffer s_args; @@ -476,6 +504,11 @@ struct default_converter : public converter { return true; } + if (delay_check) { + add_cnstr(c, mk_eq_cnstr(t_n, s_n, jst.get())); + return true; + } + return false; } @@ -488,7 +521,8 @@ std::unique_ptr mk_default_converter(environment const & env, optiona bool memoize, name_set const & extra_opaque) { return std::unique_ptr(new default_converter(env, mod_idx, memoize, extra_opaque)); } -std::unique_ptr mk_default_converter(environment const & env, bool unfold_opaque_main, bool memoize, name_set const & extra_opaque) { +std::unique_ptr mk_default_converter(environment const & env, bool unfold_opaque_main, bool memoize, + name_set const & extra_opaque) { if (unfold_opaque_main) return mk_default_converter(env, optional(0), memoize, extra_opaque); else diff --git a/src/kernel/converter.h b/src/kernel/converter.h index 466e90f53..e2728d814 100644 --- a/src/kernel/converter.h +++ b/src/kernel/converter.h @@ -26,10 +26,11 @@ public: std::unique_ptr mk_dummy_converter(); std::unique_ptr mk_default_converter(environment const & env, optional mod_idx = optional(), - bool memoize = true, - name_set const & extra_opaque = name_set()); + bool memoize = true, name_set const & extra_opaque = name_set()); std::unique_ptr mk_default_converter(environment const & env, bool unfold_opaque_main, bool memoize = true, name_set const & extra_opaque = name_set()); bool is_opaque(declaration const & d, name_set const & extra_opaque, optional const & mod_idx); +optional is_delta(environment const & env, expr const & e, name_set const & extra_opaque, optional const & mod_idx); +optional is_delta(environment const & env, expr const & e, name_set const & extra_opaque = name_set()); } diff --git a/src/library/unifier.cpp b/src/library/unifier.cpp index 9b8f133fb..b3cb54155 100644 --- a/src/library/unifier.cpp +++ b/src/library/unifier.cpp @@ -24,10 +24,7 @@ Author: Leonardo de Moura namespace lean { static name g_unifier_max_steps {"unifier", "max_steps"}; RegisterUnsignedOption(g_unifier_max_steps, LEAN_DEFAULT_UNIFIER_MAX_STEPS, "(unifier) maximum number of steps"); -static name g_unifier_unfold_opaque{"unifier", "unfold_opaque"}; -RegisterBoolOption(g_unifier_unfold_opaque, LEAN_DEFAULT_UNIFIER_UNFOLD_OPAQUE, "(unifier) unfold opaque definitions from the current module"); unsigned get_unifier_max_steps(options const & opts) { return opts.get_unsigned(g_unifier_max_steps, LEAN_DEFAULT_UNIFIER_MAX_STEPS); } -bool get_unifier_unfold_opaque(options const & opts) { return opts.get_bool(g_unifier_unfold_opaque, LEAN_DEFAULT_UNIFIER_UNFOLD_OPAQUE); } // If \c e is a metavariable ?m or a term of the form (?m l_1 ... l_n) where // l_1 ... l_n are distinct local variables, then return ?m, and store l_1 ... l_n in args. @@ -367,10 +364,10 @@ struct unifier_fn { virtual bool next(unifier_fn & u) { return u.next_lazy_constraints_case_split(*this); } }; - struct ho_case_split : public case_split { + struct simple_case_split : public case_split { list m_tail; - ho_case_split(unifier_fn & u, list const & tail):case_split(u), m_tail(tail) {} - virtual bool next(unifier_fn & u) { return u.next_ho_case_split(*this); } + simple_case_split(unifier_fn & u, list const & tail):case_split(u), m_tail(tail) {} + virtual bool next(unifier_fn & u) { return u.next_simple_case_split(*this); } }; case_split_stack m_case_splits; @@ -378,9 +375,9 @@ struct unifier_fn { unifier_fn(environment const & env, unsigned num_cs, constraint const * cs, name_generator const & ngen, substitution const & s, - bool use_exception, unsigned max_steps, bool unfold_opaque): + bool use_exception, unsigned max_steps): m_env(env), m_ngen(ngen), m_subst(s), m_plugin(get_unifier_plugin(env)), - m_tc(env, m_ngen.mk_child(), mk_default_converter(env, unfold_opaque)), + m_tc(env, m_ngen.mk_child(), mk_default_converter(env, true)), m_use_exception(use_exception), m_max_steps(max_steps), m_num_steps(0) { m_next_assumption_idx = 0; m_next_cidx = 0; @@ -525,10 +522,10 @@ struct unifier_fn { } } - enum status { Assigned, Failed, Continue }; + enum status { Solved, Failed, Continue }; /** \brief Process constraints of the form lhs =?= rhs where lhs is of the form ?m or (?m l_1 .... l_n), - where all \c l_i are distinct local variables. In this case, the method returns Assigned, if the method assign succeeds. + where all \c l_i are distinct local variables. In this case, the method returns Solved, if the method assign succeeds. The method returns \c Failed if \c rhs contains ?m, or it contains a local constant not in {l_1, ..., l_n}. Otherwise, it returns \c Continue. */ @@ -548,7 +545,7 @@ struct unifier_fn { case l_true: lean_assert(!m_subst.is_assigned(*m)); if (assign(*m, lambda_abstract_locals(rhs, locals), j)) { - return Assigned; + return Solved; } else { return Failed; } @@ -556,6 +553,20 @@ struct unifier_fn { lean_unreachable(); // LCOV_EXCL_LINE } + optional is_delta(expr const & e) { return ::lean::is_delta(m_env, e); } + + /** \brief Return true if lhs and rhs are of the form (f ...) where f can be expanded */ + bool is_eq_deltas(expr const & lhs, expr const & rhs) { + auto lhs_d = is_delta(lhs); + auto rhs_d = is_delta(rhs); + return lhs_d && rhs_d && is_eqp(*lhs_d, *rhs_d); + } + + /** \brief Return true if the constraint is of the form (f ...) =?= (f ...), where f can be expanded. */ + bool is_delta_cnstr(constraint const & c) { + return is_eq_cnstr(c) && is_eq_deltas(cnstr_lhs_expr(c), cnstr_rhs_expr(c)); + } + /** \brief Process an equality constraints. */ bool process_eq_constraint(constraint const & c) { lean_assert(is_eq_cnstr(c)); @@ -577,13 +588,9 @@ struct unifier_fn { // Handle higher-order pattern matching. status st = process_metavar_eq(lhs, rhs, new_jst); - if (st != Continue) return st == Assigned; + if (st != Continue) return st == Solved; st = process_metavar_eq(rhs, lhs, new_jst); - if (st != Continue) return st == Assigned; - - // Make sure lhs/rhs are in weak-head-normal-form - rhs = m_tc.whnf(rhs); - lhs = m_tc.whnf(lhs); + if (st != Continue) return st == Solved; // If lhs or rhs were updated, then invoke is_def_eq again. if (lhs != cnstr_lhs_expr(c) || rhs != cnstr_rhs_expr(c)) { @@ -591,7 +598,10 @@ struct unifier_fn { return is_def_eq(lhs, rhs, new_jst); } - if (m_plugin->delay_constraint(m_tc, c)) { + if (is_eq_deltas(lhs, rhs)) { + // we need to create a backtracking point for this one + add_cnstr(c, &unassigned_lvls, &unassigned_exprs, cnstr_group::Basic); + } else if (m_plugin->delay_constraint(m_tc, c)) { add_cnstr(c, &unassigned_lvls, &unassigned_exprs, cnstr_group::PluginDelayed); } else if (is_meta(lhs) && is_meta(rhs)) { // flex-flex constraints are delayed the most. @@ -624,7 +634,7 @@ struct unifier_fn { } lean_assert(!m_subst.is_assigned(lhs)); if (assign(lhs, rhs, j)) { - return Assigned; + return Solved; } else { return Failed; } @@ -659,9 +669,9 @@ struct unifier_fn { } status st = process_metavar_eq(lhs, rhs, new_jst); - if (st != Continue) return st == Assigned; + if (st != Continue) return st == Solved; st = process_metavar_eq(rhs, lhs, new_jst); - if (st != Continue) return st == Assigned; + if (st != Continue) return st == Solved; if (lhs != cnstr_lhs_level(c) || rhs != cnstr_rhs_level(c)) { constraint new_c = mk_level_eq_cnstr(lhs, rhs, new_jst); @@ -809,7 +819,7 @@ struct unifier_fn { return process_lazy_constraints(alts, mk_composite1(c.get_justification(), m_type_jst.second)); } - bool next_ho_case_split(ho_case_split & cs) { + bool next_simple_case_split(simple_case_split & cs) { if (!is_nil(cs.m_tail)) { cs.restore_state(*this); lean_assert(!in_conflict()); @@ -823,6 +833,53 @@ struct unifier_fn { } } + /** + \brief Solve constraints of the form (f a_1 ... a_n) =?= (f b_1 ... b_n) where f can be expanded. + We consider two possible solutions: + 1) a_1 =?= b_1, ..., a_n =?= b_n + 2) t =?= s, where t and s are the terms we get after expanding f + */ + bool process_delta(constraint const & c) { + lean_assert(is_delta_cnstr(c)); + expr const & lhs = cnstr_lhs_expr(c); + expr const & rhs = cnstr_rhs_expr(c); + buffer lhs_args, rhs_args; + justification j = c.get_justification(); + expr lhs_fn = get_app_rev_args(lhs, lhs_args); + expr rhs_fn = get_app_rev_args(rhs, rhs_args); + declaration d = *m_env.find(const_name(lhs_fn)); + levels lhs_lvls = const_levels(lhs_fn); + levels rhs_lvls = const_levels(lhs_fn); + if (lhs_args.size() != rhs_args.size() || + length(lhs_lvls) != length(rhs_lvls) || + length(d.get_univ_params()) != length(lhs_lvls)) { + // the constraint is not well-formed, this can happen when users are abusing the API + return false; + } + buffer cs_buffer; + while (!is_nil(lhs_lvls)) { + cs_buffer.push_back(mk_level_eq_cnstr(head(lhs_lvls), head(rhs_lvls), j)); + lhs_lvls = tail(lhs_lvls); + rhs_lvls = tail(rhs_lvls); + } + unsigned i = lhs_args.size(); + while (i > 0) { + --i; + cs_buffer.push_back(mk_eq_cnstr(lhs_args[i], rhs_args[i], j)); + } + constraints cs1 = to_list(cs_buffer.begin(), cs_buffer.end()); + + expr lhs_fn_val = instantiate_univ_params(d.get_value(), d.get_univ_params(), const_levels(lhs_fn)); + expr rhs_fn_val = instantiate_univ_params(d.get_value(), d.get_univ_params(), const_levels(rhs_fn)); + expr t = apply_beta(lhs_fn_val, lhs_args.size(), lhs_args.data()); + expr s = apply_beta(rhs_fn_val, rhs_args.size(), rhs_args.data()); + constraints cs2(mk_eq_cnstr(t, s, j)); + + justification a = mk_assumption_justification(m_next_assumption_idx); + add_case_split(std::unique_ptr(new simple_case_split(*this, list(cs2)))); + return process_constraints(cs1, a); + } + /** \brief Return true iff \c c is a flex-rigid constraint. */ static bool is_flex_rigid(constraint const & c) { if (!is_eq_cnstr(c)) @@ -1043,7 +1100,7 @@ struct unifier_fn { return process_constraints(alts[0], justification()); } else { justification a = mk_assumption_justification(m_next_assumption_idx); - add_case_split(std::unique_ptr(new ho_case_split(*this, to_list(alts.begin() + 1, alts.end())))); + add_case_split(std::unique_ptr(new simple_case_split(*this, to_list(alts.begin() + 1, alts.end())))); return process_constraints(alts[0], a); } } @@ -1082,6 +1139,8 @@ struct unifier_fn { m_cnstrs.erase_min(); if (is_choice_cnstr(c)) return process_choice_constraint(c); + else if (is_delta_cnstr(c)) + return process_delta(c); else if (is_flex_rigid(c)) return process_flex_rigid(c); else if (is_flex_flex(c)) @@ -1145,37 +1204,29 @@ lazy_list unify(std::shared_ptr u) { } lazy_list unify(environment const & env, unsigned num_cs, constraint const * cs, name_generator const & ngen, - bool use_exception, unsigned max_steps, bool unfold_opaque) { - return unify(std::make_shared(env, num_cs, cs, ngen, substitution(), use_exception, max_steps, unfold_opaque)); + bool use_exception, unsigned max_steps) { + return unify(std::make_shared(env, num_cs, cs, ngen, substitution(), use_exception, max_steps)); } lazy_list unify(environment const & env, unsigned num_cs, constraint const * cs, name_generator const & ngen, bool use_exception, options const & o) { - return unify(env, num_cs, cs, ngen, use_exception, get_unifier_max_steps(o), get_unifier_unfold_opaque(o)); + return unify(env, num_cs, cs, ngen, use_exception, get_unifier_max_steps(o)); } lazy_list unify(environment const & env, expr const & lhs, expr const & rhs, name_generator const & ngen, substitution const & s, - unsigned max_steps, bool unfold_opaque) { - name_generator new_ngen(ngen); - type_checker tc(env, new_ngen.mk_child()); + unsigned max_steps) { + auto u = std::make_shared(env, 0, nullptr, ngen, s, false, max_steps); expr _lhs = s.instantiate(lhs); expr _rhs = s.instantiate(rhs); - if (!tc.is_def_eq(_lhs, _rhs)) + if (!u->m_tc.is_def_eq(_lhs, _rhs)) return lazy_list(); - buffer cs; - while (auto c = tc.next_cnstr()) { - cs.push_back(*c); - } - if (cs.empty()) { - return lazy_list(s); - } else { - return unify(std::make_shared(env, cs.size(), cs.data(), ngen, s, false, max_steps, unfold_opaque)); - } + else + return unify(u); } lazy_list unify(environment const & env, expr const & lhs, expr const & rhs, name_generator const & ngen, substitution const & s, options const & o) { - return unify(env, lhs, rhs, ngen, s, get_unifier_max_steps(o), get_unifier_unfold_opaque(o)); + return unify(env, lhs, rhs, ngen, s, get_unifier_max_steps(o)); } static int unify_simple(lua_State * L) { diff --git a/src/library/unifier.h b/src/library/unifier.h index b88647fd5..2b4a1f7bd 100644 --- a/src/library/unifier.h +++ b/src/library/unifier.h @@ -19,10 +19,6 @@ Author: Leonardo de Moura #define LEAN_DEFAULT_UNIFIER_MAX_STEPS 10000 #endif -#ifndef LEAN_DEFAULT_UNIFIER_UNFOLD_OPAQUE -#define LEAN_DEFAULT_UNIFIER_UNFOLD_OPAQUE false -#endif - namespace lean { unsigned get_unifier_max_steps(options const & opts); bool get_unifier_unfold_opaque(options const & opts); @@ -41,13 +37,11 @@ std::pair unify_simple(substitution const & s, level std::pair unify_simple(substitution const & s, constraint const & c); lazy_list unify(environment const & env, unsigned num_cs, constraint const * cs, name_generator const & ngen, - bool use_exception = true, unsigned max_steps = LEAN_DEFAULT_UNIFIER_MAX_STEPS, - bool unfold_opaque = LEAN_DEFAULT_UNIFIER_UNFOLD_OPAQUE); + bool use_exception = true, unsigned max_steps = LEAN_DEFAULT_UNIFIER_MAX_STEPS); lazy_list unify(environment const & env, unsigned num_cs, constraint const * cs, name_generator const & ngen, bool use_exception, options const & o); lazy_list unify(environment const & env, expr const & lhs, expr const & rhs, name_generator const & ngen, - substitution const & s = substitution(), unsigned max_steps = LEAN_DEFAULT_UNIFIER_MAX_STEPS, - bool unfold_opaque = LEAN_DEFAULT_UNIFIER_UNFOLD_OPAQUE); + substitution const & s = substitution(), unsigned max_steps = LEAN_DEFAULT_UNIFIER_MAX_STEPS); lazy_list unify(environment const & env, expr const & lhs, expr const & rhs, name_generator const & ngen, substitution const & s, options const & o); diff --git a/src/tests/library/unifier.cpp b/src/tests/library/unifier.cpp index 8c6af51da..0495475b5 100644 --- a/src/tests/library/unifier.cpp +++ b/src/tests/library/unifier.cpp @@ -19,7 +19,7 @@ static void tst1() { expr t1 = f(m, m); expr t2 = f(a, b); auto r = unify(env, t1, t2, ngen); - lean_assert(r.is_nil()); + lean_assert(!r.pull()); } int main() { diff --git a/tests/lean/run/is_nil.lean b/tests/lean/run/is_nil.lean new file mode 100644 index 000000000..9e39e9ee0 --- /dev/null +++ b/tests/lean/run/is_nil.lean @@ -0,0 +1,47 @@ +import standard +using tactic + +inductive list (A : Type) : Type := +| nil {} : list A +| cons : A → list A → list A + +definition is_nil {A : Type} (l : list A) : Bool +:= list_rec true (fun h t r, false) l + +theorem is_nil_nil (A : Type) : is_nil (@nil A) +:= eqt_elim (refl true) + +theorem cons_ne_nil {A : Type} (a : A) (l : list A) : ¬ cons a l = nil +:= not_intro (assume H : cons a l = nil, + absurd + (calc true = is_nil (@nil A) : refl _ + ... = is_nil (cons a l) : { symm H } + ... = false : refl _) + true_ne_false) + +theorem T : is_nil (@nil Bool) +:= by apply is_nil_nil + +(* +local list = Const("list", {1})(Bool) +local isNil = Const("is_nil", {1})(Bool) +local Nil = Const("nil", {1})(Bool) +local m = mk_metavar("m", list) +print(isNil(Nil)) +print(isNil(m)) + + +function test_unify(env, m, lhs, rhs, num_s) + print(tostring(lhs) .. " =?= " .. tostring(rhs) .. ", expected: " .. tostring(num_s)) + local ss = unify(env, lhs, rhs, name_generator(), substitution()) + local n = 0 + for s in ss do + print("solution: " .. tostring(s:instantiate(m))) + n = n + 1 + end + if num_s ~= n then print("n: " .. n) end + assert(num_s == n) +end +print("=====================") +test_unify(get_env(), m, isNil(Nil), isNil(m), 2) +*) \ No newline at end of file diff --git a/tests/lean/run/tactic23.lean b/tests/lean/run/tactic23.lean index 8e3ef3530..4196816a3 100644 --- a/tests/lean/run/tactic23.lean +++ b/tests/lean/run/tactic23.lean @@ -32,9 +32,5 @@ theorem T1 {p : nat → Bool} {a : nat } (H : p (a+2)) : ∃ x, p (succ x) definition is_zero (n : nat) := nat_rec true (λ n r, false) n -section - set_option unifier.unfold_opaque true - - theorem T2 : ∃ a, (is_zero a) = true - := by apply exists_intro; apply refl -end \ No newline at end of file +theorem T2 : ∃ a, (is_zero a) = true +:= by apply exists_intro; apply refl diff --git a/tests/lean/run/trick.lean b/tests/lean/run/trick.lean new file mode 100644 index 000000000..20bac83ef --- /dev/null +++ b/tests/lean/run/trick.lean @@ -0,0 +1,33 @@ +import standard +using num + +definition proj1 (x : num) (y : num) := x +definition One := 1 + +(* +local num = Const({"num", "num"}) +local m = mk_metavar("m", num) +local proj1 = Const("proj1") +local zero = Const({"num", "zero"}) +local one = Const("One") +local t1 = proj1(m, one) +local t2 = proj1(m, zero) + +function test_unify(env, m, cs, num_s) + local ss = unify(env, cs, name_generator()) + local n = 0 + for s in ss do + print("solution: " .. tostring(s:instantiate(m))) + n = n + 1 + end + if num_s ~= n then print("n: " .. n) end + assert(num_s == n) +end + +local env = get_env() + +print("===============") +test_unify(env, m, { mk_eq_cnstr(proj1(m, one), proj1(zero, zero)) }, 1) +print("===============") +test_unify(env, m, { mk_eq_cnstr(proj1(m, one), proj1(zero, m)) }, 1) +*) diff --git a/tests/lua/tc_bug1.lua b/tests/lua/tc_bug1.lua index f5f1b9dbd..233981b10 100644 --- a/tests/lua/tc_bug1.lua +++ b/tests/lua/tc_bug1.lua @@ -34,7 +34,6 @@ local ng = name_generator("foo") local tc = type_checker(env, ng) local m1 = mk_metavar("m1", Bool) print("before is_def_eq") -assert(not tc:is_def_eq(and_intro(m1, q(a)), and_intro(q(a), q(b)))) assert(not tc:next_cnstr()) local tc = type_checker(env, ng) assert(tc:is_def_eq(foo_intro(m1, q(a), q(a), Ax1), foo_intro(q(a), q(a), q(a), Ax2)))