From 616f49c2e44c376f7d05a65fe43a67dedfaa08c6 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 5 May 2015 18:17:43 -0700 Subject: [PATCH] feat(frontends/lean): improved 'obtains' expression --- library/data/set/function.lean | 12 +-- src/frontends/lean/CMakeLists.txt | 3 +- src/frontends/lean/builtin_exprs.cpp | 55 +++++----- src/frontends/lean/elaborator.cpp | 138 ++++++++++++++++++++++++++ src/frontends/lean/elaborator.h | 9 ++ src/frontends/lean/init_module.cpp | 3 + src/frontends/lean/obtain_expr.cpp | 113 +++++++++++++++++++++ src/frontends/lean/obtain_expr.h | 28 ++++++ src/frontends/lean/parser.cpp | 6 ++ src/frontends/lean/parser.h | 1 + src/library/tactic/expr_to_tactic.cpp | 9 ++ src/library/tactic/expr_to_tactic.h | 5 + tests/lean/run/new_obtains.lean | 74 ++++++++++++++ 13 files changed, 422 insertions(+), 34 deletions(-) create mode 100644 src/frontends/lean/obtain_expr.cpp create mode 100644 src/frontends/lean/obtain_expr.h create mode 100644 tests/lean/run/new_obtains.lean diff --git a/library/data/set/function.lean b/library/data/set/function.lean index 300b515f6..a59b602ee 100644 --- a/library/data/set/function.lean +++ b/library/data/set/function.lean @@ -45,13 +45,13 @@ lemma image_compose (f : Y → X) (g : X → Y) (a : set X) : (f ∘ g) '[a] = f setext (take z, iff.intro (assume Hz : z ∈ (f ∘ g) '[a], - obtain x (Hx : x ∈ a ∧ f (g x) = z), from Hz, - have Hgx : g x ∈ g '[a], from in_image (and.left Hx) rfl, - show z ∈ f '[g '[a]], from in_image Hgx (and.right Hx)) + obtain x (Hx₁ : x ∈ a) (Hx₂ : f (g x) = z), from Hz, + have Hgx : g x ∈ g '[a], from in_image Hx₁ rfl, + show z ∈ f '[g '[a]], from in_image Hgx Hx₂) (assume Hz : z ∈ f '[g '[a]], - obtain y (Hy : y ∈ g '[a] ∧ f y = z), from Hz, - obtain x (Hz : x ∈ a ∧ g x = y), from and.left Hy, - show z ∈ (f ∘ g) '[a], from in_image (and.left Hz) ((and.right Hz)⁻¹ ▸ (and.right Hy)))) + obtain y (Hy₁ : y ∈ g '[a]) (Hy₂ : f y = z), from Hz, + obtain x (Hz₁ : x ∈ a) (Hz₂ : g x = y), from Hy₁, + show z ∈ (f ∘ g) '[a], from in_image Hz₁ (Hz₂⁻¹ ▸ Hy₂))) /- maps to -/ diff --git a/src/frontends/lean/CMakeLists.txt b/src/frontends/lean/CMakeLists.txt index 678ea90f0..e3da6284a 100644 --- a/src/frontends/lean/CMakeLists.txt +++ b/src/frontends/lean/CMakeLists.txt @@ -8,6 +8,7 @@ structure_cmd.cpp info_manager.cpp info_annotation.cpp find_cmd.cpp coercion_elaborator.cpp info_tactic.cpp init_module.cpp elaborator_context.cpp calc_proof_elaborator.cpp parse_tactic_location.cpp parse_rewrite_tactic.cpp builtin_tactics.cpp -type_util.cpp elaborator_exception.cpp migrate_cmd.cpp local_ref_info.cpp) +type_util.cpp elaborator_exception.cpp migrate_cmd.cpp local_ref_info.cpp +obtain_expr.cpp) target_link_libraries(lean_frontend ${LEAN_LIBS}) diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp index 03cc0cf55..573e7871d 100644 --- a/src/frontends/lean/builtin_exprs.cpp +++ b/src/frontends/lean/builtin_exprs.cpp @@ -32,6 +32,7 @@ Author: Leonardo de Moura #include "frontends/lean/info_tactic.h" #include "frontends/lean/info_annotation.h" #include "frontends/lean/structure_cmd.h" +#include "frontends/lean/obtain_expr.h" namespace lean { namespace notation { @@ -275,7 +276,7 @@ static expr parse_begin_end(parser & p, unsigned, expr const *, pos_info const & static expr parse_proof_qed_core(parser & p, pos_info const & pos) { expr r = p.parse_expr(); p.check_token_next(get_qed_tk(), "invalid proof-qed, 'qed' expected"); - r = p.mk_by(p.mk_app(get_exact_tac_fn(), r, pos), pos); + r = p.mk_by_plus(p.mk_app(get_exact_tac_fn(), r, pos), pos); return r; } @@ -439,37 +440,37 @@ static expr parse_show(parser & p, unsigned, expr const *, pos_info const & pos) } } +static obtain_struct parse_obtain_decls (parser & p, buffer & ps) { + buffer children; + while (!p.curr_is_token(get_comma_tk()) && !p.curr_is_token(get_rbracket_tk())) { + if (p.curr_is_token(get_lbracket_tk())) { + p.next(); + auto s = parse_obtain_decls(p, ps); + children.push_back(s); + p.check_token_next(get_rbracket_tk(), "invalid 'obtain' expression, ']' expected"); + } else { + unsigned old_sz = ps.size(); + unsigned rbp = 0; + p.parse_simple_binders(ps, rbp); + for (unsigned i = old_sz; i < ps.size(); i++) + children.push_back(obtain_struct()); + } + } + if (children.empty()) + throw parser_error("invalid 'obtain' expression, empty declaration block", p.pos()); + return obtain_struct(to_list(children)); +} + static expr parse_obtain(parser & p, unsigned, expr const *, pos_info const & pos) { - if (!p.env().find(get_exists_elim_name())) - throw parser_error("invalid use of 'obtain' expression, environment does not contain 'exists.elim' theorem", pos); - // exists_elim {A : Type} {P : A → Prop} {B : Prop} (H1 : ∃ x : A, P x) (H2 : ∀ (a : A) (H : P a), B) buffer ps; - auto b_pos = p.pos(); - unsigned rbp = 0; - environment env = p.parse_binders(ps, rbp); - unsigned num_ps = ps.size(); - if (num_ps < 2) - throw parser_error("invalid 'obtain' expression, at least 2 binders expected", b_pos); + obtain_struct s = parse_obtain_decls(p, ps); p.check_token_next(get_comma_tk(), "invalid 'obtain' expression, ',' expected"); p.check_token_next(get_from_tk(), "invalid 'obtain' expression, 'from' expected"); - expr H1 = p.parse_expr(); + expr from = p.parse_expr(); p.check_token_next(get_comma_tk(), "invalid 'obtain' expression, ',' expected"); - expr b = p.parse_scoped_expr(ps, env); - expr H = ps[num_ps-1]; - name H_name = local_pp_name(H); - unsigned i = num_ps-1; - while (i > 1) { - --i; - expr a = ps[i]; - expr H_aux = mk_local(p.mk_fresh_name(), H_name.append_after(i), mk_expr_placeholder(), mk_contextual_info(false)); - expr H2 = Fun({a, H}, b); - b = mk_app(mk_constant(get_exists_elim_name()), H_aux, H2); - H = H_aux; - } - expr a = ps[0]; - expr H2 = Fun({a, H}, b); - expr r = mk_app(mk_constant(get_exists_elim_name()), H1, H2); - return p.rec_save_pos(r, pos); + expr goal = p.parse_scoped_expr(ps); + expr r = p.rec_save_pos(mk_obtain_expr(s, ps, from, goal), pos); + return p.mk_by_plus(p.mk_app(get_exact_tac_fn(), r, pos), pos); } static expr * g_not = nullptr; diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 5145e742b..3c829ad00 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -285,6 +285,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_by_plus(e)) { + return visit_by_plus(e, some_expr(t), cs); } else if (is_calc_annotation(e)) { return visit_calc_proof(e, some_expr(t), cs); } else { @@ -318,6 +320,15 @@ expr elaborator::visit_by(expr const & e, optional const & t, constraint_s return m; } +expr elaborator::visit_by_plus(expr const & e, optional const & t, constraint_seq & cs) { + lean_assert(is_by_plus(e)); + expr tac = visit(get_by_plus_arg(e), cs); + expr m = m_full_context.mk_meta(m_ngen, t, e.get_tag()); + register_meta(m); + m_local_tactic_hints.insert(mlocal_name(get_app_fn(m)), tac); + 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; @@ -1342,6 +1353,129 @@ expr elaborator::visit_structure_instance(expr const & e, constraint_seq & cs) { return S_mk; } +expr elaborator::process_obtain_expr(list const & s_list, list const & from_list, + expr const & goal, bool first, constraint_seq & cs, expr const & src) { + lean_assert(length(s_list) == length(from_list)); + if (!s_list && !from_list) + return visit(goal, cs); + expr from = head(from_list); + obtain_struct s = head(s_list); + lean_assert(!first || !s.is_leaf()); + if (s.is_leaf()) { + lean_assert(is_local(from)); + expr const & from_type = mlocal_type(from); + // fix user visible name + expr goal_domain = visit(binding_domain(goal), cs); + expr new_from = ::lean::mk_local(mlocal_name(from), binding_name(goal), goal_domain, binder_info()); + if (!is_lambda(goal)) + throw_elaborator_exception("invalid 'obtain' expression, insufficient number of local declarations", src); + justification j = mk_type_mismatch_jst(new_from, goal_domain, from_type, src); + if (!is_def_eq(from_type, goal_domain, j, cs)) + throw unifier_exception(j, substitution()); + flet save1(m_context, m_context); + flet save2(m_full_context, m_full_context); + m_context.add_local(new_from); + m_full_context.add_local(new_from); + expr new_goal = instantiate(binding_body(goal), new_from); + expr r = process_obtain_expr(tail(s_list), tail(from_list), new_goal, false, cs, src); + return Fun(new_from, r); + } else { + lean_assert(!first || is_local(from)); + expr from_type = whnf(infer_type(from, cs), cs); + buffer I_args; + expr I = get_app_args(from_type, I_args); + if (!is_constant(I)) { + throw_elaborator_exception(src, [=](formatter const & fmt) { + format r = format("invalid 'obtain' expression, type of 'from' expression is not inductive"); + r += pp_indent_expr(fmt, from_type); + return r; + }); + } + name const & I_name = const_name(I); + levels const & I_lvls = const_levels(I); + if (!inductive::is_inductive_decl(env(), I_name)) + throw_elaborator_exception(sstream() << "invalid 'obtain' expression, '" << I_name + << "' is not an inductive datatype", src); + if (*inductive::get_num_intro_rules(env(), I_name) != 1) + throw_elaborator_exception(sstream() << "invalid 'obtain' expression, '" << I_name + << "' has more than one constructor", src); + unsigned nparams = *inductive::get_num_params(env(), I_name); + unsigned nindices = *inductive::get_num_indices(env(), I_name); + declaration cases_on_decl = env().get({I_name, "cases_on"}); + levels cases_on_lvls = I_lvls; + if (cases_on_decl.get_num_univ_params() != length(I_lvls)) + cases_on_lvls = cons(mk_meta_univ(m_ngen.next()), cases_on_lvls); + expr cases_on = mk_constant(cases_on_decl.get_name(), cases_on_lvls); + tag g = src.get_tag(); + expr R = cases_on; + for (unsigned i = 0; i < nparams; i++) + R = mk_app(R, I_args[i], g); + expr R_type = whnf(infer_type(R, cs), cs); + auto check_R_type = [&]() { + if (!is_pi(R_type)) + throw_elaborator_exception(sstream() << "invalid 'obtain' expression, '" + << I_name << "' has an ill-formed cases_on recursor", src); + }; + check_R_type(); + expr motive_type = binding_domain(R_type); + expr motive = m_full_context.mk_meta(m_ngen, some_expr(motive_type), g); + R = mk_app(R, motive, g); + R_type = whnf(instantiate(binding_body(R_type), motive), cs); + for (unsigned i = 0; i < nindices; i++) { + check_R_type(); + expr index_type = binding_domain(R_type); + expr index = m_full_context.mk_meta(m_ngen, some_expr(index_type), g); + R = mk_app(R, index, g); + R_type = whnf(instantiate(binding_body(R_type), index), cs); + } + check_R_type(); + expr major_type = binding_domain(R_type); + justification j = mk_type_mismatch_jst(from, from_type, major_type, src); + if (!is_def_eq(from_type, major_type, j, cs)) + throw unifier_exception(j, substitution()); + R = mk_app(R, from, g); + R_type = whnf(instantiate(binding_body(R_type), from), cs); + check_R_type(); + expr minor_type = whnf(binding_domain(R_type), cs); + buffer telescope; + to_telescope(*m_tc[m_relax_main_opaque], minor_type, telescope, optional(), cs); + lean_assert(!s.is_leaf()); + buffer s_buffer; + to_buffer(s.get_children(), s_buffer); + if (telescope.size() == 0) + throw_elaborator_exception(sstream() << "invalid 'obtain' expression, '" << I_name + << "' is an empty type", src); + if (s_buffer.size() < telescope.size()) + throw_elaborator_exception("invalid 'obtain' expression, insufficient number of local declarations", src); + if (s_buffer.size() > telescope.size()) { + obtain_struct s_tail(to_list(s_buffer.begin() + telescope.size() - 1, s_buffer.end())); + s_buffer.shrink(telescope.size() - 1); + s_buffer.push_back(s_tail); + } + lean_assert(s_buffer.size() == telescope.size()); + list new_s_list = to_list(s_buffer.begin(), s_buffer.end(), tail(s_list)); + list new_from_list = to_list(telescope.begin(), telescope.end(), tail(from_list)); + expr minor = process_obtain_expr(new_s_list, new_from_list, goal, false, cs, src); + expr infer_minor_type = infer_type(minor, cs); + justification j2 = mk_type_mismatch_jst(minor, infer_minor_type, minor_type, src); + if (!is_def_eq(infer_minor_type, minor_type, j2, cs)) + throw unifier_exception(j2, substitution()); + expr r = mk_app(R, minor, g); + if (!first) + r = Fun(from, r); + return r; + } +} + +expr elaborator::visit_obtain_expr(expr const & e, constraint_seq & cs) { + lean_assert(is_obtain_expr(e)); + expr from, decls_goal; + obtain_struct s; + decompose_obtain(e, s, from, decls_goal); + from = visit(from, cs); + return process_obtain_expr(to_list(s), to_list(from), decls_goal, true, cs, e); +} + expr elaborator::visit_core(expr const & e, constraint_seq & cs) { if (is_placeholder(e)) { return visit_placeholder(e, cs); @@ -1351,6 +1485,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_by_plus(e)) { + return visit_by_plus(e, none_expr(), cs); } else if (is_calc_annotation(e)) { return visit_calc_proof(e, none_expr(), cs); } else if (is_no_info(e)) { @@ -1379,6 +1515,8 @@ expr elaborator::visit_core(expr const & e, constraint_seq & cs) { return visit_decreasing(e, cs); } else if (is_structure_instance(e)) { return visit_structure_instance(e, cs); + } else if (is_obtain_expr(e)) { + return visit_obtain_expr(e, cs); } else { switch (e.kind()) { case expr_kind::Local: return e; diff --git a/src/frontends/lean/elaborator.h b/src/frontends/lean/elaborator.h index 4d6e3c825..7a0ec4f95 100644 --- a/src/frontends/lean/elaborator.h +++ b/src/frontends/lean/elaborator.h @@ -18,6 +18,7 @@ Author: Leonardo de Moura #include "frontends/lean/coercion_elaborator.h" #include "frontends/lean/util.h" #include "frontends/lean/calc_proof_elaborator.h" +#include "frontends/lean/obtain_expr.h" namespace lean { /** \brief Mapping from metavariable names to metavariable applications (?M ...) */ @@ -84,6 +85,9 @@ class elaborator : public coercion_info_manager { pair whnf(expr const & e) { return m_tc[m_relax_main_opaque]->whnf(e); } expr infer_type(expr const & e, constraint_seq & s) { return m_tc[m_relax_main_opaque]->infer(e, s); } expr whnf(expr const & e, constraint_seq & s) { return m_tc[m_relax_main_opaque]->whnf(e, s); } + bool is_def_eq(expr const & e1, expr const & e2, justification const & j, constraint_seq & cs) { + return m_tc[m_relax_main_opaque]->is_def_eq(e1, e2, j, cs); + } expr mk_app(expr const & f, expr const & a, tag g) { return ::lean::mk_app(f, a, g); } void register_meta(expr const & meta); @@ -111,6 +115,7 @@ class elaborator : public coercion_info_manager { expr visit_expecting_type_of(expr const & e, expr const & t, constraint_seq & cs); 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_by_plus(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); @@ -121,6 +126,7 @@ class elaborator : public coercion_info_manager { justification const & j); pair ensure_has_type(expr const & a, expr const & a_type, expr const & expected_type, justification const & j, bool relax); + bool is_choice_app(expr const & e); expr visit_choice_app(expr const & e, constraint_seq & cs); expr visit_app(expr const & e, constraint_seq & cs); @@ -172,6 +178,9 @@ class elaborator : public coercion_info_manager { bool is_structure(expr const & S); expr visit_structure_instance(expr const & e, constraint_seq & cs); + expr process_obtain_expr(list const & s_list, list const & from_list, + expr const & goal, bool first, constraint_seq & cs, expr const & src); + expr visit_obtain_expr(expr const & e, constraint_seq & cs); public: elaborator(elaborator_context & ctx, name_generator const & ngen, bool nice_mvar_names = false); std::tuple operator()(list const & ctx, expr const & e, bool _ensure_type, diff --git a/src/frontends/lean/init_module.cpp b/src/frontends/lean/init_module.cpp index 98b2d9f2e..220110685 100644 --- a/src/frontends/lean/init_module.cpp +++ b/src/frontends/lean/init_module.cpp @@ -29,6 +29,7 @@ Author: Leonardo de Moura #include "frontends/lean/pp.h" #include "frontends/lean/server.h" #include "frontends/lean/local_ref_info.h" +#include "frontends/lean/obtain_expr.h" namespace lean { void initialize_frontend_lean_module() { @@ -57,8 +58,10 @@ void initialize_frontend_lean_module() { initialize_server(); initialize_find_cmd(); initialize_local_ref_info(); + initialize_obtain_expr(); } void finalize_frontend_lean_module() { + finalize_obtain_expr(); finalize_local_ref_info(); finalize_find_cmd(); finalize_server(); diff --git a/src/frontends/lean/obtain_expr.cpp b/src/frontends/lean/obtain_expr.cpp new file mode 100644 index 000000000..32a6a2f22 --- /dev/null +++ b/src/frontends/lean/obtain_expr.cpp @@ -0,0 +1,113 @@ +/* +Copyright (c) 2015 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#include +#include "kernel/abstract.h" +#include "kernel/instantiate.h" +#include "library/kernel_serializer.h" +#include "frontends/lean/obtain_expr.h" + +namespace lean { +unsigned obtain_struct::size() const { + if (m_leaf) return 1; + unsigned r = 0; + for (auto const & o : m_children) r += o.size(); + return r; +} + +obtain_struct read_obtain_struct(deserializer & d); +inline serializer & operator<<(serializer & s, obtain_struct const & o) { o.write(s); return s; } +inline deserializer & operator>>(deserializer & d, obtain_struct & o) { + o = read_obtain_struct(d); + return d; +} + +void obtain_struct::write(serializer & s) const { + s << m_leaf; + if (!m_leaf) + write_list(s, m_children); +} + +obtain_struct read_obtain_struct(deserializer & d) { + bool leaf = d.read_bool(); + if (leaf) + return obtain_struct(); + return obtain_struct(read_list(d)); +} + +static name * g_obtain_name = nullptr; +static std::string * g_obtain_opcode = nullptr; + +[[ noreturn ]] static void throw_ex() { throw exception("unexpected occurrence of 'obtain' expression"); } + +class obtain_macro_cell : public macro_definition_cell { + obtain_struct m_struct; +public: + obtain_macro_cell(obtain_struct const & s):m_struct(s) {} + virtual name get_name() const { return *g_obtain_name; } + virtual pair get_type(expr const &, extension_context &) const { throw_ex(); } + virtual optional expand(expr const &, extension_context &) const { throw_ex(); } + virtual void write(serializer & s) const { + s << *g_obtain_opcode << m_struct; + } + obtain_struct const & get_struct() const { return m_struct; } +}; + +static bool validate(obtain_struct const & s, expr const & decls_goal) { + unsigned sz = s.size(); + expr it = decls_goal; + for (unsigned i = 0; i < sz; i++) { + if (!is_lambda(it)) + return false; + it = binding_body(it); + } + return true; +} + +static expr mk_obtain_expr_core(obtain_struct const & s, expr const & from, expr const & decls_goal) { + lean_assert(validate(s, decls_goal)); + macro_definition def(new obtain_macro_cell(s)); + expr args[2] = {from, decls_goal}; + return mk_macro(def, 2, args); +} + +expr mk_obtain_expr(obtain_struct const & s, buffer const & decls, expr const & from, expr const & goal) { + lean_assert(s.size() == decls.size()); + lean_assert(std::all_of(decls.begin(), decls.end(), is_local)); + return mk_obtain_expr_core(s, from, Fun(decls, goal)); +} + +bool is_obtain_expr(expr const & e) { + return is_macro(e) && macro_def(e).get_name() == *g_obtain_name; +} + +void decompose_obtain(expr const & e, obtain_struct & s, expr & from, expr & decls_goal) { + lean_assert(is_obtain_expr(e)); + s = static_cast(macro_def(e).raw())->get_struct(); + from = macro_arg(e, 0); + decls_goal = macro_arg(e, 1); +} + +void initialize_obtain_expr() { + g_obtain_name = new name("obtain"); + g_obtain_opcode = new std::string("Obtain"); + register_macro_deserializer(*g_obtain_opcode, + [](deserializer & d, unsigned num, expr const * args) { + if (num != 2) + throw corrupted_stream_exception(); + obtain_struct s; + d >> s; + if (!validate(s, args[1])) + throw corrupted_stream_exception(); + return mk_obtain_expr_core(s, args[0], args[1]); + }); +} + +void finalize_obtain_expr() { + delete g_obtain_opcode; + delete g_obtain_name; +} +}; diff --git a/src/frontends/lean/obtain_expr.h b/src/frontends/lean/obtain_expr.h new file mode 100644 index 000000000..bbc301290 --- /dev/null +++ b/src/frontends/lean/obtain_expr.h @@ -0,0 +1,28 @@ +/* +Copyright (c) 2015 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +#include "kernel/expr.h" + +namespace lean { +class obtain_struct { + bool m_leaf; + list m_children; +public: + obtain_struct():m_leaf(true) {} + obtain_struct(list const & c):m_leaf(false), m_children(c) {} + bool is_leaf() const { return m_leaf; } + list const & get_children() const { return m_children; } + void write(serializer & s) const; + unsigned size() const; +}; + +expr mk_obtain_expr(obtain_struct const & s, buffer const & decls, expr const & from, expr const & goal); +bool is_obtain_expr(expr const & e); +void decompose_obtain(expr const & e, obtain_struct & s, expr & from, expr & decls_goal); +void initialize_obtain_expr(); +void finalize_obtain_expr(); +} diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 53a16faf3..b9075812a 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -217,6 +217,12 @@ expr parser::mk_by(expr const & t, pos_info const & pos) { return save_pos(::lean::mk_by(t), pos); } +expr parser::mk_by_plus(expr const & t, pos_info const & pos) { + if (!has_tactic_decls()) + throw parser_error("invalid 'by+' expression, tactic module has not been imported", pos); + return save_pos(::lean::mk_by_plus(t), pos); +} + void parser::updt_options() { m_verbose = get_verbose(m_ios.get_options()); m_show_errors = get_parser_show_errors(m_ios.get_options()); diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h index bfc5781a8..f93bbe151 100644 --- a/src/frontends/lean/parser.h +++ b/src/frontends/lean/parser.h @@ -271,6 +271,7 @@ public: bool has_tactic_decls(); expr mk_by(expr const & t, pos_info const & pos); + expr mk_by_plus(expr const & t, pos_info const & pos); bool keep_new_thms() const { return m_keep_theorem_mode != keep_theorem_mode::DiscardAll; } diff --git a/src/library/tactic/expr_to_tactic.cpp b/src/library/tactic/expr_to_tactic.cpp index 44084eeb2..ca6003fd2 100644 --- a/src/library/tactic/expr_to_tactic.cpp +++ b/src/library/tactic/expr_to_tactic.cpp @@ -324,17 +324,25 @@ void register_num_tac(name const & n, std::function f) { } static name * g_by_name = nullptr; +static name * g_by_plus_name = nullptr; expr mk_by(expr const & e) { return mk_annotation(*g_by_name, e); } bool is_by(expr const & e) { return is_annotation(e, *g_by_name); } expr const & get_by_arg(expr const & e) { lean_assert(is_by(e)); return get_annotation_arg(e); } +expr mk_by_plus(expr const & e) { return mk_annotation(*g_by_plus_name, e); } +bool is_by_plus(expr const & e) { return is_annotation(e, *g_by_plus_name); } +expr const & get_by_plus_arg(expr const & e) { lean_assert(is_by_plus(e)); return get_annotation_arg(e); } + void initialize_expr_to_tactic() { g_tmp_prefix = new name(name::mk_internal_unique_name()); g_by_name = new name("by"); register_annotation(*g_by_name); + g_by_plus_name = new name("by+"); + register_annotation(*g_by_plus_name); + g_map = new expr_to_tactic_map(); g_tactic_expr_type = new expr(mk_constant(get_tactic_expr_name())); @@ -425,6 +433,7 @@ void finalize_expr_to_tactic() { delete g_map; delete g_tactic_opcode; delete g_by_name; + delete g_by_plus_name; delete g_tmp_prefix; } } diff --git a/src/library/tactic/expr_to_tactic.h b/src/library/tactic/expr_to_tactic.h index e8782f1bb..d4fb55bec 100644 --- a/src/library/tactic/expr_to_tactic.h +++ b/src/library/tactic/expr_to_tactic.h @@ -61,6 +61,11 @@ bool is_by(expr const & t); /** \see mk_by */ expr const & get_by_arg(expr const & t); +// Similar to mk_by, but instructs the elaborator to include the whole context +expr mk_by_plus(expr const & t); +bool is_by_plus(expr const & t); +expr const & get_by_plus_arg(expr const & t); + expr const & get_tactic_type(); expr const & get_and_then_tac_fn(); expr const & get_or_else_tac_fn(); diff --git a/tests/lean/run/new_obtains.lean b/tests/lean/run/new_obtains.lean new file mode 100644 index 000000000..c35c3fc80 --- /dev/null +++ b/tests/lean/run/new_obtains.lean @@ -0,0 +1,74 @@ +import data.nat + +theorem tst2 (A B C D : Type) : (A × B) × (C × D) → C × B × A := +assume p : (A × B) × (C × D), +obtain [a b] [c d], from p, +(c, b, a) + +theorem tst (a b c d : Prop) : (a ∧ b) ∧ (c ∧ d) → c ∧ b ∧ a := +assume H, +obtain [Ha Hb] Hc Hd, from H, +and.intro Hc (and.intro Hb Ha) + +theorem tst22 (A B C D : Type) : (A × B) × (C × D) → C × B × A := +assume p, +obtain [a b] [c d], from p, +(c, b, a) + +theorem tst3 (A B C D : Type) : A × B × C × D → C × B × A := +assume p, +obtain [[a b] c] d, from p, +(c, b, a) + +example (p : nat → nat → Prop) : (∃ x, p x x) → ∃ x y, p x y := +assume ex, +obtain x pxx, from ex, +exists.intro x (exists.intro x pxx) + +example (p q : nat → nat → Prop) : (∃ x y, p x y ∧ q x y ∧ q y x) → ∃ x y, p x y := +assume ex, +obtain x y pxy qxy qyx, from ex, +exists.intro x (exists.intro y pxy) + +example (p : nat → nat → Type): (Σ x, p x x) → (Σ x y, p x y) := +assume sig, +obtain x pxx, from sig, +⟨x, x, pxx⟩ + +example (p q : nat → nat → Type) : (Σ x y, p x y × q x y × q y x) → Σ x y, p x y := +assume ex : Σ x y, p x y × q x y × q y x, +obtain x y [[pxy qxy] qyx], from ex, +⟨x, y, pxy⟩ + +example (p q : nat → nat → Type) : (Σ x y, p x y × q x y × q y x) → Σ x y, p x y := +assume ex, +have ex1 : Σ x y, p x y × q x y × q y x, from ex, +obtain x y [[pxy qxy] qyx], from ex1, +⟨x, y, pxy⟩ + +example (p q : nat → nat → Type) : (Σ x y, p x y × q x y × q y x) → Σ x y, p x y := +assume ex, +obtain x y [[pxy qxy] qyx], from ex, +⟨x, y, pxy⟩ + +open nat + +definition even (a : nat) := ∃ x, a = 2*x + +example (a b : nat) (H₁ : even a) (H₂ : even b) : even (a+b) := +obtain x (Hx : a = 2*x), from H₁, +obtain y (Hy : b = 2*y), from H₂, +exists.intro + (x+y) + (calc a+b = 2*x + 2*y : by rewrite [Hx, Hy] + ... = 2*(x+y) : by rewrite mul.left_distrib) + +theorem dvd_of_dvd_add_left {m n₁ n₂ : ℕ} (H₁ : m ∣ n₁ + n₂) (H₂ : m ∣ n₁) : m ∣ n₂ := +obtain (c₁ : nat) (Hc₁ : n₁ + n₂ = m * c₁), from H₁, +obtain (c₂ : nat) (Hc₂ : n₁ = m * c₂), from H₂, +have aux : m * (c₁ - c₂) = n₂, from calc + m * (c₁ - c₂) = m * c₁ - m * c₂ : by rewrite mul_sub_left_distrib + ... = n₁ + n₂ - m * c₂ : Hc₁ + ... = n₁ + n₂ - n₁ : Hc₂ + ... = n₂ : add_sub_cancel_left, +dvd.intro aux