diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp index 7c370856b..ba2809383 100644 --- a/src/kernel/type_checker.cpp +++ b/src/kernel/type_checker.cpp @@ -491,6 +491,19 @@ bool type_checker::is_proposition(expr const & e, context const & ctx) { bool type_checker::is_proposition(expr const & e, context const & ctx, metavar_env const & menv) { return is_proposition(e, ctx, some_menv(menv)); } +bool type_checker::is_flex_proposition(expr e, context ctx, optional const & menv) { + while (is_pi(e)) { + ctx = extend(ctx, abst_name(e), abst_domain(e)); + e = abst_body(e); + } + return is_proposition(e, ctx, menv); +} +bool type_checker::is_flex_proposition(expr const & e, context const & ctx, metavar_env const & menv) { + return is_flex_proposition(e, ctx, some_menv(menv)); +} +bool type_checker::is_flex_proposition(expr const & e, context const & ctx) { + return is_flex_proposition(e, ctx, none_menv()); +} void type_checker::clear() { m_ptr->clear(); } normalizer & type_checker::get_normalizer() { return m_ptr->get_normalizer(); } expr type_check(expr const & e, ro_environment const & env, context const & ctx) { diff --git a/src/kernel/type_checker.h b/src/kernel/type_checker.h index ce84cb11b..697defcab 100644 --- a/src/kernel/type_checker.h +++ b/src/kernel/type_checker.h @@ -77,10 +77,16 @@ public: /** \brief Return true iff \c t1 is convertible to \c t2 in the context \c ctx. */ bool is_convertible(expr const & t1, expr const & t2, context const & ctx = context()); + /** \brief Return true iff \c e is a proposition (i.e., it has type Bool) */ bool is_proposition(expr const & e, context const & ctx, optional const & menv); bool is_proposition(expr const & e, context const & ctx, metavar_env const & menv); bool is_proposition(expr const & e, context const & ctx = context()); + /** \brief Return true iff \c e is a proposition or is a Pi s.t. the range is a flex_proposition */ + bool is_flex_proposition(expr e, context ctx, optional const & menv); + bool is_flex_proposition(expr const & e, context const & ctx, metavar_env const & menv); + bool is_flex_proposition(expr const & e, context const & ctx = context()); + /** \brief Reset internal caches */ void clear(); diff --git a/src/library/tactic/apply_tactic.cpp b/src/library/tactic/apply_tactic.cpp index ff8cef592..c76ae686d 100644 --- a/src/library/tactic/apply_tactic.cpp +++ b/src/library/tactic/apply_tactic.cpp @@ -9,6 +9,7 @@ Author: Leonardo de Moura #include "kernel/environment.h" #include "kernel/instantiate.h" #include "kernel/type_checker.h" +#include "kernel/abstract.h" #include "library/fo_unify.h" #include "library/kernel_bindings.h" #include "library/tactic/goal.h" @@ -43,9 +44,11 @@ static optional apply_tactic(ro_environment const & env, proof_stat // The proof is based on an application of th. // There are two kinds of arguments: // 1) regular arguments computed using unification. - // 2) propostions that generate new subgoals. + // 2) propositions that generate new subgoals. + typedef std::pair proposition_arg; // We use a pair to simulate this "union" type. - typedef list, name>> arg_list; + typedef list, + optional>> arg_list; // We may solve more than one goal. // We store the solved goals using a list of pairs // name, args. Where the 'name' is the name of the solved goal. @@ -66,21 +69,32 @@ static optional apply_tactic(ro_environment const & env, proof_stat for (auto const & mvar : mvars) { expr mvar_sol = apply(*subst, mvar); if (mvar_sol != mvar) { - l = cons(mk_pair(some_expr(mvar_sol), name()), l); + l = cons(mk_pair(some_expr(mvar_sol), optional()), l); th_type_c = instantiate(abst_body(th_type_c), mvar_sol, new_menv); } else { - if (checker.is_proposition(abst_domain(th_type_c), context(), new_menv)) { + expr arg_type = abst_domain(th_type_c); + if (checker.is_flex_proposition(arg_type, context(), new_menv)) { name new_gname(gname, new_goal_idx); new_goal_idx++; - l = cons(mk_pair(none_expr(), new_gname), l); - new_goals_buf.emplace_back(new_gname, update(g, abst_domain(th_type_c))); - th_type_c = instantiate(abst_body(th_type_c), mk_constant(new_gname, abst_domain(th_type_c)), new_menv); + hypotheses hs = g.get_hypotheses(); + update_hypotheses_fn add_hypothesis(hs); + hypotheses extra_hs; + while (is_pi(arg_type)) { + expr d = abst_domain(arg_type); + name n = arg_to_hypothesis_name(env, context(), abst_name(arg_type), d); + n = add_hypothesis(n, d); + extra_hs.emplace_front(n, d); + arg_type = instantiate(abst_body(arg_type), mk_constant(n, d), new_menv); + } + l = cons(mk_pair(none_expr(), some(proposition_arg(new_gname, extra_hs))), l); + new_goals_buf.emplace_back(new_gname, goal(add_hypothesis.get_hypotheses(), arg_type)); + th_type_c = instantiate(abst_body(th_type_c), mk_constant(new_gname, arg_type), new_menv); } else { // we have to create a new metavar in menv // since we do not have a substitution for mvar, and // it is not a proposition - expr new_m = new_menv->mk_metavar(context(), some_expr(abst_domain(th_type_c))); - l = cons(mk_pair(some_expr(new_m), name()), l); + expr new_m = new_menv->mk_metavar(context(), some_expr(arg_type)); + l = cons(mk_pair(some_expr(new_m), optional()), l); th_type_c = instantiate(abst_body(th_type_c), 1, &new_m, new_menv); } } @@ -108,8 +122,12 @@ static optional apply_tactic(ro_environment const & env, proof_stat // TODO(Leo): decide if we instantiate the metavars in the end or not. args.push_back(*arg); } else { - name const & subgoal_name = p2.second; - args.push_back(find(m, subgoal_name)); + proposition_arg const & parg = *(p2.second); + name const & subgoal_name = parg.first; + expr pr = find(m, subgoal_name); + for (auto p : parg.second) + pr = Fun(p.first, p.second, pr); + args.push_back(pr); new_m.erase(subgoal_name); } } diff --git a/src/library/tactic/goal.cpp b/src/library/tactic/goal.cpp index 6cb8a8202..355fe5f1f 100644 --- a/src/library/tactic/goal.cpp +++ b/src/library/tactic/goal.cpp @@ -18,6 +18,33 @@ Author: Leonardo de Moura namespace lean { +name mk_unique_hypothesis_name(hypotheses const & hs, name const & suggestion) { + name n = suggestion; + unsigned i = 0; + // TODO(Leo): investigate if this method is a performance bottleneck + while (true) { + bool ok = true; + for (auto const & p : hs) { + if (is_prefix_of(n, p.first)) { + ok = false; + break; + } + } + if (ok) { + return n; + } else { + i++; + n = name(suggestion, i); + } + } +} + +name update_hypotheses_fn::operator()(name const & suggestion, expr const & t) { + name n = mk_unique_hypothesis_name(m_hypotheses, suggestion); + m_hypotheses.emplace_front(n, t); + return n; +} + goal::goal(hypotheses const & hs, expr const & c):m_hypotheses(hs), m_conclusion(c) {} format goal::pp(formatter const & fmt, options const & opts) const { @@ -43,24 +70,7 @@ format goal::pp(formatter const & fmt, options const & opts) const { } name goal::mk_unique_hypothesis_name(name const & suggestion) const { - name n = suggestion; - unsigned i = 0; - // TODO(Leo): investigate if this method is a performance bottleneck - while (true) { - bool ok = true; - for (auto const & p : m_hypotheses) { - if (is_prefix_of(n, p.first)) { - ok = false; - break; - } - } - if (ok) { - return n; - } else { - i++; - n = name(suggestion, i); - } - } + return ::lean::mk_unique_hypothesis_name(m_hypotheses, suggestion); } goal_proof_fn::goal_proof_fn(std::vector && consts): diff --git a/src/library/tactic/goal.h b/src/library/tactic/goal.h index a0e226107..ee1dcafd9 100644 --- a/src/library/tactic/goal.h +++ b/src/library/tactic/goal.h @@ -28,6 +28,20 @@ public: typedef std::pair hypothesis; typedef list hypotheses; + +class update_hypotheses_fn { + hypotheses m_hypotheses; +public: + update_hypotheses_fn(hypotheses const & hs):m_hypotheses(hs) {} + hypotheses const & get_hypotheses() const { return m_hypotheses; } + /** + \brief Add a new hypothesis, the name \c n is a suggestion. + The method checks if the given name collides with an existing name. + It returns the actual name used. + */ + name operator()(name const & n, expr const & t); +}; + class goal { hypotheses m_hypotheses; expr m_conclusion; diff --git a/src/library/tactic/proof_state.cpp b/src/library/tactic/proof_state.cpp index 658231eba..ab158985a 100644 --- a/src/library/tactic/proof_state.cpp +++ b/src/library/tactic/proof_state.cpp @@ -88,16 +88,19 @@ void proof_state::get_goal_names(name_set & r) const { } } +name arg_to_hypothesis_name(ro_environment const & env, context const & ctx, name const & n, expr const & d) { + if (is_default_arrow_var_name(n) && is_proposition(d, env, ctx)) + return name("H"); + else + return n; +} + static name g_main("main"); proof_state to_proof_state(ro_environment const & env, context ctx, expr t) { list> extra_binders; while (is_pi(t)) { - name vname; - if (is_default_arrow_var_name(abst_name(t)) && is_proposition(abst_domain(t), env, ctx)) - vname = name("H"); - else - vname = abst_name(t); + name vname = arg_to_hypothesis_name(env, ctx, abst_name(t), abst_domain(t)); extra_binders.emplace_front(vname, abst_domain(t)); ctx = extend(ctx, vname, abst_domain(t)); t = abst_body(t); diff --git a/src/library/tactic/proof_state.h b/src/library/tactic/proof_state.h index 6ef79f656..a5dee697c 100644 --- a/src/library/tactic/proof_state.h +++ b/src/library/tactic/proof_state.h @@ -120,6 +120,12 @@ goals map_goals(proof_state const & s, F && f) { io_state_stream const & operator<<(io_state_stream const & out, proof_state & s); +/** + \brief Return a name based on \c n that is suitable to be used as a hypothesis name + It basically renames \c n to 'H' if \c d is a proposition and \c n is the default arrow binder name. +*/ +name arg_to_hypothesis_name(ro_environment const & env, context const & ctx, name const & n, expr const & d); + UDATA_DEFS_CORE(goals) UDATA_DEFS(proof_state) void open_proof_state(lua_State * L); diff --git a/tests/lean/apply_tac2.lean b/tests/lean/apply_tac2.lean new file mode 100644 index 000000000..878349912 --- /dev/null +++ b/tests/lean/apply_tac2.lean @@ -0,0 +1,7 @@ +Check @Discharge +Theorem T (a b : Bool) : a => b => b => a. + apply Discharge. + apply Discharge. + apply Discharge. + assumption. + done. \ No newline at end of file diff --git a/tests/lean/apply_tac2.lean.expected.out b/tests/lean/apply_tac2.lean.expected.out new file mode 100644 index 000000000..c9da3cd33 --- /dev/null +++ b/tests/lean/apply_tac2.lean.expected.out @@ -0,0 +1,4 @@ + Set: pp::colors + Set: pp::unicode +@Discharge : Π (a b : Bool), (a → b) → (a ⇒ b) + Proved: T