From c5a62f8abba59aebf2e2bc2073c890f6927ddc58 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 30 Oct 2014 22:22:04 -0700 Subject: [PATCH] feat(frontends/lean): insert `!` in calculational proofs when needed This is part of #268 --- src/frontends/lean/CMakeLists.txt | 2 +- src/frontends/lean/calc.cpp | 21 ++--- src/frontends/lean/calc.h | 1 + src/frontends/lean/calc_proof_elaborator.cpp | 82 ++++++++++++++++++++ src/frontends/lean/calc_proof_elaborator.h | 23 ++++++ src/frontends/lean/elaborator.cpp | 20 +++++ src/frontends/lean/elaborator.h | 1 + tests/lean/run/imp_bang.lean | 14 ++++ 8 files changed, 153 insertions(+), 11 deletions(-) create mode 100644 src/frontends/lean/calc_proof_elaborator.cpp create mode 100644 src/frontends/lean/calc_proof_elaborator.h create mode 100644 tests/lean/run/imp_bang.lean diff --git a/src/frontends/lean/CMakeLists.txt b/src/frontends/lean/CMakeLists.txt index 81dbdebd6..48622d37f 100644 --- a/src/frontends/lean/CMakeLists.txt +++ b/src/frontends/lean/CMakeLists.txt @@ -8,7 +8,7 @@ theorem_queue.cpp structure_cmd.cpp info_manager.cpp no_info.cpp extra_info.cpp local_context.cpp choice_iterator.cpp placeholder_elaborator.cpp coercion_elaborator.cpp info_tactic.cpp proof_qed_elaborator.cpp init_module.cpp elaborator_context.cpp -elaborator_exception.cpp) +calc_proof_elaborator.cpp elaborator_exception.cpp) target_link_libraries(lean_frontend ${LEAN_LIBS}) diff --git a/src/frontends/lean/calc.cpp b/src/frontends/lean/calc.cpp index bd3bca6d9..c90781419 100644 --- a/src/frontends/lean/calc.cpp +++ b/src/frontends/lean/calc.cpp @@ -155,6 +155,16 @@ void register_calc_cmds(cmd_table & r) { add_cmd(r, cmd_info("calc_trans", "set the transitivity rule for a pair of operators, this command is relevant for the calculational proof '{...}' notation", calc_trans_cmd)); } +static expr mk_calc_annotation_core(expr const & e) { return mk_annotation(*g_calc_name, e); } +static expr mk_calc_annotation(expr const & pr) { + if (is_by(pr) || is_begin_end_annotation(pr) || is_sorry(pr)) { + return pr; + } else { + return mk_calc_annotation_core(pr); + } +} +bool is_calc_annotation(expr const & e) { return is_annotation(e, *g_calc_name); } + typedef std::tuple calc_pred; typedef pair calc_step; inline name const & pred_op(calc_pred const & p) { return std::get<0>(p); } @@ -198,16 +208,6 @@ static expr mk_op_fn(parser & p, name const & op, unsigned num_placeholders, pos return r; } -static expr mk_calc_annotation(expr const & pr) { - if (is_by(pr) || is_begin_end_annotation(pr) || is_sorry(pr)) { - return pr; - } else { - // TODO(Leo): replace with custom annotation for calc - // that will influence the elaborator - return mk_proof_qed_annotation(pr); - } -} - static void parse_calc_proof(parser & p, buffer const & preds, std::vector & steps) { steps.clear(); auto pos = p.pos(); @@ -310,6 +310,7 @@ void initialize_calc() { g_calc_name = new name("calc"); g_key = new std::string("calc"); calc_ext::initialize(); + register_annotation(*g_calc_name); } void finalize_calc() { diff --git a/src/frontends/lean/calc.h b/src/frontends/lean/calc.h index 7df7cb68c..8d47b04d2 100644 --- a/src/frontends/lean/calc.h +++ b/src/frontends/lean/calc.h @@ -10,6 +10,7 @@ namespace lean { class parser; void register_calc_cmds(cmd_table & r); expr parse_calc(parser & p); +bool is_calc_annotation(expr const & e); void initialize_calc(); void finalize_calc(); } diff --git a/src/frontends/lean/calc_proof_elaborator.cpp b/src/frontends/lean/calc_proof_elaborator.cpp new file mode 100644 index 000000000..cd1eb919f --- /dev/null +++ b/src/frontends/lean/calc_proof_elaborator.cpp @@ -0,0 +1,82 @@ +/* +Copyright (c) 2014 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#include "kernel/free_vars.h" +#include "kernel/instantiate.h" +#include "library/unifier.h" +#include "library/reducible.h" +#include "library/metavar_closure.h" +#include "frontends/lean/util.h" +#include "frontends/lean/local_context.h" +#include "frontends/lean/info_manager.h" + +namespace lean { +/** \brief Create a "choice" constraint that postpones the resolution of a calc proof step. + + By delaying it, we can perform quick fixes such as: + - adding symmetry + - adding ! + - adding subst +*/ +constraint mk_calc_proof_cnstr(environment const & env, local_context const & _ctx, + expr const & m, expr const & _e, + constraint_seq const & cs, unifier_config const & cfg, + info_manager * im, bool relax) { + justification j = mk_failed_to_synthesize_jst(env, m); + auto choice_fn = [=](expr const & meta, expr const & meta_type, substitution const & s, + name_generator const & _ngen) { + local_context ctx = _ctx; + expr e = _e; + name_generator ngen(_ngen); + type_checker_ptr tc(mk_type_checker(env, ngen.mk_child(), relax)); + constraint_seq new_cs = cs; + expr e_type = tc->infer(e, new_cs); + e_type = tc->whnf(e_type, new_cs); + tag g = e.get_tag(); + while (is_pi(e_type)) { + binder_info bi = binding_info(e_type); + if (!bi.is_implicit() && !bi.is_inst_implicit()) { + if (!has_free_var(binding_body(e_type), 0)) { + // if the rest of the type does not reference argument, + // then we also stop consuming arguments + break; + } + } + expr imp_arg = ctx.mk_meta(ngen, some_expr(binding_domain(e_type)), g); + e = mk_app(e, imp_arg, g); + e_type = tc->whnf(instantiate(binding_body(e_type), imp_arg), new_cs); + } + + justification new_j = mk_type_mismatch_jst(e, e_type, meta_type); + if (!tc->is_def_eq(e_type, meta_type, new_j, new_cs)) + throw unifier_exception(new_j, s); + buffer cs_buffer; + new_cs.linearize(cs_buffer); + metavar_closure cls(meta); + cls.add(meta_type); + cls.mk_constraints(s, j, relax, cs_buffer); + cs_buffer.push_back(mk_eq_cnstr(meta, e, j, relax)); + + unifier_config new_cfg(cfg); + new_cfg.m_discard = false; + unify_result_seq seq = unify(env, cs_buffer.size(), cs_buffer.data(), ngen, substitution(), new_cfg); + auto p = seq.pull(); + lean_assert(p); + substitution new_s = p->first.first; + constraints postponed = map(p->first.second, + [&](constraint const & c) { + // we erase internal justifications + return update_justification(c, j); + }); + if (im) + im->instantiate(new_s); + constraints r = cls.mk_constraints(new_s, j, relax); + return append(r, postponed); + }; + bool owner = false; + return mk_choice_cnstr(m, choice_fn, to_delay_factor(cnstr_group::Epilogue), owner, j, relax); +} +} diff --git a/src/frontends/lean/calc_proof_elaborator.h b/src/frontends/lean/calc_proof_elaborator.h new file mode 100644 index 000000000..8509240a7 --- /dev/null +++ b/src/frontends/lean/calc_proof_elaborator.h @@ -0,0 +1,23 @@ +/* +Copyright (c) 2014 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +#include "library/unifier.h" +#include "frontends/lean/info_manager.h" + +namespace lean { +/** \brief Create a "choice" constraint that postpones the resolution of a calc proof step. + + By delaying it, we can perform quick fixes such as: + - adding symmetry + - adding ! + - adding subst +*/ +constraint mk_calc_proof_cnstr(environment const & env, local_context const & ctx, + expr const & m, expr const & e, + constraint_seq const & cs, unifier_config const & cfg, + info_manager * im, bool relax); +} diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index f5afb88eb..c81c78462 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -43,10 +43,12 @@ Author: Leonardo de Moura #include "frontends/lean/choice_iterator.h" #include "frontends/lean/placeholder_elaborator.h" #include "frontends/lean/proof_qed_elaborator.h" +#include "frontends/lean/calc_proof_elaborator.h" #include "frontends/lean/info_tactic.h" #include "frontends/lean/pp_options.h" #include "frontends/lean/begin_end_ext.h" #include "frontends/lean/elaborator_exception.h" +#include "frontends/lean/calc.h" namespace lean { /** \brief 'Choice' expressions (choice e_1 ... e_n) are mapped into a metavariable \c ?m @@ -265,6 +267,8 @@ expr elaborator::visit_expecting_type_of(expr const & e, expr const & t, constra return visit_choice(e, some_expr(t), cs); } else if (is_by(e)) { return visit_by(e, some_expr(t), cs); + } else if (is_calc_annotation(e)) { + return visit_calc_proof(e, some_expr(t), cs); } else if (is_proof_qed_annotation(e)) { return visit_proof_qed(e, some_expr(t), cs); } else { @@ -298,6 +302,20 @@ expr elaborator::visit_by(expr const & e, optional const & t, constraint_s return m; } +expr elaborator::visit_calc_proof(expr const & e, optional const & t, constraint_seq & cs) { + lean_assert(is_calc_annotation(e)); + info_manager * im = nullptr; + if (infom()) + im = &m_pre_info_data; + pair ecs = visit(get_annotation_arg(e)); + expr m = m_full_context.mk_meta(m_ngen, t, e.get_tag()); + register_meta(m); + constraint c = mk_calc_proof_cnstr(env(), m_context, m, ecs.first, ecs.second, m_unifier_config, + im, m_relax_main_opaque); + cs += c; + return m; +} + expr elaborator::visit_proof_qed(expr const & e, optional const & t, constraint_seq & cs) { lean_assert(is_proof_qed_annotation(e)); info_manager * im = nullptr; @@ -801,6 +819,8 @@ expr elaborator::visit_core(expr const & e, constraint_seq & cs) { return visit_let_value(e, cs); } else if (is_by(e)) { return visit_by(e, none_expr(), cs); + } else if (is_calc_annotation(e)) { + return visit_calc_proof(e, none_expr(), cs); } else if (is_proof_qed_annotation(e)) { return visit_proof_qed(e, none_expr(), cs); } else if (is_no_info(e)) { diff --git a/src/frontends/lean/elaborator.h b/src/frontends/lean/elaborator.h index 369dbb0e7..57cd18da4 100644 --- a/src/frontends/lean/elaborator.h +++ b/src/frontends/lean/elaborator.h @@ -103,6 +103,7 @@ class elaborator : public coercion_info_manager { expr visit_choice(expr const & e, optional const & t, constraint_seq & cs); expr visit_by(expr const & e, optional const & t, constraint_seq & cs); expr visit_proof_qed(expr const & e, optional const & t, constraint_seq & cs); + expr visit_calc_proof(expr const & e, optional const & t, constraint_seq & cs); expr add_implict_args(expr e, constraint_seq & cs, bool relax); pair ensure_fun(expr f, constraint_seq & cs); bool has_coercions_from(expr const & a_type); diff --git a/tests/lean/run/imp_bang.lean b/tests/lean/run/imp_bang.lean new file mode 100644 index 000000000..dc621aed8 --- /dev/null +++ b/tests/lean/run/imp_bang.lean @@ -0,0 +1,14 @@ +import algebra.category.basic +open eq eq.ops category functor natural_transformation + +variables {obC obD : Type} {C : category obC} {D : category obD} {F G H : C ⇒ D} + +protected definition compose2 (η : G ⟹ H) (θ : F ⟹ G) : F ⟹ H := +natural_transformation.mk + (λ a, η a ∘ θ a) + (λ a b f, calc + H f ∘ (η a ∘ θ a) = (H f ∘ η a) ∘ θ a : assoc + ... = (η b ∘ G f) ∘ θ a : {naturality η f} + ... = η b ∘ (G f ∘ θ a) : symm !assoc + ... = η b ∘ (θ b ∘ F f) : {naturality θ f} + ... = (η b ∘ θ b) ∘ F f : assoc)