From 58c9421babe704b5f13c70010176d9f16db1169c Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 14 Oct 2014 17:12:57 -0700 Subject: [PATCH] refactor(library/tactic): elaborate expressions nested in tactics with respect to current goal, save postponed constraints (e.g., flex-flex constraints) closes #44, fixes #70 --- library/tools/fake_simplifier.lean | 2 +- library/tools/helper_tactics.lean | 2 +- library/tools/tactic.lean | 1 - src/frontends/lean/CMakeLists.txt | 3 +- src/frontends/lean/builtin_exprs.cpp | 49 ++- src/frontends/lean/builtin_tactics.cpp | 33 ++ src/frontends/lean/builtin_tactics.h | 14 + src/frontends/lean/elaborator.cpp | 104 +++-- src/frontends/lean/elaborator.h | 6 +- src/frontends/lean/init_module.cpp | 3 + src/frontends/lean/proof_qed_elaborator.cpp | 1 - src/frontends/lean/token_table.cpp | 2 +- src/frontends/lean/tokens.cpp | 4 + src/frontends/lean/tokens.h | 1 + src/frontends/lean/util.cpp | 2 +- src/library/tactic/apply_tactic.cpp | 90 +++-- src/library/tactic/apply_tactic.h | 1 + src/library/tactic/expr_to_tactic.cpp | 411 +++++++++++++------- src/library/tactic/expr_to_tactic.h | 11 +- src/library/tactic/goal.cpp | 6 + src/library/tactic/goal.h | 18 +- src/library/tactic/proof_state.cpp | 22 +- src/library/tactic/proof_state.h | 15 +- src/library/tactic/tactic.h | 5 + tests/lean/have1.lean | 2 +- tests/lean/run/beginend.lean | 9 + tests/lean/run/tactic10.lean | 4 +- tests/lean/run/tactic11.lean | 13 +- tests/lean/run/tactic12.lean | 4 +- tests/lean/run/tactic13.lean | 4 +- tests/lean/run/tactic17.lean | 11 +- tests/lean/run/tactic18.lean | 5 +- tests/lean/run/tactic19.lean | 7 +- tests/lean/run/tactic29.lean | 2 +- tests/lean/run/tactic8.lean | 8 +- tests/lean/show1.lean | 2 +- 36 files changed, 626 insertions(+), 251 deletions(-) create mode 100644 src/frontends/lean/builtin_tactics.cpp create mode 100644 src/frontends/lean/builtin_tactics.h create mode 100644 tests/lean/run/beginend.lean diff --git a/library/tools/fake_simplifier.lean b/library/tools/fake_simplifier.lean index 43770e68fa..2d01a65c3a 100644 --- a/library/tools/fake_simplifier.lean +++ b/library/tools/fake_simplifier.lean @@ -4,6 +4,6 @@ open tactic namespace fake_simplifier -- until we have the simplifier... -opaque definition simp : tactic := apply @sorry +opaque definition simp : tactic := apply sorry end fake_simplifier diff --git a/library/tools/helper_tactics.lean b/library/tools/helper_tactics.lean index bda430b3b5..335069a7b6 100644 --- a/library/tools/helper_tactics.lean +++ b/library/tools/helper_tactics.lean @@ -12,6 +12,6 @@ import .tactic open tactic namespace helper_tactics - definition apply_refl := apply @eq.refl + definition apply_refl := apply eq.refl tactic_hint apply_refl end helper_tactics diff --git a/library/tools/tactic.lean b/library/tools/tactic.lean index 1fe7674f03..4bdf8e1028 100644 --- a/library/tools/tactic.lean +++ b/library/tools/tactic.lean @@ -36,7 +36,6 @@ opaque definition state : tactic := builtin opaque definition fail : tactic := builtin opaque definition id : tactic := builtin opaque definition beta : tactic := builtin -opaque definition apply {B : Type} (b : B) : tactic := builtin opaque definition unfold {B : Type} (b : B) : tactic := builtin opaque definition exact {B : Type} (b : B) : tactic := builtin opaque definition trace (s : string) : tactic := builtin diff --git a/src/frontends/lean/CMakeLists.txt b/src/frontends/lean/CMakeLists.txt index 97ebc9a7f9..6a79b11f1a 100644 --- a/src/frontends/lean/CMakeLists.txt +++ b/src/frontends/lean/CMakeLists.txt @@ -7,6 +7,7 @@ begin_end_ext.cpp class.cpp pp_options.cpp tactic_hint.cpp pp.cpp 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 -proof_qed_elaborator.cpp init_module.cpp elaborator_context.cpp) +proof_qed_elaborator.cpp init_module.cpp elaborator_context.cpp +builtin_tactics.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 b30cf0018b..557f2fd54a 100644 --- a/src/frontends/lean/builtin_exprs.cpp +++ b/src/frontends/lean/builtin_exprs.cpp @@ -15,6 +15,7 @@ Author: Leonardo de Moura #include "library/choice.h" #include "library/let.h" #include "frontends/lean/builtin_exprs.h" +#include "frontends/lean/builtin_tactics.h" #include "frontends/lean/token_table.h" #include "frontends/lean/calc.h" #include "frontends/lean/begin_end_ext.h" @@ -117,12 +118,21 @@ static expr parse_by(parser & p, unsigned, expr const *, pos_info const & pos) { return p.mk_by(t, pos); } -static expr parse_begin_end(parser & p, unsigned, expr const *, pos_info const & pos) { +static expr parse_begin_end_core(parser & p, pos_info const & pos) { if (!p.has_tactic_decls()) throw parser_error("invalid 'begin-end' expression, tactic module has not been imported", pos); optional pre_tac = get_begin_end_pre_tactic(p.env()); - optional r; - while (true) { + buffer tacs; + bool first = true; + while (!p.curr_is_token(get_end_tk())) { + if (first) + first = false; + else + p.check_token_next(get_comma_tk(), "invalid 'begin-end' expression, ',' expected"); + if (p.curr_is_token(get_end_tk())) { + p.next(); + throw parser_error("invalid 'begin-end' expression, tactic or expression expected", p.pos()); + } bool use_exact = (p.curr_is_token(get_have_tk()) || p.curr_is_token(get_show_tk()) || p.curr_is_token(get_assume_tk()) || p.curr_is_token(get_take_tk()) || p.curr_is_token(get_fun_tk())); @@ -133,17 +143,25 @@ static expr parse_begin_end(parser & p, unsigned, expr const *, pos_info const & if (pre_tac) tac = p.mk_app({get_and_then_tac_fn(), *pre_tac, tac}, pos); tac = p.mk_app(get_determ_tac_fn(), tac, pos); - r = r ? p.mk_app({get_and_then_tac_fn(), *r, tac}, pos) : tac; - if (p.curr_is_token(get_end_tk())) { - auto pos = p.pos(); - p.next(); - return p.mk_by(*r, pos); - } else if (p.curr_is_token(get_comma_tk())) { - p.next(); - } else { - throw parser_error("invalid begin-end, ',' or 'end' expected", p.pos()); - } + tacs.push_back(tac); } + auto end_pos = p.pos(); + p.next(); + if (tacs.empty()) { + expr tac = get_id_tac_fn(); + if (pre_tac) + tac = p.mk_app({get_and_then_tac_fn(), *pre_tac, tac}, end_pos); + tacs.push_back(tac); + } + expr r = tacs[0]; + for (unsigned i = 1; i < tacs.size(); i++) { + r = p.mk_app({get_and_then_tac_fn(), r, tacs[i]}, end_pos); + } + return p.mk_by(r, end_pos); +} + +static expr parse_begin_end(parser & p, unsigned, expr const *, pos_info const & pos) { + return parse_begin_end_core(p, pos); } static expr parse_proof_qed_core(parser & p, pos_info const & pos) { @@ -161,6 +179,10 @@ static expr parse_proof(parser & p, expr const & prop) { auto pos = p.pos(); p.next(); return parse_proof_qed_core(p, pos); + } else if (p.curr_is_token(get_begin_tk())) { + auto pos = p.pos(); + p.next(); + return parse_begin_end_core(p, pos); } else if (p.curr_is_token(get_by_tk())) { // parse: 'by' tactic auto pos = p.pos(); @@ -386,6 +408,7 @@ parse_table init_nud_table() { r = r.add({transition("begin", mk_ext_action(parse_begin_end))}, x0); r = r.add({transition("proof", mk_ext_action(parse_proof_qed))}, x0); r = r.add({transition("sorry", mk_ext_action(parse_sorry))}, x0); + init_nud_tactic_table(r); return r; } diff --git a/src/frontends/lean/builtin_tactics.cpp b/src/frontends/lean/builtin_tactics.cpp new file mode 100644 index 0000000000..cd5ceb30a1 --- /dev/null +++ b/src/frontends/lean/builtin_tactics.cpp @@ -0,0 +1,33 @@ +/* +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 +#include "library/explicit.h" +#include "library/tactic/expr_to_tactic.h" +#include "frontends/lean/parser.h" +#include "frontends/lean/parse_table.h" + +namespace lean { +using notation::transition; +using notation::mk_ext_action; + +static expr parse_apply(parser & p, unsigned, expr const *, pos_info const & pos) { + parser::no_undef_id_error_scope scope(p); + expr e = p.parse_expr(std::numeric_limits::max()); + return p.save_pos(mk_apply_tactic_macro(e), pos); +} + +void init_nud_tactic_table(parse_table & r) { + expr x0 = mk_var(0); + r = r.add({transition("apply", mk_ext_action(parse_apply))}, x0); +} + +void initialize_builtin_tactics() { +} + +void finalize_builtin_tactics() { +} +} diff --git a/src/frontends/lean/builtin_tactics.h b/src/frontends/lean/builtin_tactics.h new file mode 100644 index 0000000000..fd1fe62212 --- /dev/null +++ b/src/frontends/lean/builtin_tactics.h @@ -0,0 +1,14 @@ +/* +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 "frontends/lean/parse_table.h" + +namespace lean { +void init_nud_tactic_table(parse_table & r); +void initialize_builtin_tactics(); +void finalize_builtin_tactics(); +} diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index e8a3dd9e82..e93cdf979c 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -91,8 +91,9 @@ elaborator::elaborator(elaborator_context & ctx, name_generator const & ngen): m_context(), m_full_context(), m_unifier_config(ctx.m_ios.get_options(), true /* use exceptions */, true /* discard */) { - m_has_sorry = has_sorry(m_ctx.m_env), - m_relax_main_opaque = false; + m_has_sorry = has_sorry(m_ctx.m_env); + m_relax_main_opaque = false; + m_use_tactic_hints = true; m_no_info = false; m_tc[0] = mk_type_checker(ctx.m_env, m_ngen.mk_child(), false); m_tc[1] = mk_type_checker(ctx.m_env, m_ngen.mk_child(), true); @@ -601,6 +602,8 @@ expr elaborator::visit_sort(expr const & e) { expr elaborator::visit_macro(expr const & e, constraint_seq & cs) { if (is_as_is(e)) { return get_as_is_arg(e); + } else if (is_tactic_macro(e)) { + return e; } else { buffer args; for (unsigned i = 0; i < macro_num_args(e); i++) @@ -882,25 +885,12 @@ void elaborator::display_unsolved_proof_state(expr const & mvar, proof_state con } } -// For each occurrence of \c exact_tac in \c pre_tac, display its unassigned metavariables. -// This is a trick to improve the quality of the error messages. -void elaborator::check_exact_tacs(expr const & pre_tac, substitution const & s) { - for_each(pre_tac, [&](expr const & e, unsigned) { - expr const & f = get_app_fn(e); - if (is_constant(f) && const_name(f) == const_name(get_exact_tac_fn())) { - display_unassigned_mvars(e, s); - return false; - } else { - return true; - } - }); -} - optional elaborator::get_pre_tactic_for(substitution & subst, expr const & mvar, name_set & visited) { if (auto it = m_local_tactic_hints.find(mlocal_name(mvar))) { expr pre_tac = subst.instantiate(*it); - pre_tac = solve_unassigned_mvars(subst, pre_tac, visited); - check_exact_tacs(pre_tac, subst); + // TODO(Leo): after we move to new apply/exact, we will not need the following + // command anymore. + pre_tac = solve_unassigned_mvars(subst, pre_tac, visited); return some_expr(pre_tac); } else { return none_expr(); @@ -909,7 +899,15 @@ optional elaborator::get_pre_tactic_for(substitution & subst, expr const & optional elaborator::pre_tactic_to_tactic(expr const & pre_tac, expr const & mvar) { try { - return optional(expr_to_tactic(env(), pre_tac, pip())); + bool relax = m_relax_main_opaque; + auto fn = [=](goal const & g, name_generator const & ngen, expr const & e) { + elaborator aux_elaborator(m_ctx, ngen); + // Disable tactic hints when processing expressions nested in tactics. + // We must do it otherwise, it is easy to make the system loop. + bool use_tactic_hints = false; + return aux_elaborator.elaborate_nested(g.to_context(), e, relax, use_tactic_hints); + }; + return optional(expr_to_tactic(env(), fn, pre_tac, pip())); } catch (expr_to_tactic_exception & ex) { auto out = regular(env(), ios()); display_error_pos(out, pip(), mvar); @@ -980,12 +978,12 @@ void elaborator::solve_unassigned_mvar(substitution & subst, expr mvar, name_set expr type = m_tc[m_relax_main_opaque]->infer(*meta).first; // first solve unassigned metavariables in type type = solve_unassigned_mvars(subst, type, visited); - proof_state ps(goals(goal(*meta, type)), subst, m_ngen.mk_child()); + proof_state ps = to_proof_state(*meta, type, subst, m_ngen.mk_child()); if (auto local_hint = get_local_tactic_hint(subst, mvar, visited)) { // using user provided tactic bool show_failure = true; try_using(subst, mvar, ps, *local_hint, show_failure); - } else { + } else if (m_use_tactic_hints) { // using tactic_hints for (expr const & pre_tac : get_tactic_hints(env())) { if (auto tac = pre_tactic_to_tactic(pre_tac, mvar)) { @@ -1022,8 +1020,8 @@ void elaborator::display_unassigned_mvars(expr const & e, substitution const & s expr meta = tmp_s.instantiate(*it); expr meta_type = tmp_s.instantiate(type_checker(env()).infer(meta).first); goal g(meta, meta_type); - display_unsolved_proof_state(e, proof_state(goals(g), substitution(), m_ngen), - "don't know how to synthesize it"); + proof_state ps(goals(g), substitution(), m_ngen, constraints()); + display_unsolved_proof_state(e, ps, "don't know how to synthesize it"); } return false; }); @@ -1078,8 +1076,8 @@ std::tuple elaborator::apply(substitution & s, expr con return std::make_tuple(r, to_list(new_ps.begin(), new_ps.end())); } -std::tuple elaborator::operator()(list const & ctx, expr const & e, bool _ensure_type, - bool relax_main_opaque) { +auto elaborator::operator()(list const & ctx, expr const & e, bool _ensure_type, bool relax_main_opaque) +-> std::tuple { m_context.set_ctx(ctx); m_full_context.set_ctx(ctx); flet set_relax(m_relax_main_opaque, relax_main_opaque); @@ -1126,6 +1124,62 @@ std::tuple elaborator::operator()( return std::make_tuple(new_r_t, new_r_v, to_list(new_params.begin(), new_params.end())); } +// Auxiliary procedure for #translate +static expr translate_local_name(environment const & env, list const & ctx, name const & local_name, + expr const & src) { + for (expr const & local : ctx) { + if (mlocal_name(local) == local_name) + return local; + } + // TODO(Leo): we should create an elaborator exception. + // Using kernel_exception here is just a dirty hack. + throw_kernel_exception(env, sstream() << "unknown identifier '" << local_name << "'", src); +} + +/** \brief Translated local constants (and undefined constants) occurring in \c e into + local constants provided by \c ctx. + Throw exception is \c ctx does not contain the local constant. +*/ +static expr translate(environment const & env, list const & ctx, expr const & e) { + auto fn = [&](expr const & e) { + if (is_placeholder(e)) { + return some_expr(e); // ignore placeholders + } else if (is_constant(e)) { + if (!env.find(const_name(e))) { + return some_expr(translate_local_name(env, ctx, const_name(e), e)); + } else { + return none_expr(); + } + } else if (is_local(e)) { + return some_expr(translate_local_name(env, ctx, mlocal_name(e), e)); + } else { + return none_expr(); + } + }; + return replace(e, fn); +} + +/** \brief Elaborate expression \c e in context \c ctx. */ +pair elaborator::elaborate_nested(list const & ctx, expr const & n, + bool relax, bool use_tactic_hints) { + expr e = translate(env(), ctx, n); + m_context.set_ctx(ctx); + m_full_context.set_ctx(ctx); + flet set_relax(m_relax_main_opaque, relax); + flet set_discard(m_unifier_config.m_discard, false); + flet set_use_hints(m_use_tactic_hints, use_tactic_hints); + constraint_seq cs; + expr r = visit(e, cs); + auto p = solve(cs).pull(); + lean_assert(p); + substitution s = p->first.first; + constraints rcs = p->first.second; + r = s.instantiate(r); + r = solve_unassigned_mvars(s, r); + copy_info_to_manager(s); + return mk_pair(r, rcs); +} + static name * g_tmp_prefix = nullptr; std::tuple elaborate(elaborator_context & env, list const & ctx, expr const & e, diff --git a/src/frontends/lean/elaborator.h b/src/frontends/lean/elaborator.h index 382be38183..c07fbdf1e6 100644 --- a/src/frontends/lean/elaborator.h +++ b/src/frontends/lean/elaborator.h @@ -50,10 +50,10 @@ class elaborator : public coercion_info_manager { // if m_no_info is true, we do not collect information when true, // we set is to true whenever we find no_info annotation. bool m_no_info; + bool m_use_tactic_hints; info_manager m_pre_info_data; bool m_has_sorry; unifier_config m_unifier_config; - struct choice_expr_elaborator; environment const & env() const { return m_ctx.m_env; } @@ -122,7 +122,6 @@ class elaborator : public coercion_info_manager { expr visit(expr const & e, constraint_seq & cs); unify_result_seq solve(constraint_seq const & cs); void display_unsolved_proof_state(expr const & mvar, proof_state const & ps, char const * msg); - void check_exact_tacs(expr const & pre_tac, substitution const & s); optional get_pre_tactic_for(substitution & subst, expr const & mvar, name_set & visited); optional pre_tactic_to_tactic(expr const & pre_tac, expr const & mvar); optional get_local_tactic_hint(substitution & subst, expr const & mvar, name_set & visited); @@ -135,9 +134,10 @@ class elaborator : public coercion_info_manager { void check_sort_assignments(substitution const & s); expr apply(substitution & s, expr const & e, name_set & univ_params, buffer & new_params); std::tuple apply(substitution & s, expr const & e); + pair elaborate_nested(list const & g, expr const & e, + bool relax, bool use_tactic_hints); public: elaborator(elaborator_context & ctx, name_generator const & ngen); - std::tuple operator()(list const & ctx, expr const & e, bool _ensure_type, bool relax_main_opaque); std::tuple operator()(expr const & t, expr const & v, name const & n, bool is_opaque); diff --git a/src/frontends/lean/init_module.cpp b/src/frontends/lean/init_module.cpp index cc80e84cf5..f78b5fb3f8 100644 --- a/src/frontends/lean/init_module.cpp +++ b/src/frontends/lean/init_module.cpp @@ -18,6 +18,7 @@ Author: Leonardo de Moura #include "frontends/lean/begin_end_ext.h" #include "frontends/lean/builtin_cmds.h" #include "frontends/lean/builtin_exprs.h" +#include "frontends/lean/builtin_tactics.h" #include "frontends/lean/inductive_cmd.h" #include "frontends/lean/structure_cmd.h" #include "frontends/lean/info_manager.h" @@ -33,6 +34,7 @@ void initialize_frontend_lean_module() { initialize_token_table(); initialize_parse_table(); initialize_builtin_cmds(); + initialize_builtin_tactics(); initialize_builtin_exprs(); initialize_elaborator_context(); initialize_elaborator(); @@ -71,6 +73,7 @@ void finalize_frontend_lean_module() { finalize_elaborator(); finalize_elaborator_context(); finalize_builtin_exprs(); + finalize_builtin_tactics(); finalize_builtin_cmds(); finalize_parse_table(); finalize_token_table(); diff --git a/src/frontends/lean/proof_qed_elaborator.cpp b/src/frontends/lean/proof_qed_elaborator.cpp index c1706facf1..f405a17693 100644 --- a/src/frontends/lean/proof_qed_elaborator.cpp +++ b/src/frontends/lean/proof_qed_elaborator.cpp @@ -30,7 +30,6 @@ constraint mk_proof_qed_cnstr(environment const & env, expr const & m, expr cons constraint_seq new_cs = cs + tcs.second + dcs.second; buffer cs_buffer; new_cs.linearize(cs_buffer); - metavar_closure cls(meta); cls.add(meta_type); cls.mk_constraints(s, j, relax, cs_buffer); diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp index 6d208770d0..98e1008825 100644 --- a/src/frontends/lean/token_table.cpp +++ b/src/frontends/lean/token_table.cpp @@ -76,7 +76,7 @@ void init_token_table(token_table & t) { {".", 0}, {":", 0}, {"::", 0}, {"calc", 0}, {":=", 0}, {"--", 0}, {"#", 0}, {"(*", 0}, {"/-", 0}, {"begin", g_max_prec}, {"proof", g_max_prec}, {"qed", 0}, {"@", g_max_prec}, {"sorry", g_max_prec}, {"+", g_plus_prec}, {g_cup, g_cup_prec}, {"->", g_arrow_prec}, {"local", 0}, - {nullptr, 0}}; + {"apply", 0}, {nullptr, 0}}; char const * commands[] = {"theorem", "axiom", "variable", "protected", "private", "opaque", "definition", "coercion", diff --git a/src/frontends/lean/tokens.cpp b/src/frontends/lean/tokens.cpp index c3281a5841..9144015751 100644 --- a/src/frontends/lean/tokens.cpp +++ b/src/frontends/lean/tokens.cpp @@ -60,6 +60,7 @@ static name * g_then = nullptr; static name * g_by = nullptr; static name * g_proof = nullptr; static name * g_qed = nullptr; +static name * g_begin = nullptr; static name * g_end = nullptr; static name * g_definition = nullptr; static name * g_theorem = nullptr; @@ -143,6 +144,7 @@ void initialize_tokens() { g_by = new name("by"); g_proof = new name("proof"); g_qed = new name("qed"); + g_begin = new name("begin"); g_end = new name("end"); g_definition = new name("definition"); g_theorem = new name("theorem"); @@ -210,6 +212,7 @@ void finalize_tokens() { delete g_by; delete g_proof; delete g_qed; + delete g_begin; delete g_end; delete g_raw; delete g_true; @@ -310,6 +313,7 @@ name const & get_then_tk() { return *g_then; } name const & get_by_tk() { return *g_by; } name const & get_proof_tk() { return *g_proof; } name const & get_qed_tk() { return *g_qed; } +name const & get_begin_tk() { return *g_begin; } name const & get_end_tk() { return *g_end; } name const & get_definition_tk() { return *g_definition; } name const & get_theorem_tk() { return *g_theorem; } diff --git a/src/frontends/lean/tokens.h b/src/frontends/lean/tokens.h index ed462d3474..8c52517454 100644 --- a/src/frontends/lean/tokens.h +++ b/src/frontends/lean/tokens.h @@ -61,6 +61,7 @@ name const & get_using_tk(); name const & get_then_tk(); name const & get_by_tk(); name const & get_proof_tk(); +name const & get_begin_tk(); name const & get_qed_tk(); name const & get_end_tk(); name const & get_definition_tk(); diff --git a/src/frontends/lean/util.cpp b/src/frontends/lean/util.cpp index 0f54801960..fe2b30657e 100644 --- a/src/frontends/lean/util.cpp +++ b/src/frontends/lean/util.cpp @@ -322,7 +322,7 @@ justification mk_failed_to_synthesize_jst(environment const & env, expr const & substitution tmp(subst); expr new_m = instantiate_meta(m, tmp); expr new_type = type_checker(env).infer(new_m).first; - proof_state ps(goals(goal(new_m, new_type)), substitution(), name_generator("dontcare")); + proof_state ps = to_proof_state(new_m, new_type, name_generator("dontcare")); return format("failed to synthesize placeholder") + line() + ps.pp(fmt); }); } diff --git a/src/library/tactic/apply_tactic.cpp b/src/library/tactic/apply_tactic.cpp index 7badcb5f09..eef2a92b86 100644 --- a/src/library/tactic/apply_tactic.cpp +++ b/src/library/tactic/apply_tactic.cpp @@ -13,17 +13,18 @@ Author: Leonardo de Moura #include "kernel/instantiate.h" #include "kernel/abstract.h" #include "kernel/type_checker.h" +#include "library/reducible.h" #include "library/kernel_bindings.h" #include "library/unifier.h" #include "library/occurs.h" +#include "library/metavar_closure.h" #include "library/type_util.h" #include "library/tactic/apply_tactic.h" namespace lean { -/** - \brief Traverse \c e and collect metavariable applications (?m l1 ... ln), and store in result. - The function only succeeds if all metavariable applications are "simple", i.e., the arguments - are distinct local constants. +/** \brief Traverse \c e and collect metavariable applications (?m l1 ... ln), and store in result. + The function only succeeds if all metavariable applications are "simple", i.e., the arguments + are distinct local constants. */ bool collect_simple_metas(expr const & e, buffer & result) { bool failed = false; @@ -58,7 +59,7 @@ void collect_simple_meta(expr const & e, buffer & metas) { we say ?m_i is "redundant" if it occurs in the type of some ?m_j. This procedure removes from metas any redundant element. */ -static void remove_redundant_metas(buffer & metas) { +void remove_redundant_metas(buffer & metas) { buffer mvars; for (expr const & m : metas) mvars.push_back(get_app_fn(m)); @@ -81,65 +82,78 @@ static void remove_redundant_metas(buffer & metas) { metas.shrink(k); } -proof_state_seq apply_tactic_core(environment const & env, io_state const & ios, proof_state const & s, expr const & _e, - bool add_meta, bool add_subgoals, bool relax_main_opaque) { - // TODO(Leo): we are ignoring constraints produces by type checker +static proof_state_seq apply_tactic_core(environment const & env, io_state const & ios, proof_state const & s, expr const & _e, + buffer & cs, bool add_meta, bool add_subgoals, bool relax_main_opaque) { goals const & gs = s.get_goals(); if (empty(gs)) return proof_state_seq(); name_generator ngen = s.get_ngen(); - type_checker tc(env, ngen.mk_child()); + std::unique_ptr tc = mk_type_checker(env, ngen.mk_child(), relax_main_opaque); goal g = head(gs); goals tail_gs = tail(gs); expr t = g.get_type(); expr e = _e; - expr e_t = tc.infer(e).first; + auto e_t_cs = tc->infer(e); + e_t_cs.second.linearize(cs); + expr e_t = e_t_cs.first; buffer metas; - collect_simple_meta(e, metas); if (add_meta) { - unsigned num_t = get_expect_num_args(tc, t); - unsigned num_e_t = get_expect_num_args(tc, e_t); + unsigned num_t = get_expect_num_args(*tc, t); + unsigned num_e_t = get_expect_num_args(*tc, e_t); if (num_t > num_e_t) return proof_state_seq(); // no hope to unify then for (unsigned i = 0; i < num_e_t - num_t; i++) { - e_t = tc.whnf(e_t).first; + auto e_t_cs = tc->whnf(e_t); + e_t_cs.second.linearize(cs); + e_t = e_t_cs.first; expr meta = g.mk_meta(ngen.next(), binding_domain(e_t)); e = mk_app(e, meta); e_t = instantiate(binding_body(e_t), meta); metas.push_back(meta); } } - list meta_lst = to_list(metas.begin(), metas.end()); - unify_result_seq rseq = unify(env, t, e_t, ngen.mk_child(), relax_main_opaque, s.get_subst(), - unifier_config(ios.get_options())); + metavar_closure cls(t); + cls.mk_constraints(s.get_subst(), justification(), relax_main_opaque); + pair dcs = tc->is_def_eq(t, e_t); + if (!dcs.first) + return proof_state_seq(); + dcs.second.linearize(cs); + unifier_config cfg(ios.get_options()); + unify_result_seq rseq = unify(env, cs.size(), cs.data(), ngen.mk_child(), s.get_subst(), cfg); + list meta_lst = to_list(metas.begin(), metas.end()); return map2(rseq, [=](pair const & p) -> proof_state { - substitution const & subst = p.first; - // TODO(Leo): save postponed constraints + substitution const & subst = p.first; + constraints const & postponed = p.second; name_generator new_ngen(ngen); - type_checker tc(env, new_ngen.mk_child()); substitution new_subst = subst; expr new_e = new_subst.instantiate_all(e); expr new_p = g.abstract(new_e); check_has_no_local(new_p, _e, "apply"); new_subst.assign(g.get_name(), new_p); + // std::cout << g.get_name() << " := " << new_p << "\n"; goals new_gs = tail_gs; if (add_subgoals) { + // TODO(Leo): if mk_type_checker should return a shared_ptr, then we can reuse the tc defined + // before + std::unique_ptr tc = mk_type_checker(env, new_ngen.mk_child(), relax_main_opaque); buffer metas; for (auto m : meta_lst) { if (!new_subst.is_assigned(get_app_fn(m))) metas.push_back(m); } - remove_redundant_metas(metas); - unsigned i = metas.size(); - while (i > 0) { - --i; - new_gs = cons(goal(metas[i], new_subst.instantiate_all(tc.infer(metas[i]).first)), new_gs); - } + for (unsigned i = 0; i < metas.size(); i++) + new_gs = cons(goal(metas[i], new_subst.instantiate_all(tc->infer(metas[i]).first)), new_gs); } - return proof_state(new_gs, new_subst, new_ngen); + return proof_state(new_gs, new_subst, new_ngen, postponed); }); } +static proof_state_seq apply_tactic_core(environment const & env, io_state const & ios, proof_state const & s, expr const & e, + bool add_meta, bool add_subgoals, bool relax_main_opaque) { + buffer cs; + return apply_tactic_core(env, ios, s, e, cs, add_meta, add_subgoals, relax_main_opaque); +} + level refresh_univ_metavars(level const & l, name_generator & ngen, name_map & level_map) { return replace(l, [&](level const & l) { @@ -182,7 +196,7 @@ tactic apply_tactic(expr const & e, bool relax_main_opaque, bool refresh_univ_mv name_generator ngen = s.get_ngen(); substitution new_subst = s.get_subst(); expr new_e = refresh_univ_metavars(new_subst.instantiate_all(e), ngen); - proof_state new_s(s.get_goals(), new_subst, ngen); + proof_state new_s(s.get_goals(), new_subst, ngen, s.get_postponed()); return apply_tactic_core(env, ios, new_s, new_e, true, true, relax_main_opaque); } else { return apply_tactic_core(env, ios, s, e, true, true, relax_main_opaque); @@ -206,6 +220,26 @@ tactic eassumption_tactic(bool relax_main_opaque) { }); } +tactic apply_tactic(elaborate_fn const & elab, expr const & e, bool relax_main_opaque) { + return tactic([=](environment const & env, io_state const & ios, proof_state const & s) { + goals const & gs = s.get_goals(); + if (empty(gs)) + return proof_state_seq(); + goal const & g = head(gs); + name_generator ngen = s.get_ngen(); + expr new_e; + buffer cs; + // std::cout << "new apply tactic: " << e << "\n"; + auto ecs = elab(g, ngen.mk_child(), e); + new_e = ecs.first; + to_buffer(ecs.second, cs); + // std::cout << "after elaboration: " << new_e << "\n"; + to_buffer(s.get_postponed(), cs); + proof_state new_s(s.get_goals(), s.get_subst(), ngen, constraints()); + return apply_tactic_core(env, ios, new_s, new_e, cs, true, true, relax_main_opaque); + }); +} + int mk_apply_tactic(lua_State * L) { return push_tactic(L, apply_tactic(to_expr(L, 1))); } int mk_eassumption_tactic(lua_State * L) { return push_tactic(L, eassumption_tactic()); } void open_apply_tactic(lua_State * L) { diff --git a/src/library/tactic/apply_tactic.h b/src/library/tactic/apply_tactic.h index 64015b8584..c465a62432 100644 --- a/src/library/tactic/apply_tactic.h +++ b/src/library/tactic/apply_tactic.h @@ -9,6 +9,7 @@ Author: Leonardo de Moura #include "library/tactic/tactic.h" namespace lean { tactic apply_tactic(expr const & e, bool relax_main_opaque = true, bool refresh_univ_mvars = true); +tactic apply_tactic(elaborate_fn const & fn, expr const & e, bool relax_main_opaque = true); tactic eassumption_tactic(bool relax_main_opaque = true); void open_apply_tactic(lua_State * L); } diff --git a/src/library/tactic/expr_to_tactic.cpp b/src/library/tactic/expr_to_tactic.cpp index 4deb69f498..2a9b93d3a6 100644 --- a/src/library/tactic/expr_to_tactic.cpp +++ b/src/library/tactic/expr_to_tactic.cpp @@ -7,15 +7,35 @@ Author: Leonardo de Moura #include #include #include "util/sstream.h" +#include "util/optional.h" #include "kernel/instantiate.h" #include "kernel/type_checker.h" #include "library/annotation.h" #include "library/string.h" #include "library/num.h" +#include "library/kernel_serializer.h" #include "library/tactic/expr_to_tactic.h" #include "library/tactic/apply_tactic.h" namespace lean { +static expr * g_exact_tac_fn = nullptr; +static expr * g_and_then_tac_fn = nullptr; +static expr * g_or_else_tac_fn = nullptr; +static expr * g_id_tac_fn = nullptr; +static expr * g_repeat_tac_fn = nullptr; +static expr * g_determ_tac_fn = nullptr; +static expr * g_tac_type = nullptr; +static expr * g_builtin_tac = nullptr; +static expr * g_fixpoint_tac = nullptr; +expr const & get_exact_tac_fn() { return *g_exact_tac_fn; } +expr const & get_and_then_tac_fn() { return *g_and_then_tac_fn; } +expr const & get_or_else_tac_fn() { return *g_or_else_tac_fn; } +expr const & get_id_tac_fn() { return *g_id_tac_fn; } +expr const & get_determ_tac_fn() { return *g_determ_tac_fn; } +expr const & get_repeat_tac_fn() { return *g_repeat_tac_fn; } +expr const & get_tactic_type() { return *g_tac_type; } +expr const & get_builtin_tac() { return *g_builtin_tac; } + typedef std::unordered_map expr_to_tactic_map; static expr_to_tactic_map * g_map = nullptr; @@ -27,21 +47,6 @@ void register_tac(name const & n, expr_to_tactic_fn const & fn) { get_expr_to_tactic_map().insert(mk_pair(n, fn)); } -static expr * g_exact_tac_fn = nullptr; -static expr * g_and_then_tac_fn = nullptr; -static expr * g_or_else_tac_fn = nullptr; -static expr * g_repeat_tac_fn = nullptr; -static expr * g_determ_tac_fn = nullptr; -static expr * g_tac_type = nullptr; -static expr * g_builtin_tac = nullptr; -static expr * g_fixpoint_tac = nullptr; -expr const & get_exact_tac_fn() { return *g_exact_tac_fn; } -expr const & get_and_then_tac_fn() { return *g_and_then_tac_fn; } -expr const & get_or_else_tac_fn() { return *g_or_else_tac_fn; } -expr const & get_determ_tac_fn() { return *g_determ_tac_fn; } -expr const & get_repeat_tac_fn() { return *g_repeat_tac_fn; } -expr const & get_tactic_type() { return *g_tac_type; } - bool has_tactic_decls(environment const & env) { try { type_checker tc(env); @@ -55,6 +60,93 @@ bool has_tactic_decls(environment const & env) { } } +static name * g_tactic_name = nullptr; +static std::string * g_tactic_opcode = nullptr; + +name const & get_tactic_name() { return *g_tactic_name; } +std::string const & get_tactic_opcode() { return *g_tactic_opcode; } + +LEAN_THREAD_VALUE(bool, g_unfold_tactic_macros, true); + +/** \brief We use macros to wrap some builtin tactics that would not type check otherwise. + Example: in the tactic `apply t`, `t` is a pre-term (i.e., a term before elaboration). + Moreover its context depends on the goal it is applied to. +*/ +class tactic_macro_definition_cell : public macro_definition_cell { + name m_name; + expr_to_tactic_fn m_fn; +public: + tactic_macro_definition_cell(name const & n, expr_to_tactic_fn const & fn): + m_name(n), m_fn(fn) {} + name const & get_tatic_kind() const { return m_name; } + expr_to_tactic_fn const & get_fn() const { return m_fn; } + virtual name get_name() const { return get_tactic_name(); } + virtual format pp(formatter const &) const { return format(m_name); } + virtual void display(std::ostream & out) const { out << m_name; } + virtual pair get_type(expr const &, extension_context &) const { + return mk_pair(get_tactic_type(), constraint_seq()); + } + virtual optional expand(expr const &, extension_context &) const { + // Remark: small hack for conditionally expanding tactic macros. + // When processing type checking a macro definition, we want to unfold it, + // otherwise the kernel will not accept it. + // When converting it to a tactic object, we don't want to unfold it. + // The procedure expr_to_tactic temporarily sets g_unfold_tactic_macros to false. + // This is a thread local storage. So, there is no danger. + if (g_unfold_tactic_macros) + return some_expr(get_builtin_tac()); + else + return none_expr(); + } + virtual void write(serializer & s) const { + s.write_string(get_tactic_opcode()); + s << m_name; + } +}; + +typedef std::unordered_map tactic_macros; +static tactic_macros * g_tactic_macros = nullptr; +tactic_macros & get_tactic_macros() { return *g_tactic_macros; } + +void register_tactic_macro(name const & n, expr_to_tactic_fn const & fn) { + tactic_macros & ms = get_tactic_macros(); + lean_assert(ms.find(n) == ms.end()); + ms.insert(mk_pair(n, macro_definition(new tactic_macro_definition_cell(n, fn)))); +} + +static void register_tacm(name const & n, expr_to_tactic_fn const & fn) { + register_tactic_macro(n, fn); +} + +expr mk_tactic_macro(name const & kind, unsigned num_args, expr const * args) { + tactic_macros & ms = get_tactic_macros(); + auto it = ms.find(kind); + if (it != ms.end()) { + return mk_macro(it->second, num_args, args); + } else { + throw exception(sstream() << "unknown builtin tactic '" << kind << "'"); + } +} + +expr mk_tactic_macro(name const & kind, expr const & e) { + return mk_tactic_macro(kind, 1, &e); +} + +bool is_tactic_macro(expr const & e) { + return is_macro(e) && macro_def(e).get_name() == get_tactic_name(); +} + +static name * g_apply_tactic_name = nullptr; + +expr mk_apply_tactic_macro(expr const & e) { + return mk_tactic_macro(*g_apply_tactic_name, e); +} + +expr_to_tactic_fn const & get_tactic_macro_fn(expr const & e) { + lean_assert(is_tactic_macro(e)); + return static_cast(macro_def(e).raw())->get_fn(); +} + static void throw_failed(expr const & e) { throw expr_to_tactic_exception(e, "failed to convert expression into tactic"); } @@ -69,42 +161,47 @@ static bool is_builtin_tactic(expr const & v) { return false; } -tactic expr_to_tactic(type_checker & tc, expr e, pos_info_provider const * p) { +tactic expr_to_tactic(type_checker & tc, elaborate_fn const & fn, expr e, pos_info_provider const * p) { e = tc.whnf(e).first; - expr f = get_app_fn(e); - if (!is_constant(f)) - throw_failed(e); - optional it = tc.env().find(const_name(f)); - if (!it || !it->is_definition()) - throw_failed(e); - expr v = it->get_value(); - if (is_builtin_tactic(v)) { - auto const & map = get_expr_to_tactic_map(); - auto it2 = map.find(const_name(f)); - if (it2 != map.end()) - return it2->second(tc, e, p); - else - throw expr_to_tactic_exception(e, sstream() << "implementation for builtin tactic '" << const_name(f) << "' was not found"); + if (is_tactic_macro(e)) { + return get_tactic_macro_fn(e)(tc, fn, e, p); } else { - // unfold definition - buffer locals; - get_app_rev_args(e, locals); - level_param_names const & ps = it->get_univ_params(); - levels ls = const_levels(f); - unsigned num_ps = length(ps); - unsigned num_ls = length(ls); - if (num_ls > num_ps) - throw expr_to_tactic_exception(e, sstream() << "invalid number of universes"); - if (num_ls < num_ps) { - buffer extra_ls; - name_generator ngen = tc.mk_ngen(); - for (unsigned i = num_ls; i < num_ps; i++) - extra_ls.push_back(mk_meta_univ(ngen.next())); - ls = append(ls, to_list(extra_ls.begin(), extra_ls.end())); + expr f = get_app_fn(e); + if (!is_constant(f)) + throw_failed(e); + optional it = tc.env().find(const_name(f)); + if (!it || !it->is_definition()) + throw_failed(e); + expr v = it->get_value(); + if (is_builtin_tactic(v)) { + auto const & map = get_expr_to_tactic_map(); + auto it2 = map.find(const_name(f)); + if (it2 != map.end()) + return it2->second(tc, fn, e, p); + else + throw expr_to_tactic_exception(e, sstream() << "implementation for builtin tactic '" << + const_name(f) << "' was not found"); + } else { + // unfold definition + buffer locals; + get_app_rev_args(e, locals); + level_param_names const & ps = it->get_univ_params(); + levels ls = const_levels(f); + unsigned num_ps = length(ps); + unsigned num_ls = length(ls); + if (num_ls > num_ps) + throw expr_to_tactic_exception(e, sstream() << "invalid number of universes"); + if (num_ls < num_ps) { + buffer extra_ls; + name_generator ngen = tc.mk_ngen(); + for (unsigned i = num_ls; i < num_ps; i++) + extra_ls.push_back(mk_meta_univ(ngen.next())); + ls = append(ls, to_list(extra_ls.begin(), extra_ls.end())); + } + v = instantiate_univ_params(v, ps, ls); + v = apply_beta(v, locals.size(), locals.data()); + return expr_to_tactic(tc, fn, v, p); } - v = instantiate_univ_params(v, ps, ls); - v = apply_beta(v, locals.size(), locals.data()); - return expr_to_tactic(tc, v, p); } } @@ -116,19 +213,21 @@ static name_generator next_name_generator() { return name_generator(name(*g_tmp_prefix, r)); } -tactic expr_to_tactic(environment const & env, expr const & e, pos_info_provider const * p) { +tactic expr_to_tactic(environment const & env, elaborate_fn const & fn, expr const & e, pos_info_provider const * p) { + // std::cout << "expr_to_tactic: " << e << "\n"; + flet let(g_unfold_tactic_macros, false); type_checker tc(env, next_name_generator()); - return expr_to_tactic(tc, e, p); + return expr_to_tactic(tc, fn, e, p); } -tactic fixpoint(expr const & b) { +tactic fixpoint(expr const & b, elaborate_fn const & fn) { return tactic([=](environment const & env, io_state const & ios, proof_state const & s) -> proof_state_seq { - return expr_to_tactic(env, b, nullptr)(env, ios, s); + return expr_to_tactic(env, fn, b, nullptr)(env, ios, s); }); } void register_simple_tac(name const & n, std::function f) { - register_tac(n, [=](type_checker &, expr const & e, pos_info_provider const *) { + register_tac(n, [=](type_checker &, elaborate_fn const &, expr const & e, pos_info_provider const *) { if (!is_constant(e)) throw expr_to_tactic_exception(e, "invalid constant tactic"); return f(); @@ -136,40 +235,42 @@ void register_simple_tac(name const & n, std::function f) { } void register_bin_tac(name const & n, std::function f) { - register_tac(n, [=](type_checker & tc, expr const & e, pos_info_provider const * p) { + register_tac(n, [=](type_checker & tc, elaborate_fn const & fn, expr const & e, pos_info_provider const * p) { buffer args; get_app_args(e, args); if (args.size() != 2) throw expr_to_tactic_exception(e, "invalid binary tactic, it must have two arguments"); - return f(expr_to_tactic(tc, args[0], p), - expr_to_tactic(tc, args[1], p)); + return f(expr_to_tactic(tc, fn, args[0], p), + expr_to_tactic(tc, fn, args[1], p)); }); } void register_unary_tac(name const & n, std::function f) { - register_tac(n, [=](type_checker & tc, expr const & e, pos_info_provider const * p) { + register_tac(n, [=](type_checker & tc, elaborate_fn const & fn, expr const & e, pos_info_provider const * p) { buffer args; get_app_args(e, args); if (args.size() != 1) throw expr_to_tactic_exception(e, "invalid unary tactic, it must have one argument"); - return f(expr_to_tactic(tc, args[0], p)); + return f(expr_to_tactic(tc, fn, args[0], p)); }); } void register_unary_num_tac(name const & n, std::function f) { - register_tac(n, [=](type_checker & tc, expr const & e, pos_info_provider const * p) { + register_tac(n, [=](type_checker & tc, elaborate_fn const & fn, expr const & e, pos_info_provider const * p) { buffer args; get_app_args(e, args); if (args.size() != 2) throw expr_to_tactic_exception(e, "invalid tactic, it must have two arguments"); - tactic t = expr_to_tactic(tc, args[0], p); + tactic t = expr_to_tactic(tc, fn, args[0], p); optional k = to_num(args[1]); if (!k) k = to_num(tc.whnf(args[1]).first); if (!k) throw expr_to_tactic_exception(e, "invalid tactic, second argument must be a numeral"); if (!k->is_unsigned_int()) - throw expr_to_tactic_exception(e, "invalid tactic, second argument does not fit in a machine unsigned integer"); + throw expr_to_tactic_exception(e, + "invalid tactic, second argument does not fit in " + "a machine unsigned integer"); return f(t, k->get_unsigned_int()); }); } @@ -180,6 +281,11 @@ 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); } +static void check_macro_args(expr const & e, unsigned num_args, char const * msg) { + if (macro_num_args(e) != num_args) + throw expr_to_tactic_exception(e, msg); +} + void initialize_expr_to_tactic() { g_tmp_prefix = new name(name::mk_internal_unique_name()); @@ -188,76 +294,116 @@ void initialize_expr_to_tactic() { g_map = new expr_to_tactic_map(); - name g_tac("tactic"); - name g_builtin_tac_name(g_tac, "builtin"); - name g_exact_tac_name(g_tac, "exact"); - name g_and_then_tac_name(g_tac, "and_then"); - name g_or_else_tac_name(g_tac, "or_else"); - name g_repeat_tac_name(g_tac, "repeat"); - name g_fixpoint_name(g_tac, "fixpoint"); - name g_determ_tac_name(g_tac, "determ"); - g_exact_tac_fn = new expr(Const(g_exact_tac_name)); - g_and_then_tac_fn = new expr(Const(g_and_then_tac_name)); - g_or_else_tac_fn = new expr(Const(g_or_else_tac_name)); - g_repeat_tac_fn = new expr(Const(g_repeat_tac_name)); - g_determ_tac_fn = new expr(Const(g_determ_tac_name)); - g_tac_type = new expr(Const(g_tac)); - g_builtin_tac = new expr(Const(g_builtin_tac_name)); - g_fixpoint_tac = new expr(Const(g_fixpoint_name)); + g_tactic_name = new name("tactic"); + g_tactic_opcode = new std::string("TAC"); - register_simple_tac(name(g_tac, "id"), []() { return id_tactic(); }); - register_simple_tac(name(g_tac, "now"), []() { return now_tactic(); }); - register_simple_tac(name(g_tac, "assumption"), []() { return assumption_tactic(); }); - register_simple_tac(name(g_tac, "eassumption"), []() { return eassumption_tactic(); }); - register_simple_tac(name(g_tac, "fail"), []() { return fail_tactic(); }); - register_simple_tac(name(g_tac, "beta"), []() { return beta_tactic(); }); - register_bin_tac(g_and_then_tac_name, [](tactic const & t1, tactic const & t2) { return then(t1, t2); }); - register_bin_tac(name(g_tac, "append"), [](tactic const & t1, tactic const & t2) { return append(t1, t2); }); - register_bin_tac(name(g_tac, "interleave"), [](tactic const & t1, tactic const & t2) { return interleave(t1, t2); }); - register_bin_tac(name(g_tac, "par"), [](tactic const & t1, tactic const & t2) { return par(t1, t2); }); - register_bin_tac(g_or_else_tac_name, [](tactic const & t1, tactic const & t2) { return orelse(t1, t2); }); - register_unary_tac(g_repeat_tac_name, [](tactic const & t1) { return repeat(t1); }); - register_tac(name(g_tac, "state"), [](type_checker &, expr const & e, pos_info_provider const * p) { - if (p) - if (auto it = p->get_pos_info(e)) - return trace_state_tactic(std::string(p->get_file_name()), *it); - return trace_state_tactic(); - }); - register_tac(name(g_tac, "trace"), [](type_checker & tc, expr const & e, pos_info_provider const *) { - buffer args; - get_app_args(e, args); - if (args.size() != 1) - throw expr_to_tactic_exception(e, "invalid trace tactic, argument expected"); - if (auto str = to_string(args[0])) - return trace_tactic(*str); - else if (auto str = to_string(tc.whnf(args[0]).first)) - return trace_tactic(*str); - else - throw expr_to_tactic_exception(e, "invalid trace tactic, string value expected"); - }); - register_tac(name(g_tac, "apply"), [](type_checker &, expr const & e, pos_info_provider const *) { - return apply_tactic(app_arg(e)); - }); - register_tac(g_exact_tac_name, [](type_checker &, expr const & e, pos_info_provider const *) { - return exact_tactic(app_arg(e)); - }); - register_tac(name(g_tac, "unfold"), [](type_checker &, expr const & e, pos_info_provider const *) { - expr id = get_app_fn(app_arg(e)); - if (!is_constant(id)) - return fail_tactic(); - else - return unfold_tactic(const_name(id)); - }); - register_unary_num_tac(name(g_tac, "at_most"), [](tactic const & t, unsigned k) { return take(t, k); }); - register_unary_num_tac(name(g_tac, "discard"), [](tactic const & t, unsigned k) { return discard(t, k); }); - register_unary_num_tac(name(g_tac, "focus_at"), [](tactic const & t, unsigned k) { return focus(t, k); }); - register_unary_num_tac(name(g_tac, "try_for"), [](tactic const & t, unsigned k) { return try_for(t, k); }); - register_tac(g_fixpoint_name, [](type_checker & tc, expr const & e, pos_info_provider const *) { - if (!is_constant(app_fn(e))) - throw expr_to_tactic_exception(e, "invalid fixpoint tactic, it must have one argument"); - expr r = tc.whnf(mk_app(app_arg(e), e)).first; - return fixpoint(r); - }); + g_tactic_macros = new tactic_macros(); + + register_macro_deserializer(*g_tactic_opcode, + [](deserializer & d, unsigned num, expr const * args) { + name kind; + d >> kind; + return mk_tactic_macro(kind, num, args); + }); + + g_apply_tactic_name = new name(*g_tactic_name, "apply"); + + name builtin_tac_name(*g_tactic_name, "builtin"); + name exact_tac_name(*g_tactic_name, "exact"); + name and_then_tac_name(*g_tactic_name, "and_then"); + name or_else_tac_name(*g_tactic_name, "or_else"); + name repeat_tac_name(*g_tactic_name, "repeat"); + name fixpoint_name(*g_tactic_name, "fixpoint"); + name determ_tac_name(*g_tactic_name, "determ"); + name id_tac_name(*g_tactic_name, "id"); + g_exact_tac_fn = new expr(Const(exact_tac_name)); + g_and_then_tac_fn = new expr(Const(and_then_tac_name)); + g_or_else_tac_fn = new expr(Const(or_else_tac_name)); + g_id_tac_fn = new expr(Const(id_tac_name)); + g_repeat_tac_fn = new expr(Const(repeat_tac_name)); + g_determ_tac_fn = new expr(Const(determ_tac_name)); + g_tac_type = new expr(Const(*g_tactic_name)); + g_builtin_tac = new expr(Const(builtin_tac_name)); + g_fixpoint_tac = new expr(Const(fixpoint_name)); + + register_simple_tac(id_tac_name, + []() { return id_tactic(); }); + register_simple_tac(name(*g_tactic_name, "now"), + []() { return now_tactic(); }); + register_simple_tac(name(*g_tactic_name, "assumption"), + []() { return assumption_tactic(); }); + register_simple_tac(name(*g_tactic_name, "eassumption"), + []() { return eassumption_tactic(); }); + register_simple_tac(name(*g_tactic_name, "fail"), + []() { return fail_tactic(); }); + register_simple_tac(name(*g_tactic_name, "beta"), + []() { return beta_tactic(); }); + register_bin_tac(and_then_tac_name, + [](tactic const & t1, tactic const & t2) { return then(t1, t2); }); + register_bin_tac(name(*g_tactic_name, "append"), + [](tactic const & t1, tactic const & t2) { return append(t1, t2); }); + register_bin_tac(name(*g_tactic_name, "interleave"), + [](tactic const & t1, tactic const & t2) { return interleave(t1, t2); }); + register_bin_tac(name(*g_tactic_name, "par"), + [](tactic const & t1, tactic const & t2) { return par(t1, t2); }); + register_bin_tac(or_else_tac_name, + [](tactic const & t1, tactic const & t2) { return orelse(t1, t2); }); + register_unary_tac(repeat_tac_name, + [](tactic const & t1) { return repeat(t1); }); + register_tac(name(*g_tactic_name, "state"), + [](type_checker &, elaborate_fn const &, expr const & e, pos_info_provider const * p) { + if (p) + if (auto it = p->get_pos_info(e)) + return trace_state_tactic(std::string(p->get_file_name()), *it); + return trace_state_tactic(); + }); + register_tac(name(*g_tactic_name, "trace"), + [](type_checker & tc, elaborate_fn const &, expr const & e, pos_info_provider const *) { + buffer args; + get_app_args(e, args); + if (args.size() != 1) + throw expr_to_tactic_exception(e, "invalid trace tactic, argument expected"); + if (auto str = to_string(args[0])) + return trace_tactic(*str); + else if (auto str = to_string(tc.whnf(args[0]).first)) + return trace_tactic(*str); + else + throw expr_to_tactic_exception(e, "invalid trace tactic, string value expected"); + }); + register_tacm(*g_apply_tactic_name, + [](type_checker &, elaborate_fn const & fn, expr const & e, pos_info_provider const *) { + // std::cout << "gen apply: " << e << "\n"; + check_macro_args(e, 1, "invalid 'apply' tactic, it must have one argument"); + return apply_tactic(fn, macro_arg(e, 0)); + }); + register_tac(exact_tac_name, + [](type_checker &, elaborate_fn const &, expr const & e, pos_info_provider const *) { + // TODO(Leo): use elaborate_fn + return exact_tactic(app_arg(e)); + }); + register_tac(name(*g_tactic_name, "unfold"), + [](type_checker &, elaborate_fn const &, expr const & e, pos_info_provider const *) { + expr id = get_app_fn(app_arg(e)); + if (!is_constant(id)) + return fail_tactic(); + else + return unfold_tactic(const_name(id)); + }); + register_unary_num_tac(name(*g_tactic_name, "at_most"), + [](tactic const & t, unsigned k) { return take(t, k); }); + register_unary_num_tac(name(*g_tactic_name, "discard"), + [](tactic const & t, unsigned k) { return discard(t, k); }); + register_unary_num_tac(name(*g_tactic_name, "focus_at"), + [](tactic const & t, unsigned k) { return focus(t, k); }); + register_unary_num_tac(name(*g_tactic_name, "try_for"), + [](tactic const & t, unsigned k) { return try_for(t, k); }); + register_tac(fixpoint_name, + [](type_checker & tc, elaborate_fn const & fn, expr const & e, pos_info_provider const *) { + if (!is_constant(app_fn(e))) + throw expr_to_tactic_exception(e, "invalid fixpoint tactic, it must have one argument"); + expr r = tc.whnf(mk_app(app_arg(e), e)).first; + return fixpoint(r, fn); + }); } void finalize_expr_to_tactic() { @@ -268,8 +414,13 @@ void finalize_expr_to_tactic() { delete g_repeat_tac_fn; delete g_or_else_tac_fn; delete g_and_then_tac_fn; + delete g_id_tac_fn; delete g_exact_tac_fn; + delete g_apply_tactic_name; + delete g_tactic_macros; delete g_map; + delete g_tactic_name; + delete g_tactic_opcode; delete g_by_name; delete g_tmp_prefix; } diff --git a/src/library/tactic/expr_to_tactic.h b/src/library/tactic/expr_to_tactic.h index efbadfd3a9..210887a75f 100644 --- a/src/library/tactic/expr_to_tactic.h +++ b/src/library/tactic/expr_to_tactic.h @@ -24,7 +24,7 @@ bool has_tactic_decls(environment const & env); and definitions marked as 'tactic.builtin' are handled by the code registered using \c register_expr_to_tactic. */ -tactic expr_to_tactic(environment const & env, expr const & e, pos_info_provider const *p); +tactic expr_to_tactic(environment const & env, elaborate_fn const & fn, expr const & e, pos_info_provider const * p); /** \brief Create an expression `by t`, where \c t is an expression of type `tactic`. @@ -44,9 +44,15 @@ expr const & get_tactic_type(); expr const & get_exact_tac_fn(); expr const & get_and_then_tac_fn(); expr const & get_or_else_tac_fn(); +expr const & get_id_tac_fn(); expr const & get_repeat_tac_fn(); expr const & get_determ_tac_fn(); +expr mk_tactic_macro(name const & kind, unsigned num_args, expr const * args); +expr mk_tactic_macro(name const & kind, expr const & e); +bool is_tactic_macro(expr const & e); +expr mk_apply_tactic_macro(expr const & e); + /** \brief Exception used to report a problem when an expression is being converted into a tactic. */ class expr_to_tactic_exception : public tactic_exception { public: @@ -54,7 +60,8 @@ public: expr_to_tactic_exception(expr const & e, sstream const & strm):tactic_exception(e, strm) {} }; -typedef std::function expr_to_tactic_fn; +typedef std::function +expr_to_tactic_fn; /** \brief Register a new "procedural attachment" for expr_to_tactic. */ void register_tac(name const & n, expr_to_tactic_fn const & fn); diff --git a/src/library/tactic/goal.cpp b/src/library/tactic/goal.cpp index a50dbe67b4..969e3f772a 100644 --- a/src/library/tactic/goal.cpp +++ b/src/library/tactic/goal.cpp @@ -92,6 +92,12 @@ bool goal::validate(environment const & env) const { } } +list goal::to_context() const { + buffer locals; + get_app_rev_args(m_meta, locals); + return to_list(locals.begin(), locals.end()); +} + DECL_UDATA(goal) static int mk_goal(lua_State * L) { return push_goal(L, goal(to_expr(L, 1), to_expr(L, 2))); } diff --git a/src/library/tactic/goal.h b/src/library/tactic/goal.h index 5716f38ea8..0689accb08 100644 --- a/src/library/tactic/goal.h +++ b/src/library/tactic/goal.h @@ -44,32 +44,34 @@ public: expr get_mvar() const { return get_app_fn(m_meta); } - /** - \brief Given a term \c v with type get_type(), build a lambda abstraction + /** \brief Given a term \c v with type get_type(), build a lambda abstraction that is the solution for the metavariable associated with this goal. */ expr abstract(expr const & v) const; - /** - \brief Create a metavariable application (?m l_1 ... l_n) with the given type, + /** \brief Create a metavariable application (?m l_1 ... l_n) with the given type, and the locals from this goal. If only_contextual == true, then we only include the local constants that are marked as contextual. */ expr mk_meta(name const & m, expr const & type, bool only_contextual = true) const; - /** - brief Return true iff get_type() only contains local constants that arguments + /** \brief Return true iff get_type() only contains local constants that arguments of get_meta(), and each argument of get_meta() only contains local constants that are previous arguments. */ bool validate_locals() const; - /** - \brief Return true iff \c validate_locals() return true and type of \c get_meta() in + /** \brief Return true iff \c validate_locals() return true and type of \c get_meta() in \c env is get_type() */ bool validate(environment const & env) const; + /** \brief Return the goal's "context". + That is, given ?m l_1 ... l_n, return the list + [l_n, ..., l_1] + */ + list to_context() const; + format pp(formatter const & fmt) const; }; diff --git a/src/library/tactic/proof_state.cpp b/src/library/tactic/proof_state.cpp index a4f3166cd6..54b779c668 100644 --- a/src/library/tactic/proof_state.cpp +++ b/src/library/tactic/proof_state.cpp @@ -30,6 +30,15 @@ bool get_proof_state_goal_names(options const & opts) { return opts.get_bool(*g_proof_state_goal_names, LEAN_PROOF_STATE_GOAL_NAMES); } +proof_state::proof_state(goals const & gs, substitution const & s, + name_generator const & ngen, constraints const & postponed): + m_goals(gs), m_subst(s), m_ngen(ngen), m_postponed(postponed) { + if (std::any_of(gs.begin(), gs.end(), + [&](goal const & g) { return s.is_assigned(g.get_mvar()); })) { + m_goals = filter(gs, [&](goal const & g) { return !s.is_assigned(g.get_mvar()); }); + } +} + format proof_state::pp(formatter const & fmt) const { options const & opts = fmt.get_options(); bool show_goal_names = get_proof_state_goal_names(opts); @@ -67,8 +76,12 @@ io_state_stream const & operator<<(io_state_stream const & out, proof_state cons return out; } +proof_state to_proof_state(expr const & meta, expr const & type, substitution const & subst, name_generator ngen) { + return proof_state(goals(goal(meta, type)), subst, ngen, constraints()); +} + proof_state to_proof_state(expr const & meta, expr const & type, name_generator ngen) { - return proof_state(goals(goal(meta, type)), substitution(), ngen); + return to_proof_state(meta, type, substitution(), ngen); } DECL_UDATA(goals) @@ -148,10 +161,11 @@ static int mk_proof_state(lua_State * L) { int nargs = lua_gettop(L); if (nargs == 2) { return push_proof_state(L, proof_state(to_proof_state(L, 1), to_goals(L, 2))); - } else if (nargs == 3) { + } else if (nargs == 3 && is_proof_state(L, 1)) { return push_proof_state(L, proof_state(to_proof_state(L, 1), to_goals(L, 2), to_substitution(L, 3))); - } else if (nargs == 4) { - return push_proof_state(L, proof_state(to_goals(L, 1), to_substitution(L, 2), to_name_generator(L, 3))); + } else if (nargs == 3) { + return push_proof_state(L, proof_state(to_goals(L, 1), to_substitution(L, 2), to_name_generator(L, 3), + constraints())); } else { throw exception("proof_state invalid number of arguments"); } diff --git a/src/library/tactic/proof_state.h b/src/library/tactic/proof_state.h index 3ecad84e34..6d8410b938 100644 --- a/src/library/tactic/proof_state.h +++ b/src/library/tactic/proof_state.h @@ -19,16 +19,20 @@ class proof_state { goals m_goals; substitution m_subst; name_generator m_ngen; + constraints m_postponed; public: - proof_state(goals const & gs, substitution const & s, name_generator const & ngen): - m_goals(gs), m_subst(s), m_ngen(ngen) {} - proof_state(proof_state const & s, goals const & gs, substitution const & subst):proof_state(gs, subst, s.m_ngen) {} - proof_state(proof_state const & s, goals const & gs):proof_state(s, gs, s.m_subst) {} - proof_state(proof_state const & s, name_generator const & ngen):proof_state(s.m_goals, s.m_subst, ngen) {} + proof_state(goals const & gs, substitution const & s, name_generator const & ngen, constraints const & postponed); + proof_state(proof_state const & s, goals const & gs, substitution const & subst): + proof_state(gs, subst, s.m_ngen, s.m_postponed) {} + proof_state(proof_state const & s, goals const & gs): + proof_state(s, gs, s.m_subst) {} + proof_state(proof_state const & s, name_generator const & ngen): + proof_state(s.m_goals, s.m_subst, ngen, s.m_postponed) {} goals const & get_goals() const { return m_goals; } substitution const & get_subst() const { return m_subst; } name_generator const & get_ngen() const { return m_ngen; } + constraints const & get_postponed() const { return m_postponed; } /** \brief Return true iff this state does not have any goals left */ bool is_final_state() const { return empty(m_goals); } @@ -38,6 +42,7 @@ public: inline optional some_proof_state(proof_state const & s) { return some(s); } inline optional none_proof_state() { return optional (); } +proof_state to_proof_state(expr const & meta, expr const & type, substitution const & subst, name_generator ngen); proof_state to_proof_state(expr const & meta, expr const & type, name_generator ngen); goals map_goals(proof_state const & s, std::function(goal const & g)> f); diff --git a/src/library/tactic/tactic.h b/src/library/tactic/tactic.h index fee055c6c8..0c3c90e82b 100644 --- a/src/library/tactic/tactic.h +++ b/src/library/tactic/tactic.h @@ -14,6 +14,11 @@ Author: Leonardo de Moura #include "library/tactic/proof_state.h" namespace lean { +/** \brief Function for elaborating expressions nested in tactics. + Some tactics contain nested expression (aka pre-terms) that need to be elaborated. +*/ +typedef std::function(goal const &, name_generator const &, expr const &)> elaborate_fn; + /** \brief Throw an exception is \c v contains local constants, \c e is only used for position information. */ void check_has_no_local(expr const & v, expr const & e, char const * tac_name); diff --git a/tests/lean/have1.lean b/tests/lean/have1.lean index 30444a0165..30fe172f64 100644 --- a/tests/lean/have1.lean +++ b/tests/lean/have1.lean @@ -6,7 +6,7 @@ axiom H1 : a = b axiom H2 : b = c check have e1 [visible] : a = b, from H1, - have e2 : a = c, by apply trans; apply e1; apply H2, + have e2 : a = c, by apply trans; apply H2; apply e1, have e3 : c = a, from e2⁻¹, have e4 [visible] : b = a, from e1⁻¹, have e5 : b = c, from e4 ⬝ e2, diff --git a/tests/lean/run/beginend.lean b/tests/lean/run/beginend.lean new file mode 100644 index 0000000000..763e257cca --- /dev/null +++ b/tests/lean/run/beginend.lean @@ -0,0 +1,9 @@ +import tools.tactic +open tactic + +theorem foo (A : Type) (a b c : A) (Hab : a = b) (Hbc : b = c) : a = c := +begin + apply eq.trans, + apply Hbc, + apply Hab +end diff --git a/tests/lean/run/tactic10.lean b/tests/lean/run/tactic10.lean index 061d6be3bd..80545111a0 100644 --- a/tests/lean/run/tactic10.lean +++ b/tests/lean/run/tactic10.lean @@ -3,7 +3,7 @@ open tactic theorem tst (a b : Prop) (H : a ↔ b) : b ↔ a := by apply iff.intro; - apply (assume Hb, iff.elim_right H Hb); - apply (assume Ha, iff.elim_left H Ha) + apply (assume Ha, iff.elim_left H Ha); + apply (assume Hb, iff.elim_right H Hb) check tst diff --git a/tests/lean/run/tactic11.lean b/tests/lean/run/tactic11.lean index 32eaabea28..76675f6c93 100644 --- a/tests/lean/run/tactic11.lean +++ b/tests/lean/run/tactic11.lean @@ -5,5 +5,14 @@ theorem tst (a b : Prop) (H : a ↔ b) : b ↔ a := have H1 [visible] : a → b, -- We need to mark H1 as fact, otherwise it is not visible by tactics from iff.elim_left H, by apply iff.intro; - apply (assume Hb, iff.elim_right H Hb); - apply (assume Ha, H1 Ha) + apply (assume Ha, H1 Ha); + apply (assume Hb, iff.elim_right H Hb) + +theorem tst2 (a b : Prop) (H : a ↔ b) : b ↔ a +:= have H1 [visible] : a → b, + from iff.elim_left H, + begin + apply iff.intro, + apply (assume Ha, H1 Ha), + apply (assume Hb, iff.elim_right H Hb) + end diff --git a/tests/lean/run/tactic12.lean b/tests/lean/run/tactic12.lean index 7798f06844..c09288c2cd 100644 --- a/tests/lean/run/tactic12.lean +++ b/tests/lean/run/tactic12.lean @@ -3,9 +3,9 @@ open tactic theorem tst (a b : Prop) (H : ¬ a ∨ ¬ b) (Hb : b) : ¬ a ∧ b := by apply and.intro; + assumption; apply not_intro; exact (assume Ha, or.elim H (assume Hna, @absurd _ false Ha Hna) - (assume Hnb, @absurd _ false Hb Hnb)); - assumption + (assume Hnb, @absurd _ false Hb Hnb)) diff --git a/tests/lean/run/tactic13.lean b/tests/lean/run/tactic13.lean index 34bbd1f10f..c51161b9f8 100644 --- a/tests/lean/run/tactic13.lean +++ b/tests/lean/run/tactic13.lean @@ -4,9 +4,9 @@ open tactic theorem tst (a b : Prop) (H : ¬ a ∨ ¬ b) (Hb : b) : ¬ a ∧ b := begin apply and.intro, + assumption, apply not_intro, assume Ha, or.elim H (assume Hna, @absurd _ false Ha Hna) - (assume Hnb, @absurd _ false Hb Hnb), - assumption + (assume Hnb, @absurd _ false Hb Hnb) end diff --git a/tests/lean/run/tactic17.lean b/tests/lean/run/tactic17.lean index 962d0afe41..b8f0ebe99b 100644 --- a/tests/lean/run/tactic17.lean +++ b/tests/lean/run/tactic17.lean @@ -4,7 +4,10 @@ open tactic constant A : Type.{1} constant f : A → A → A -theorem tst {a b c : A} (H1 : a = b) (H2 : b = c) : f a b = f b c -:= by apply (@congr A A _ _ (f a) (f b)); - apply (congr_arg f); - !assumption +theorem tst {a b c : A} (H1 : a = b) (H2 : b = c) : f a b = f b c := +begin + apply (@congr A A _ _ (f a) (f b)), + assumption, + apply (congr_arg f), + assumption +end diff --git a/tests/lean/run/tactic18.lean b/tests/lean/run/tactic18.lean index 3ea937658d..cc1fc0ebec 100644 --- a/tests/lean/run/tactic18.lean +++ b/tests/lean/run/tactic18.lean @@ -5,7 +5,6 @@ constant A : Type.{1} constant f : A → A → A theorem tst {a b c : A} (H1 : a = b) (H2 : b = c) : f a b = f b c -:= by apply (@congr A A); +:= by apply (eq.subst H1); apply (eq.subst H2); - apply eq.refl; - assumption + apply eq.refl diff --git a/tests/lean/run/tactic19.lean b/tests/lean/run/tactic19.lean index 9ca23e9d9d..155bfc8a5e 100644 --- a/tests/lean/run/tactic19.lean +++ b/tests/lean/run/tactic19.lean @@ -2,7 +2,6 @@ import logic open tactic theorem tst {A : Type} {f : A → A → A} {a b c : A} (H1 : a = b) (H2 : b = c) : f a b = f b c -:= by apply congr; - apply (eq.subst H2); - apply eq.refl; - assumption +:= by apply (eq.subst H2); + apply (eq.subst H1); + apply eq.refl diff --git a/tests/lean/run/tactic29.lean b/tests/lean/run/tactic29.lean index f557c4179f..b3c6bac878 100644 --- a/tests/lean/run/tactic29.lean +++ b/tests/lean/run/tactic29.lean @@ -12,7 +12,7 @@ section check H check H2 theorem test : a = b ∧ a = a - := by apply and.intro; apply H; apply eq.refl + := by apply and.intro; apply eq.refl; apply H end check @test diff --git a/tests/lean/run/tactic8.lean b/tests/lean/run/tactic8.lean index 1150e2a542..fd771a7d81 100644 --- a/tests/lean/run/tactic8.lean +++ b/tests/lean/run/tactic8.lean @@ -1,9 +1,9 @@ import logic open tactic -theorem tst {A B : Prop} (H1 : A) (H2 : B) : A ∧ B ∧ A -:= by (apply @and.intro; - apply (show A, from H1); - apply (show B ∧ A, from and.intro H2 H1)) +theorem tst {A B : Prop} (H1 : A) (H2 : B) : A ∧ B ∧ A := +by apply @and.intro; + apply (show B ∧ A, from and.intro H2 H1); + apply (show A, from H1) check @tst diff --git a/tests/lean/show1.lean b/tests/lean/show1.lean index 4efbb3d37c..4e83014f8e 100644 --- a/tests/lean/show1.lean +++ b/tests/lean/show1.lean @@ -8,7 +8,7 @@ axiom H2 : b = c check show a = c, from H1 ⬝ H2 print "------------" check have e1 [visible] : a = b, from H1, - have e2 : a = c, by apply eq.trans; apply e1; apply H2, + have e2 : a = c, by apply eq.trans; apply H2; apply e1, have e3 : c = a, from e2⁻¹, have e4 [visible] : b = a, from e1⁻¹, show b = c, from e1⁻¹ ⬝ e2